論文の概要: Efficient Proof Generation for Lean Statements with Multiple Candidate Answers

• arxiv url: http://arxiv.org/abs/2610.34490v1
• Date: Sun, 25 Oct 2026 18:32:39 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-10-27 22:27:13.623449
• Title: Efficient Proof Generation for Lean Statements with Multiple Candidate Answers
• Title（参考訳）: 複数の候補回答を持つリーン文書の効率的な証明生成
• Abstract要約: 本稿では,候補解答選択,回答補足,形式的証明生成を統合した共同証明フレームワークを提案する。 その中核は訓練された証明器で、与えられた答えを選択したり、提案したりし、1回の呼び出しで少なくとも1つの答えの証明を生成する。 本フレームワークは,トークンコストの約6分の1で,候補毎の証明生成と同じ形式的証明成功率を達成する。
• 参考スコア（独自算出の注目度）: 10.945354774645098
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: In formal systems such as Lean 4, efficiently finding answers to mathematical problems and generating verifiable proofs is an important task in automated mathematical reasoning. In the traditional way where an upstream solver provides multiple candidate answers, the common workflow requires searching for proofs for each candidate separately, incurring redundant computational cost. To this end, we propose a joint proof framework that integrates candidate answer selection, answer supplementation, and formal proof generation into a unified reasoning process. At its core is a trained prover that selects given or proposes new answers and generates a proof for at least one answer in a single call. Joint proof can also reuse generated proofs to check for faithfulness errors. For problems with a unique answer, if two distinct answers both obtain verifiable proofs under the same formal statement, this confirms the statement does not faithfully preserve the original problem semantics. On MATH-500, AMC 2023, and AIME 2024/2025/2026, our framework achieves the same formal proof success rate as per-candidate proof generation with about one sixth of the token cost, and identifies at least 6.1% of the formalized statements as unfaithful without requiring additional judges. Our model and code are available at https://github.com/Linppz/Gobble-Prover.
• Abstract（参考訳）: リーン4のような形式システムでは、数学的な問題に対する解答を効率よく見つけ、検証可能な証明を生成することが、自動化された数学的推論において重要なタスクである。 アップストリームソルバが複数の候補回答を提供する従来の方法では、一般的なワークフローでは、各候補の証明を別々に検索し、冗長な計算コストを発生させる必要がある。 そこで本研究では,候補解答の選択,補足,形式的証明生成を統一的推論プロセスに統合する共同証明フレームワークを提案する。 その中核は訓練された証明器で、与えられた答えを選択したり、提案したりし、1回の呼び出しで少なくとも1つの答えの証明を生成する。 合同証明はまた、生成した証明を再利用して忠実度エラーをチェックすることもできる。 独特な答えを持つ問題に対して、2つの異なる解が同一の形式的ステートメントの下で検証可能な証明を得た場合、この文は元の問題意味論を忠実に保存していないことを確認する。 MATH-500, AMC 2023, AIME 2024/2025/2026では, トークンコストの約6分の1で候補ごとの証明生成と同じ形式的証明成功率を達成し, さらなる審査を必要とせずに, 少なくとも6.1%の定式化文を不信と判断する。 私たちのモデルとコードはhttps://github.com/Linppz/Gobble-Prover.comで公開されています。

関連論文リスト

• SemantEq: Faithful Bidirectional Equivalence of Formal Statements [13.298690488679421]
  ステートメントの自動形式化は、自然言語からLean 4のような証明アシスタントに数学を翻訳する。 プローバーが強くなるにつれて、正当性の重荷は証明からステートメント、すなわち形式的ステートメントがそのソースを忠実に翻訳するかどうかへと移行する。 より原則化された関係であるSemantEqを紹介します。
  論文  参考訳（メタデータ） (2026-10-23T17:20:12Z)
• Maestro: Agentic Formal Proof Development by Coordination [21.09901199432239]
  Maestroは、グローバルな調整を通じて障害を処理するリーンの証明ハーネスです。 エージェントが飽和していないすべてのベンチマークにおいて、各モデルのネイティブコーディングエージェントよりも多くのターゲットを証明している。 また、共有するベンチマークで発行されたすべての証明システムよりも優れています。
  論文  参考訳（メタデータ） (2026-10-19T07:21:10Z)
