ゲーデル証明者：オープンソース自動定理証明のためのフロンティアモデル

Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Proving

February 11, 2025

著者: Yong Lin, Shange Tang, Bohan Lyu, Jiayun Wu, Hongzhou Lin, Kaiyu Yang, Jia Li, Mengzhou Xia, Danqi Chen, Sanjeev Arora, Chi Jin

cs.AI

要旨

Goedel-Proverは、数学問題の自動形式証明において最先端のパフォーマンスを達成するオープンソースの大規模言語モデル（LLM）です。この分野における主要な課題は、形式化された数学の文や証明の希少性であり、私たちは以下の方法で取り組んでいます。Numinaから自然言語の数学問題を形式言語（Lean 4）に変換する文の形式化器を訓練し、164万の形式文のデータセットを作成します。LLMは、形式文が元の自然言語の問題の内容を正確に保持しているかをチェックするために使用されます。その後、一連の証明器を訓練して形式証明の大規模なデータセットを反復的に構築します。各証明器は、以前のものでは証明できなかった多くの文を証明に成功し、これらの新しい証明は次の証明器の訓練セットに追加されます。最終的な証明器は、全体の証明生成においてすべての既存のオープンソースモデルを凌駕します。miniF2Fベンチマークでは、32回の試行で57.6％の成功率（Pass@32）を達成し、以前の最高のオープンソースモデルを7.6％上回ります。PutnamBenchでは、Goedel-Proverは7つの問題を成功裏に解決し（Pass@512）、リーダーボードで首位を獲得します。さらに、Lean Workbookの問題に対して29.7Kの形式証明を生成し、以前の作業で生成された15.7Kをほぼ倍増させます。

English

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.