Benchmark · math

PutnamBench

2 परिणाम 1 मॉडल

PutnamBench स्नातक-स्तरीय प्रतियोगिता गणित पर आधारित एक औपचारिक प्रमेय-सिद्धि (formal theorem-proving) बेंचमार्क है: यह मापता है कि कोई सिस्टम किसी प्रूफ असिस्टेंट (Lean 4, Isabelle या Coq) के भीतर Putnam प्रतियोगिता की कितनी समस्याएँ सिद्ध कर सकता है, और स्कोर मशीन-सत्यापित प्रमाणों की संख्या या अंश होता है।

और पढ़ें

उदाहरण: एक कठिन स्नातक-स्तरीय Putnam समस्या — जैसे संख्या-सिद्धांत का कोई विभाज्यता कथन, किसी समाकल (integral) या असमिका की सीमा, या कोई साहचर्यिक सर्वसमिका (combinatorial identity) — को एक औपचारिक प्रमेय-कथन के रूप में दिया जाता है, जिसका प्रमाण `sorry` के रूप में छोड़ दिया जाता है ताकि सिस्टम उसे पूरा करे।
स्कोरिंग: मीट्रिक उन समस्याओं की संख्या (या प्रतिशत) है जिनके लिए सिस्टम पूर्ण औपचारिक प्रमाण देता है। कोई समस्या तभी गिनी जाती है जब प्रूफ असिस्टेंट उसे पूरी तरह सत्यापित कर दे; आंशिक तर्क या अनौपचारिक विवेचन का स्कोर शून्य होता है।
सत्यापन: परिणाम केवल तभी स्वीकार होता है जब लक्ष्य प्रूफ असिस्टेंट का कर्नेल पूरे प्रमाण की टाइप-जाँच बिना `sorry`, बिना किसी अतिरिक्त स्वयंसिद्ध (axiom) और दिए गए कथन में बदलाव किए बिना कर दे — सत्यापक का हाँ/नहीं ही एकमात्र निर्णायक है।
यह क्यों मायने रखता है: Putnam समस्याएँ स्नातक-स्तरीय गणित की सबसे कठिन समस्याओं में से हैं, और मशीन-जाँचे गए प्रमाण गलत या 'रिवॉर्ड-हैक' किए गए तर्क की कोई गुंजाइश नहीं छोड़ते, जिससे PutnamBench स्वचालित प्रमेय-सिद्धि और गणितीय विवेचन के लिए MiniF2F का एक कठोर और कहीं अधिक कठिन उत्तराधिकारी बन जाता है।

हल किया गया उदाहरण

कार्य

(उदाहरणस्वरूप, सरलीकृत।) PutnamBench प्रारूप में एक Lean 4 प्रमेय, जिसे बिना sorry के सिद्ध करना है: ```lean theorem putnam_illustrative (n : ℕ) : ∑ i ∈ Finset.range n, (2 * i + 1) = n ^ 2 := by sorry ```

समाधान

```lean
theorem putnam_illustrative (n : ℕ) :
    ∑ i ∈ Finset.range n, (2 * i + 1) = n ^ 2 := by
  induction n with
  | zero => simp
  | succ k ih => rw [Finset.sum_range_succ, ih]; ring
```

व्याख्या

पहले n विषम संख्याओं का योग n^2 होता है; इसे आगमन (induction) से सिद्ध किया जाता है: आधार-स्थिति 0 = 0 पर सिमट जाती है, और चरण Finset.sum_range_succ का उपयोग करता है, आगमन-परिकल्पना लगाता है, और k^2 + (2k+1) = (k+1)^2 को ring से बंद कर देता है। यह केवल इसलिए पास होता है क्योंकि Lean का कर्नेल हर चरण स्वीकार करता है — असली PutnamBench समस्या इससे कहीं अधिक कठिन है।

Leanstral 1.5

समयरेखा

तारीख़	मॉडल	स्कोर	स्रोत
2026-07-03	Leanstral 1.5	587.0pts	Mistral ने Leanstral-1.5-119B-A6B जारी किया
2026-07-03	Leanstral 1.5	587.0pts	Leanstral 1.5: सबके लिए प्रूफ की प्रचुरता