論文の概要: ProofNet++: A Neuro-Symbolic System for Formal Proof Verification with Self-Correction

• arxiv url: http://arxiv.org/abs/2505.24230v1
• Date: Fri, 30 May 2025 05:44:34 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-06-02 19:47:52.786151
• Title: ProofNet++: A Neuro-Symbolic System for Formal Proof Verification with Self-Correction
• Title（参考訳）: ProofNet++:自己補正による形式的証明のためのニューロシンボリックシステム
• Authors: Murari Ambati,
• Abstract要約: 本稿では,自動定理証明を強化するニューロシンボリックフレームワークProofNet++を提案する。 ProofNet++は,従来のモデルよりも検証精度,正確性,形式的妥当性を著しく向上することを示す。
• 参考スコア（独自算出の注目度）: 0.0
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: We propose ProofNet++, a neuro-symbolic framework that enhances automated theorem proving by combining large language models (LLMs) with formal proof verification and self-correction mechanisms. Current LLM-based systems suffer from hallucinated logical steps and unverifiable reasoning. ProofNet++ mitigates these limitations by integrating symbolic proof tree supervision, a reinforcement learning loop using verifiers as reward functions, and an iterative self-correction module. Our experiments on miniF2F, Lean's mathlib, and HOL Light show that ProofNet++ significantly improves proof accuracy, correctness, and formal verifiability over prior models. We provide theoretical analysis of the convergence and stability of the verifier-guided RL framework and release our datasets and codebase for future research.
• Abstract（参考訳）: 本稿では,大言語モデル(LLM)と形式的証明検証,自己訂正機構を組み合わせることで,自動定理証明を強化するニューロシンボリックフレームワークProofNet++を提案する。 現在のLLMベースのシステムは、幻覚的な論理ステップと検証不可能な推論に悩まされている。 ProofNet++は、これらの制限を、象徴的な証明ツリーの監督、検証を報酬関数として使用する強化学習ループ、反復的な自己訂正モジュールを統合することで緩和する。 MiniF2F、Lean's Mathlib、HOL Lightの実験から、ProofNet++は事前モデルよりも証明精度、正確性、形式的妥当性を著しく向上することが示された。 本稿では,検証対象のRLフレームワークの収束と安定性に関する理論的解析を行い,今後の研究のためのデータセットとコードベースをリリースする。

関連論文リスト

• Lean-STaR: Learning to Interleave Thinking and Proving [53.923617816215774]
  証明の各ステップに先立って,非公式な思考を生成するために,言語モデルをトレーニングするフレームワークであるLean-STaRを紹介します。 Lean-STaRは、Lean定理証明環境内のminiF2F-testベンチマークで最先端の結果を達成する。
  論文  参考訳（メタデータ） (2024-07-14T01:43:07Z)
• Neuro-Symbolic Integration Brings Causal and Reliable Reasoning Proofs [95.07757789781213]
  LLMの複雑な推論には2行のアプローチが採用されている。 1行の作業は様々な推論構造を持つLLMを誘導し、構造出力は自然に中間推論ステップと見なすことができる。 他方の行では、LCMのない宣言的解法を用いて推論処理を行い、推論精度は向上するが、解法のブラックボックスの性質により解釈性に欠ける。 具体的には,Prologインタプリタが生成した中間検索ログにアクセスし,人間可読推論に解釈可能であることを示す。
  論文  参考訳（メタデータ） (2023-11-16T11:26:21Z)

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

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