論文の概要: On Reasoning-Centric LLM-based Automated Theorem Proving

• arxiv url: http://arxiv.org/abs/2604.19558v1
• Date: Tue, 21 Apr 2026 15:11:42 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-04-22 22:41:49.835542
• Title: On Reasoning-Centric LLM-based Automated Theorem Proving
• Title（参考訳）: 推論中心LLMに基づく自動定理証明について
• Authors: Yican Sun, Chengwei Shi, Hangzhou Lyu, Yingfei Xiong,
• Abstract要約: 本稿では,Rocq の推論中心の証明エージェント ReCent-Prover を紹介する。 ReCent-Proverは、過去の最先端技術よりも証明された定理の数において相対的に22.58%向上していることを示す。
• 参考スコア（独自算出の注目度）: 1.8002666661892468
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Automated theorem proving is fundamental to formal methods, and the recent trend is to integrate large language models (LLMs) and proof assistants to form effective proof agents. While existing proof agents show promising performance, they inadequately leverage reasoning capabilities of modern LLMs in high-level planning and self-critique. We argue that proof agents should not merely generate tactics but also reason strategically about proof plans and critically evaluate their own proposals. This paper introduces ReCent-Prover, a reasoning-centric LLM-based proof agent for Rocq that addresses two critical limitations in current systems. First, we present validation with reflection, enabling LLMs to scrutinize their generated tactics and synthesize failure summaries when reflection identifies potential errors, filtering out potentially misapplied tactics earlier. Second, we propose retrieval with planning, which conditions retrieval on LLM-generated proof plans rather than subgoal similarity, retrieving lemmas and proofs that align with the anticipated proof strategy. Both techniques increase the number of invocations of LLMs. However, when evaluated on the CoqStoq benchmark, even under the same budget of LLM invocations, ReCent-Prover achieves a 22.58% relative improvement in the number of proved theorems over the previous state-of-the-art, demonstrating that our reasoning-centric design significantly enhances automated theorem proving capabilities.
• Abstract（参考訳）: 自動定理証明は形式的手法の基本であり、近年のトレンドは、大きな言語モデル(LLM)と証明アシスタントを統合して効果的な証明エージェントを形成することである。 既存の証明エージェントは有望な性能を示すが、高いレベルの計画と自己批判において、現代のLLMの推論能力は不十分である。 証明エージェントは単に戦術を生成するだけでなく、証明計画について戦略的に判断し、彼らの提案を批判的に評価するべきだと我々は主張する。 本稿では,現在のシステムにおける2つの限界に対処する論理型LLMに基づくRocqの証明エージェントであるReCent-Proverを紹介する。 まず、リフレクションによる検証を行い、LLMが生成した戦術を精査し、リフレクションが潜在的なエラーを識別した場合に失敗サマリーを合成し、潜在的に悪用された戦術を早期にフィルタリングできるようにする。 第2に,LLM 生成した証明計画の条件をサブゴナルな類似性ではなく,予測された証明戦略と整合した補題と証明を検索する計画付き検索を提案する。 どちらの手法もLLMの呼び出し数を増加させる。 しかし、コクストックベンチマークで評価すると、LLMの実行と同じ予算の下でも、ReCent-Proverは従来の最先端技術よりも証明された定理の数に対して相対的に22.58%向上し、我々の推論中心の設計が自動定理証明能力を著しく向上させることを示した。

関連論文リスト

• PROMISE: Proof Automation as Structural Imitation of Human Reasoning [15.113069562646302]
  ProMISEは,証明状態遷移に対するステートフルな探索として,証明生成を再構成する構造認識フレームワークである。 複数のLLMバックエンドにまたがるSEL4ベンチマークのPROMISEを評価し,SeleneやRangoといった先行システムと比較した。
  論文  参考訳（メタデータ） (2026-04-07T03:49:12Z)
• On Multi-Step Theorem Prediction via Non-Parametric Structural Priors [50.16583672681106]
  本研究では,インコンテキスト学習(ICL)のレンズによる学習自由な定理予測について検討する。 本稿では,過去の解の時間的依存関係を有向グラフとしてエンコードし,推論中に探索空間を効果的に引き起こす明示的なトポロジ的制約を課すTheorem Precedence Graphsを提案する。 FormalGeo7kベンチマークの実験から,本手法は89.29%の精度を実現し,ICLベースラインを著しく上回り,最先端の教師付きモデルに適合することがわかった。
  論文  参考訳（メタデータ） (2026-03-05T06:08:50Z)
• A State-Transition Framework for Efficient LLM Reasoning [58.18141262230392]
  ロングチェイン・オブ・ソート (Long Chain-of-Thought, CoT) 推論は、複雑な推論タスクにおいて、Large Language Models (LLM) のパフォーマンスを大幅に改善する。 既存の研究は通常、COT配列を圧縮することでLCMの推論効率を高める。 状態遷移過程としてLLMの推論過程をモデル化する効率的な推論フレームワークを提案する。
  論文  参考訳（メタデータ） (2026-02-01T12:40:40Z)
• Implicit Reasoning in Large Language Models: A Comprehensive Survey [67.53966514728383]
  大規模言語モデル(LLM)は、幅広いタスクにまたがる強力な一般化を実証している。 最近の研究は、暗黙の推論に拍車をかけた、明示的な思考の連鎖から注意を向けている。 本調査では,表現形式から計算戦略へ焦点を移し,実行パラダイムを中心とした分類を紹介した。
  論文  参考訳（メタデータ） (2025-09-02T14:16:02Z)
• Revisiting LLM Reasoning via Information Bottleneck [57.519119962528166]
  大規模言語モデル(LLM)は、最近、検証可能な報酬付き強化学習(RLVR)を通じて推論能力の顕著な進歩を示した。 本稿では,情報ボトルネック(IB)の原理に基づくLLM推論の理論的特徴について述べる。 IB対応推論最適化(IBRO)を提案する。
  論文  参考訳（メタデータ） (2025-07-24T13:14:25Z)
• Towards Advanced Mathematical Reasoning for LLMs via First-Order Logic Theorem Proving [14.569345246475509]
  大規模言語モデル(LLM)は、有望な一階述語論理(FOL)推論能力を示している。 しかし、多段階のFOL還元を含む複雑な数学的推論におけるそれらの効果はいまだ研究されていない。 LLMの生成戦略の多様性と再現性を向上する自己適応型ソリューションであるDREAMを提案する。
  論文  参考訳（メタデータ） (2025-06-20T16:09:56Z)
• Are LLMs Rigorous Logical Reasoners? Empowering Natural Language Proof Generation by Stepwise Decoding with Contrastive Learning [14.718645333008332]
  近年の大規模言語モデルの進歩は、自然言語の証明計画に大きな進歩をもたらした。 本稿では, 逆学習による段階的復号化手法を提案し, 発電機の復号処理中に発生する2つの一般的な誤りに対処する。
  論文  参考訳（メタデータ） (2023-11-12T05:12:49Z)
• Faithful Explanations of Black-box NLP Models Using LLM-generated Counterfactuals [67.64770842323966]
  NLPシステムの予測に関する因果的説明は、安全性を確保し、信頼を確立するために不可欠である。 既存の手法は、しばしばモデル予測を効果的または効率的に説明できない。 本稿では, 対物近似(CF)の2つの手法を提案する。
  論文  参考訳（メタデータ） (2023-10-01T07:31:04Z)

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

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