Benchmark · math
PutnamBench
PutnamBench معيار لإثبات المبرهنات بشكل صوري مبني على رياضيات مسابقات المرحلة الجامعية: يقيس كم مسألة من مسابقة Putnam يستطيع النظام إثباتها داخل مساعِد إثبات (Lean 4 أو Isabelle أو Coq)، ويُحتسب بعدد أو نسبة البراهين التي تحقّقت منها الآلة.
اقرأ المزيد
- مثال
- مسألة Putnam جامعية صعبة — مثل ادعاء قابلية قسمة من نظرية الأعداد، أو حدّ لتكامل أو متباينة، أو مطابقة توافيقية — تُقدَّم بوصفها نصّ مبرهنة صوري يُترك برهانه على هيئة `sorry` ليكمله النظام.
- طريقة التقييم
- المقياس هو عدد (أو نسبة) المسائل التي ينتج لها النظام برهانًا صوريًّا كاملًا. لا تُحتسب المسألة إلا إذا تحقّق منها مساعِد الإثبات بالكامل؛ أما الحجج الجزئية أو الاستدلال غير الصوري فدرجتها صفر.
- التحقق
- لا يُقبل الناتج إلا عندما تُجري نواة مساعِد الإثبات المستهدف تدقيق الأنواع للبرهان كاملًا دون `sorry`، ودون بديهيات إضافية، ودون تغيير النص المعطى — وقرار المتحقّق بنعم/لا هو الحَكَم الوحيد.
- لماذا يهم
- تُعدّ مسائل Putnam من أصعب رياضيات المرحلة الجامعية، والبراهين التي تتحقّق منها الآلة لا تترك مجالًا للاستدلال الخاطئ أو المتلاعَب به، ما يجعل PutnamBench خَلَفًا صارمًا وأصعب بكثير لـ MiniF2F في الإثبات الآلي للمبرهنات والاستدلال الرياضي.
مثال محلول
المهمة
(توضيحي ومبسّط.) مبرهنة بلغة Lean 4 بصيغة PutnamBench، يجب إثباتها دون
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؛ ويُثبت بالاستقراء: الحالة الأساسية تؤول إلى 0 = 0، والخطوة تستخدم
Finset.sum_range_succ، وتطبّق فرض الاستقراء، وتُغلق k^2 + (2k+1) = (k+1)^2 بواسطة ring. وهو ينجح فقط لأن نواة Lean تقبل كل خطوة — أما مسألة PutnamBench الحقيقية فأصعب بكثير.| التاريخ | النموذج | النتيجة | المصدر |
|---|---|---|---|
| 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: وفرة البراهين للجميع |