論文の概要: Hilbert: Recursively Building Formal Proofs with Informal Reasoning

• arxiv url: http://arxiv.org/abs/2509.22819v1
• Date: Fri, 26 Sep 2025 18:24:23 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-09-30 22:32:18.890899
• Title: Hilbert: Recursively Building Formal Proofs with Informal Reasoning
• Title（参考訳）: Hilbert: Informal Reasoningを使ったフォーマルな証明を再帰的に構築する
• Authors: Sumanth Varambally, Thomas Voice, Yanchao Sun, Zhifeng Chen, Rose Yu, Ke Ye,
• Abstract要約: 大規模言語モデル(LLM)は、驚くべき数学的推論能力を示しているが、そのソリューションには自動検証できないエラーが含まれていることが多い。 非公式な推論と形式的検証の相補的な強みを組み合わせたエージェントフレームワークであるHilbertを紹介する。 我々のシステムは4つのコンポーネントを編成する: 数学的推論に優れる非公式のLLM、リーン4の戦術に最適化された特殊なLLM、形式検証器、意味定理検索器。
• 参考スコア（独自算出の注目度）: 38.36481253622752
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Large Language Models (LLMs) demonstrate impressive mathematical reasoning abilities, but their solutions frequently contain errors that cannot be automatically verified. Formal theorem proving systems such as Lean 4 offer automated verification with complete accuracy, motivating recent efforts to build specialized prover LLMs that generate verifiable proofs in formal languages. However, a significant gap remains: current prover LLMs solve substantially fewer problems than general-purpose LLMs operating in natural language. We introduce Hilbert, an agentic framework that bridges this gap by combining the complementary strengths of informal reasoning and formal verification. Our system orchestrates four components: an informal LLM that excels at mathematical reasoning, a specialized prover LLM optimized for Lean 4 tactics, a formal verifier, and a semantic theorem retriever. Given a problem that the prover is unable to solve, Hilbert employs recursive decomposition to split the problem into subgoals that it solves with the prover or reasoner LLM. It leverages verifier feedback to refine incorrect proofs as necessary. Experimental results demonstrate that Hilbert substantially outperforms existing approaches on key benchmarks, achieving 99.2% on miniF2F, 6.6% points above the best publicly available method. Hilbert achieves the best known result on PutnamBench. It solves 462/660 problems (70.0%), outperforming proprietary approaches like SeedProver (50.4%) and achieving a 422% improvement over the best publicly available baseline. Thus, Hilbert effectively narrows the gap between informal reasoning and formal proof generation.
• Abstract（参考訳）: 大規模言語モデル(LLM)は、驚くべき数学的推論能力を示すが、そのソリューションには自動検証できないエラーが頻繁に含まれている。 Lean 4のような形式的定理証明システムは、完全な精度で自動検証を提供する。 しかし、大きなギャップが残っている: 現在の証明子 LLM は、自然言語で動作する汎用 LLM よりも、かなり少ない問題を解く。 非公式な推論と形式的検証の相補的な強みを組み合わせることで、このギャップを橋渡しするエージェントフレームワークであるHilbertを紹介します。 我々のシステムは4つのコンポーネントを編成する: 数学的推論に優れる非公式のLLM、リーン4の戦術に最適化された特殊なLLM、形式検証器、意味定理検索器。 証明者が解けない問題を考えると、ヒルベルトは再帰分解を用いて問題を証明者または推論者 LLM で解ける部分ゴールに分割する。 検証器のフィードバックを利用して、不正確な証明を必要に応じて洗練する。 実験の結果、ヒルベルトは鍵となるベンチマークのアプローチをかなり上回り、MiniF2Fで99.2%を達成している。 ヒルベルトはパットナムベンチで最もよく知られた結果を得た。 462/660問題(70.0%)を解決し、SeedProver(50.4%)のようなプロプライエタリなアプローチを上回り、最高の公開ベースラインよりも422%改善している。 したがって、ヒルベルトは非公式な推論と形式的な証明生成の間のギャップを効果的に狭める。

関連論文リスト

• Solving Inequality Proofs with Large Language Models [46.71658812761115]
  不等式証明は様々な科学・数学分野において不可欠である。 これにより、大きな言語モデル(LLM)の需要が高まるフロンティアとなる。 我々は、Olympiadレベルの不平等を専門家が計算したデータセットであるIneqMathをリリースした。
  論文  参考訳（メタデータ） (2025-06-09T16:43:38Z)
• APOLLO: Automated LLM and Lean Collaboration for Advanced Formal Reasoning [8.056359341994941]
  APOLLOは、Leanコンパイラの強みとLLMの推論能力を組み合わせた、モデルに依存しないパイプラインである。 エージェントのセットが証明を分析し、シンタックスのエラーを修正し、リーンを使って証明の誤りを特定します。 修理されたサブステイストは再結合され、再検証され、ユーザ制御された最大試行回数まで反復される。
  論文  参考訳（メタデータ） (2025-05-09T03:38:31Z)
• LeanProgress: Guiding Search for Neural Theorem Proving via Proof Progress Prediction [74.79306773878955]
  証明の進捗を予測する手法であるLeanProgressを紹介します。 実験の結果、LeanProgressは全体の予測精度が75.1%に達することがわかった。
  論文  参考訳（メタデータ） (2025-02-25T07:46:36Z)
• 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)
• Proof Automation with Large Language Models [6.587933406842906]
  大規模言語モデル(LLM)は、自然言語で非公式な証明を自動的に生成する可能性を示している。 本稿では,まず LLM に初期証明を生成することを促し,次に目標とする記号法を利用して低レベルの問題を反復的に修復する,新しい生成・修復手法である PALM を提案する。 その結果、PALMは他の最先端の手法よりも大幅に優れており、76.6%から180.4%の定理を証明できた。
  論文  参考訳（メタデータ） (2024-09-22T00:19:27Z)
• TheoremLlama: Transforming General-Purpose LLMs into Lean4 Experts [26.98890165420689]
  TheoremLlamaは、汎用的なLean4エキスパートをトレーニングするエンドツーエンドフレームワークである。 我々のフレームワークは,MiniF2F-ValidデータセットとTestデータセットでそれぞれ36.48%,33.61%の累積精度を達成した。
  論文  参考訳（メタデータ） (2024-07-03T15:36:18Z)
• 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)

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

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