ベンチマーク · math
PutnamBench
PutnamBench は大学レベルの競技数学から作られた形式的定理証明のベンチマークで、システムが証明支援系（Lean 4、Isabelle、Coq）の中で Putnam コンペティションの問題をいくつ証明できるかを測り、機械検証された証明の件数または割合で採点します。
詳しく見る
- 例
- 難しい大学レベルの Putnam 問題——たとえば数論の整除性の主張、積分や不等式の評価、あるいは組合せ論的恒等式——が形式的な定理文として与えられ、その証明は `sorry` として残され、システムが補完します。
- 採点方法
- 指標は、システムが完全な形式的証明を与えた問題の件数（または割合）です。証明支援系が完全に検証した場合にのみその問題は数えられ、部分的な議論や非形式的な推論は 0 点です。
- 検証方法
- 結果は、対象の証明支援系のカーネルが `sorry` なし・追加の公理なし・与えられた文の変更なしで証明全体を型検査したときにのみ受理されます——検証器の可否のみが判定者です。
- 重要な理由
- 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 になり、帰納法で証明します。基底段階は 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: 証明の豊かさ、すべてに |