• Does the Proof Prove It That Way? Faithful Formalization of Elements Proofs [16.584143060150165]
  我々は,5つの条件を満たす形式的なリーン証明を生成する,エージェント的・オラクル誘導型証明探索であるPristisを紹介した。 その中核は、新しい忠実に保存される分割とコンカレント検索であり、これは orderDecompose という名前で呼ばれる。 ピスティスをユークリッドの要素の最初の3冊の本に適用し、忠実な形式的証明を含む高品質なアーティファクトを創出する。
  論文  参考訳（メタデータ） (2026-08-15T22:20:08Z)
• Safe: Enhancing Mathematical Reasoning in Large Language Models via Retrospective Step-aware Formal Verification [56.218970738892764]
  Chain-of-Thoughtプロンプトは、大規模言語モデル(LLM)から推論能力を引き出すデファクトメソッドとなっている。 検出が極めて難しいCoTの幻覚を緩和するために、現在の方法は不透明なボックスとして機能し、彼らの判断に対する確認可能な証拠を提供しておらず、おそらくその効果を制限する。 任意のスコアを割り当てるのではなく、各推論ステップで形式数学言語Lean 4で数学的主張を明確にし、幻覚を識別するための公式な証明を提供しようとしている。
  論文  参考訳（メタデータ） (2025-06-05T03:16:08Z)
• Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Proving [72.8626512877667]
  我々は,2025年4月5日現在,数学問題の自動証明生成における最先端(最先端)性能を実現する,オープンソースの言語モデルであるGoedel-Proverを紹介した。 まず、自然言語の数学問題をNuminaデータセットからLean 4で等価な形式ステートメントに変換するためにLLMをトレーニングします。 次に,一連のプロデューサをトレーニングすることで,形式証明の大規模なデータセットを開発する。 最後に、Goedel-Pset-v1-solvedというデータセットを取得し、Goedel-Pset-v1から800K以上のステートメントの証明を含む。
  論文  参考訳（メタデータ） (2025-02-11T15:27:35Z)
• A Lean Dataset for International Math Olympiad: Small Steps towards Writing Math Proofs for Hard Problems [0.0]
  リーンの残りのIMO問題に対する完全な、オリジナルの公式な証明を書いています。 この取り組みは,5,880行のリーン証明を作成することで,現在パブリックドメインにある証明の可用性を拡大するものだ。
  論文  参考訳（メタデータ） (2024-11-28T02:50:42Z)
• Generating Natural Language Proofs with Verifier-Guided Search [74.9614610172561]
  NLProofS (Natural Language Proof Search) を提案する。 NLProofSは仮説に基づいて関連するステップを生成することを学習する。 EntailmentBank と RuleTaker の最先端のパフォーマンスを実現している。
  論文  参考訳（メタデータ） (2022-05-25T02:22:30Z)
• multiPRover: Generating Multiple Proofs for Improved Interpretability in Rule Reasoning [73.09791959325204]
  我々は、自然言語の事実と規則の形で明示的な知識を推論することを目的としている言語形式推論の一種に焦点を当てる。 PRoverという名前の最近の研究は、質問に答え、答えを説明する証明グラフを生成することによって、そのような推論を行う。 本研究では,自然言語規則ベースの推論のために複数の証明グラフを生成するという,新たな課題に対処する。
  論文  参考訳（メタデータ） (2021-06-02T17:58:35Z)
• PRover: Proof Generation for Interpretable Reasoning over Rules [81.40404921232192]
  本稿では,ルールベース上の二項質問に応答し,対応する証明を生成するトランスフォーマーモデルを提案する。 本モデルは,効率的な制約付き学習パラダイムを用いて,証明グラフに対応するノードやエッジを予測できることを学習する。 我々は、QAと証明生成のための有望な結果を示すために、合成、手書き、人文による規則ベースの実験を行う。
  論文  参考訳（メタデータ） (2020-10-06T15:47:53Z)

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

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