要約
数学的問題のための自動化された正式な証明生成で最先端の（SOTA）パフォーマンスを達成するオープンソースの大手言語モデル（LLM）であるGoedel-Proverを紹介します。
この分野の重要な課題は、正式な数学の声明と証明の希少性であり、次の方法で取り組んでいます。
Numinaの自然言語の数学の問題を正式な言語（Lean 4）に翻訳するために、声明のフォーマライザーを訓練し、164万人の正式な声明のデータセットを作成します。
LLMは、正式な声明が元の自然言語の問題の内容を正確に保持することを確認するために使用されます。
次に、一連のプロバーをトレーニングすることにより、正式な証明の大きなデータセットを繰り返し作成します。
各プロバーは、以前のものができないことができない多くの声明を証明することに成功し、これらの新しい証明は次のプロバーのトレーニングセットに追加されます。
最終的なプロバーは、根本的な生成のすべての既存のオープンソースモデルよりも優れています。
MINIF2Fベンチマークでは、57.6％の成功率（Pass@32）を達成し、以前のベストオープンソースモデルを7.6％超えています。
Putnambenchでは、Goedel-Proverは7つの問題（@512を渡す）を正常に解決し、リーダーボードで最初にランキングします。
さらに、リーンワークブックの問題について29.7kの正式な証明を生成し、以前の作品によって生成された15.7kをほぼ2倍にします。
要約(オリジナル)
We introduce Goedel-Prover, an open-source large language model (LLM) that achieves the state-of-the-art (SOTA) performance in automated formal proof generation for mathematical problems. The key challenge in this field is the scarcity of formalized math statements and proofs, which we tackle in the following ways. We train statement formalizers to translate the natural language math problems from Numina into formal language (Lean 4), creating a dataset of 1.64 million formal statements. LLMs are used to check that the formal statements accurately preserve the content of the original natural language problems. We then iteratively build a large dataset of formal proofs by training a series of provers. Each prover succeeds in proving many statements that the previous ones could not, and these new proofs are added to the training set for the next prover. The final prover outperforms all existing open-source models in whole-proof generation. On the miniF2F benchmark, it achieves a 57.6% success rate (Pass@32), exceeding the previous best open-source model by 7.6%. On PutnamBench, Goedel-Prover successfully solves 7 problems (Pass@512), ranking first on the leaderboard. Furthermore, it generates 29.7K formal proofs for Lean Workbook problems, nearly doubling the 15.7K produced by earlier works.
arxiv情報
| 著者 | Yong Lin,Shange Tang,Bohan Lyu,Jiayun Wu,Hongzhou Lin,Kaiyu Yang,Jia Li,Mengzhou Xia,Danqi Chen,Sanjeev Arora,Chi Jin |
| 発行日 | 2025-02-11 15:27:35+00:00 |
| arxivサイト | arxiv_id(pdf) |
提供元, 利用サービス
arxiv.jp, Google