論文の概要: Automating Mathematical Proof Generation Using Large Language Model Agents and Knowledge Graphs

• arxiv url: http://arxiv.org/abs/2503.11657v2
• Date: Sat, 26 Jul 2025 09:39:50 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-07-29 14:15:45.841683
• Title: Automating Mathematical Proof Generation Using Large Language Model Agents and Knowledge Graphs
• Title（参考訳）: 大規模言語モデルエージェントと知識グラフを用いた数学的証明生成の自動化
• Authors: Vincent Li, Tim Knappe, Yule Fu, Kevin Han, Kevin Zhu,
• Abstract要約: KGプロデューサは、数学的証明の構築と形式化のために汎用LLMを拡張している。 汎用LLMはKG-Proverと組み合わせてミニF2Fテストで最大21%向上した。 KG-ProverはProofNetの2-11%、miniF2F-test、MUSTARDデータセットなど、さらなるスケーリングなしで一貫した改善を実現している。
• 参考スコア（独自算出の注目度）: 2.534053759586253
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Large language models have demonstrated remarkable capabilities in natural language processing tasks requiring multi-step logical reasoning capabilities, such as automated theorem proving. However, challenges persist within theorem proving, such as the identification of key mathematical concepts, understanding their interrelationships, and formalizing proofs correctly within natural language. We present KG-prover, a novel framework that leverages knowledge graphs mined from reputable mathematical texts to augment general-purpose LLMs to construct and formalize mathematical proofs. We also study the effects of scaling graph-based, test-time compute using KG-Prover, demonstrating significant performance improvements over baselines across multiple datasets. General-purpose LLMs improve up to 21\% on miniF2F-test when combined with KG-Prover, with consistent improvements ranging from 2-11\% on the ProofNet, miniF2F-test, and MUSTARD datasets without additional scaling. Furthermore, KG-Prover with o4-mini achieves over 50% miniF2F-test. This work provides a promising approach for augmenting natural language proof reasoning with knowledge graphs without the need for additional finetuning.
• Abstract（参考訳）: 大規模言語モデルは、自動定理証明のような多段階論理推論能力を必要とする自然言語処理タスクにおいて顕著な能力を示した。 しかし、重要な数学的概念の同定、それらの相互関係の理解、自然言語内での証明の正しい形式化など、定理の証明には課題が持続する。 提案するKG-proverは,計算可能な数学的テキストから抽出した知識グラフを利用して汎用LLMを増強し,数学的証明の構築と形式化を行う新しいフレームワークである。 また、KG-Proverを用いてグラフベースのテストタイム計算をスケールすることの効果について検討し、複数のデータセットをまたいだベースラインよりも大幅な性能向上を示す。 汎用LLMは、KG-Proverと組み合わせた場合、miniF2F-testで21\%改善され、ProofNetで2-11\%、miniF2F-test、MUSTARDデータセットで追加スケーリングなしで一貫した改善が加えられた。 さらに、o4-miniのKG-Proverは50%以上のミニF2Fテストを達成する。 この研究は、追加の微調整を必要とせず、知識グラフによる推論を自然言語で証明するための有望なアプローチを提供する。

関連論文リスト

• Proof-RM: A Scalable and Generalizable Reward Model for Math Proof [67.53066972145183]
  大規模言語モデル(LLM)は,*検証リワード*(RLVR)を用いた強化学習を通じて,強力な数学推論能力を示した。 多くの先進的な数学的問題は証明ベースであり、単純な解マッチングによって証明の真性を決定するための保証された方法はない。 自動検証を実現するには、完全な証明プロセスを確実に評価できるリワードモデル(RM)が必要である。
  論文  参考訳（メタデータ） (2026-02-02T17:42:53Z)
• Evaluating Frontier LLMs on PhD-Level Mathematical Reasoning: A Benchmark on a Textbook in Theoretical Computer Science about Randomized Algorithms [14.853721511192736]
  大規模言語モデル(LLM)は、自動数学的推論と科学的発見の突破口となった。 GP-5-Thinking、Gemini-3-Pro、Claude-Sonnet-4.5-Thinking、Grok-4の4つのフロンティアモデルのベンチマークを示す。 上位モデルの精度は高いが,他のモデルでは一貫性が著しく低下していることがわかった。
  論文  参考訳（メタデータ） (2025-12-16T00:34:55Z)
• DeepSeekMath-V2: Towards Self-Verifiable Mathematical Reasoning [26.142347272743496]
  正しい答えは正しい推論を保証するものではない。 深い推論の限界を推し進めるためには、数学的推論の包括性と厳密さを検証する必要があると信じている。 我々のモデルであるDeepSeekMath-V2は、IMO 2025とCMO 2024のゴールドレベルスコア、Patnam 2024のほぼ完璧な118/120のスケールされたテストタイム計算を達成し、強力な定理証明能力を示す。
  論文  参考訳（メタデータ） (2025-11-27T16:01:22Z)
• DRIFT: Decompose, Retrieve, Illustrate, then Formalize Theorems [14.568293842955065]
  DRIFTは、非公式な数学的ステートメントをより小さく、より扱いやすい'サブコンポーネント'に分解するフレームワークである。 これは、モデルが形式化タスクにおいてより効果的に前提を使用するのを助けるために、イラストラティブな定理を回収する。 我々は,様々なベンチマーク(ProofNet,ConNF,MiniF2F-test)でDRIFTを評価し,前提条件の検索を継続的に改善することを発見した。
  論文  参考訳（メタデータ） (2025-10-12T21:42:04Z)
