論文の概要: Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Proving

• arxiv url: http://arxiv.org/abs/2502.07640v2
• Date: Fri, 14 Feb 2025 14:40:12 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-02-17 14:47:26.955693
• Title: Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Proving
• Title（参考訳）: Goedel-Prover: オープンソース自動定理証明のフロンティアモデル
• Authors: Yong Lin, Shange Tang, Bohan Lyu, Jiayun Wu, Hongzhou Lin, Kaiyu Yang, Jia Li, Mengzhou Xia, Danqi Chen, Sanjeev Arora, Chi Jin,
• Abstract要約: 本稿では,オープンソースの大規模言語モデル(LLM)であるGoedel-Proverを紹介する。
• 参考スコア（独自算出の注目度）: 72.8626512877667
• License:
• Abstract: 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. Despite using only supervised fine-tuning, our final prover significantly outperforms the previous best open-source model, DeepSeek-Prover-V1.5, which employs reinforcement learning. On the miniF2F benchmark, our model achieves a success rate of 57.6% (Pass@32), surpassing DeepSeek-Prover-V1.5 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.
• Abstract（参考訳）: 本稿では,オープンソースの大規模言語モデル(LLM)であるGoedel-Proverを紹介する。 この分野での重要な課題は、形式化された数学のステートメントや証明が不足していることである。 我々はステートメントフォーマライザを訓練し、自然言語の数学問題をNuminaからフォーマルな言語(Lean 4)に翻訳し、1億6600万のフォーマルなステートメントのデータセットを作成します。 LLMは、形式文が元の自然言語問題の内容を正確に保存していることを確認するために使用される。 次に、一連のプローバーをトレーニングすることで、形式的証明の大規模なデータセットを反復的に構築する。 それぞれの証明者は、前の証明ができないという多くの主張を証明し、これらの新しい証明が次の証明のためのトレーニングセットに追加される。 教師付き微調整のみを使用しても、これまでの最高のオープンソースモデルであるDeepSeek-Prover-V1.5よりも大幅に優れています。 miniF2Fベンチマークでは、DepSeek-Prover-V1.5を7.6%上回る57.6%(Pass@32)の成功率を達成した。 PutnamBenchでは、Goedel-Proverが7つの問題を解決する(Pass@512)。 さらに、リーンワークブックの問題に対する29.7Kの正式な証明も生成し、以前の成果の15.7Kをほぼ倍増している。

関連論文リスト

• InternLM2.5-StepProver: Advancing Automated Theorem Proving via Expert Iteration on Large-Scale LEAN Problems [47.93470713879515]
  InternLM2.5-SteperはMiniF2F、Lean-Workbook-Plus、ProofNet、Patnamベンチマークのオープンソースステート・オブ・ザ・アートを実現している。 MiniF2Fテストでは65.9%をパスし、Lean-Workbook-Plusの17.0%の問題を証明(あるいは否定)している。
  論文  参考訳（メタデータ） (2024-10-21T07:18:23Z)
• Proof Automation with Large Language Models [6.587933406842906]
  大規模言語モデル(LLM)は、自然言語で非公式な証明を自動的に生成する可能性を示している。 本稿では,まず LLM に初期証明を生成することを促し,次に目標とする記号法を利用して低レベルの問題を反復的に修復する,新しい生成・修復手法である PALM を提案する。 その結果、PALMは他の最先端の手法よりも大幅に優れており、76.6%から180.4%の定理を証明できた。
  論文  参考訳（メタデータ） (2024-09-22T00:19:27Z)
• DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data [65.5290035371111]
  本稿では,高校・学部レベルの数学競争問題から得られたリーン4証明データを生成する手法を提案する。 この合成データセットでDeepSeekMath 7Bモデルを微調整します。 我々のモデルは、Lean 4 Formalized International Mathematical Olympiad (FIMO)ベンチマークで148の問題を5つ証明しましたが、GPT-4は証明できませんでした。
  論文  参考訳（メタデータ） (2024-05-23T09:03:42Z)
• MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data [85.50740598523818]
  MUSTARDは、高品質で多様性のある定理と証明データの均一な合成をマスターするフレームワークである。 5,866個の有効なデータポイントを持つMUSTARDSAUCEベンチマークを示す。 我々は広範囲な解析を行い、MUSTARDが検証された高品質なステップバイステップデータを生成することを示す。
  論文  参考訳（メタデータ） (2024-02-14T05:57:58Z)
• Baldur: Whole-Proof Generation and Repair with Large Language Models [8.100054850290507]
  我々は、自然言語のテキストとコードに基づいて訓練され、証明について微調整された大きな言語モデルを使用して、一度に定理のすべての証明を生成する。 我々は、この証明生成モデルと微調整の補修モデルを組み合わせて、生成した証明を修復し、さらに証明力を増強する。 本手法をプロトタイプであるBaldurで評価し、6,336 Isabelle/HOL定理とその証明のベンチマークで評価する。
  論文  参考訳（メタデータ） (2023-03-08T22:00:15Z)
• Generating Natural Language Proofs with Verifier-Guided Search [74.9614610172561]
  NLProofS (Natural Language Proof Search) を提案する。 NLProofSは仮説に基づいて関連するステップを生成することを学習する。 EntailmentBank と RuleTaker の最先端のパフォーマンスを実現している。
  論文  参考訳（メタデータ） (2022-05-25T02:22:30Z)
• PRover: Proof Generation for Interpretable Reasoning over Rules [81.40404921232192]
  本稿では,ルールベース上の二項質問に応答し,対応する証明を生成するトランスフォーマーモデルを提案する。 本モデルは,効率的な制約付き学習パラダイムを用いて,証明グラフに対応するノードやエッジを予測できることを学習する。 我々は、QAと証明生成のための有望な結果を示すために、合成、手書き、人文による規則ベースの実験を行う。
  論文  参考訳（メタデータ） (2020-10-06T15:47:53Z)

関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。

指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。