ProofBench

概要

ProofBenchは、Vals AIがLean 4の専門家チームとともに作成したベンチマークで、形式的な定理証明の能力を測る。各問題では、自然言語で書かれた定理の主張と、検証済みのLean 4による形式化が組になっており、モデルはLean 4のチェッカーが受理する証明を作らなければならない。問題は大学院または学部上級のレベルで、解析学、代数学、確率論、数論、論理学にわたる。リーダーボードは非公開の100問の分割で実行され、モデルはMathlibの検索ツールとコード実行ツールを使い、1問あたり最大40ターンまでエージェントとして取り組む。

方法論

結果は、公開されているVals AIのProofBenchリーダーボードから取得している。グラフに示すのは証明の成功率、つまりモデルのLean 4の証明が形式的なチェッカーを通った問題の割合である。採点は問題ごとの二値で部分点はない。リーダーボードにある標準誤差、推論の強度（reasoning effort）の設定、レイテンシ、テスト1件あたりのコストはデータのエクスポートに残している。

証明は判定役のモデルではなくLean 4のコンパイラが検査するので、スコアは完全に検証された形式的な正しさを反映する。各モデルは、Vals AIが選んだ固定の推論の強度の設定で1回ずつ掲載されている。リーダーボードにはHarmonicの定理証明システムAristotleも含まれるが、これは独自の実行環境で動くため、保存はするがグラフには載せない。