• Enrich-on-Graph: Query-Graph Alignment for Complex Reasoning with LLM Enriching [61.824094419641575]
  大言語モデル(LLM)は知識グラフ質問応答(KGQA)のような知識集約的なシナリオにおける幻覚と事実的誤りに苦しむ これは、構造化知識グラフ(KG)と非構造化クエリのセマンティックギャップによるもので、その焦点や構造に固有の違いが原因である。 既存の手法は通常、バニラKGの資源集約的で非スケーリング可能な推論を用いるが、このギャップを見落としている。 我々は、LLMの事前知識を活用してKGを充実させる柔軟なフレームワークEnrich-on-Graph(EoG)を提案し、グラフとクエリ間のセマンティックギャップを埋める。
  論文  参考訳（メタデータ） (2025-09-25T06:48:52Z)
• Generating Millions Of Lean Theorems With Proofs By Exploring State Transition Graphs [6.65877320351217]
  我々はLeanNavigatorを開発した。これはリーンの定理と証明の大規模なデータセットを生成する新しい方法だ。 我々は10億のトークンを合計470万の定理で生成し、以前のデータセットを桁違いに上回った。 この広範なデータセットを使用して、我々は、定理証明タスクにおいて最先端のReProverモデルより優れたAIモデルを訓練した。
  論文  参考訳（メタデータ） (2025-02-16T06:20:39Z)
• Alchemy: Amplifying Theorem-Proving Capability through Symbolic Mutation [71.32761934724867]
  この研究は、記号的突然変異を通じて形式的な定理を構成するデータ合成のフレームワークであるAlchemyを提案する。 マドリブにおける各候補定理について、書き直しや適用に使用できるすべてのイベーシブルな定理を同定する。 その結果、マドリブの定理の数は110kから6Mへと桁違いに増加する。
  論文  参考訳（メタデータ） (2024-10-21T08:04:21Z)
• LLM Critics Help Catch Bugs in Mathematics: Towards a Better Mathematical Verifier with Natural Language Feedback [71.95402654982095]
  本研究では,自然言語フィードバック型検証器Math-Minosを提案する。 実験の結果,少量の自然言語フィードバックが検証器の性能を大幅に向上させることがわかった。
  論文  参考訳（メタデータ） (2024-06-20T06:42:27Z)
• MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data [85.50740598523818]
  MUSTARDは、高品質で多様性のある定理と証明データの均一な合成をマスターするフレームワークである。 5,866個の有効なデータポイントを持つMUSTARDSAUCEベンチマークを示す。 我々は広範囲な解析を行い、MUSTARDが検証された高品質なステップバイステップデータを生成することを示す。
  論文  参考訳（メタデータ） (2024-02-14T05:57:58Z)
• Enhancing Neural Theorem Proving through Data Augmentation and Dynamic Sampling Method [1.8130068086063336]
  本稿では,定理証明のための新しい動的サンプリング手法であるDS-Proverを紹介する。 単純化と書き直しの戦術を複数の前提で1つの前提で戦術に分解することで、トレーニングデータセットを強化します。 ProofNetデータセットでは14.2%の最先端パフォーマンス(Pass@1)、MiniF2Fでは29.8%のパフォーマンスを実現しています。
  論文  参考訳（メタデータ） (2023-12-20T09:55:21Z)
• TRIGO: Benchmarking Formal Mathematical Proof Reduction for Generative Language Models [68.65075559137608]
  本稿では, ATP ベンチマーク TRIGO を提案する。このベンチマークでは, ステップバイステップの証明で三角法式を縮小するだけでなく, 論理式上で生成する LM の推論能力を評価する。 我々は、Webから三角法式とその縮小フォームを収集し、手作業で単純化プロセスに注釈を付け、それをリーン形式言語システムに翻訳する。 我々はLean-Gymに基づく自動生成装置を開発し、モデルの一般化能力を徹底的に分析するために、様々な困難と分布のデータセット分割を作成する。
  論文  参考訳（メタデータ） (2023-10-16T08:42:39Z)
• Lila: A Unified Benchmark for Mathematical Reasoning [59.97570380432861]
  LILAは、23の多様なタスクと4次元からなる統一的な数学的推論ベンチマークである。 我々は,Pythonプログラムの形式でタスク命令とソリューションを収集することにより,20のデータセットベンチマークを拡張してベンチマークを構築した。 LILAで訓練された汎用数学的推論モデルであるBHASKARAを紹介する。
  論文  参考訳（メタデータ） (2022-10-31T17:41:26Z)
• Proof Artifact Co-training for Theorem Proving with Language Models [4.934817254755007]
  PACT(bf Proof bf Artifact bf Co-bf Training)は、カーネルレベルのコトレーニング用証明項から自己教師付きデータを抽出する一般的な手法である。 我々は、Transformer言語モデルによって駆動されるニューラル定理証明器でリーンを計測し、PACTがテスト定理の保留組における成功率を証明する定理を32%から48%に改善することを示す。
  論文  参考訳（メタデータ） (2021-02-11T18:59:24Z)
• Generative Language Modeling for Automated Theorem Proving [94.01137612934842]
  この研究は、自動定理プロバーの人間に対する大きな制限が言語モデルから生成することで対処できる可能性によって動機づけられている。 本稿ではメタマス形式化言語のための自動証明と証明アシスタント GPT-f を提案し,その性能を解析する。
  論文  参考訳（メタデータ） (2020-09-07T19:50:10Z)

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

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