Fugu-MT 論文翻訳(概要): ProofNet++: A Neuro-Symbolic System for Formal Proof Verification with Self-Correction

論文の概要: 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フレームワークの収束と安定性に関する理論的解析を行い,今後の研究のためのデータセットとコードベースをリリースする。

関連論文リスト

VerIF: Verification Engineering for Reinforcement Learning in Instruction Following [55.60192044049083]
検証可能な報酬(RLVR)による強化学習は、大規模言語モデル(LLM)の強化の鍵となる技術となっている。ルールベースのコード検証とLLMベースの大規模な推論モデルによる検証を組み合わせた検証手法であるVerIFを提案する。我々はVerIFを用いたRLトレーニングを2つのモデルに適用し、いくつかの代表的な命令追従ベンチマークで大幅に改善した。
論文参考訳（メタデータ） (2025-06-11T17:10:36Z)
Abstraction-Based Proof Production in Formal Verification of Neural Networks [0.7048747239308888]
本稿では,抽象的検証を実証する新しいフレームワークを提案する。この作業は、共通の抽象化技術をサポートすることにより、スケーラブルで信頼性の高い検証を可能にすることを目的としている。
論文参考訳（メタデータ） (2025-06-11T07:00:09Z)
Towards Reliable Proof Generation with LLMs: A Neuro-Symbolic Approach [14.213719696233934]
大型言語モデル(LLM)は厳密な論理的推論と記号的推論を必要とする形式的ドメインと競合する。本稿では,LLMの生成強度と構造成分を組み合わせ,この課題を克服するニューロシンボリックアプローチを提案する。
論文参考訳（メタデータ） (2025-05-20T15:13:32Z)
Can Large Language Models Learn Formal Logic? A Data-Driven Training and Evaluation Framework [2.9334627971166336]
本稿では,大規模言語モデル(LLM)の論理的推論能力について検討する。訓練されたLLMは、一連の仮定とゴールを入力として受け取り、その仮定からゴールを正式に導出する証明を出力として生成する。トレーニングにとって重要な障害は、現実世界の証明が不足していることだ。
論文参考訳（メタデータ） (2025-04-28T19:25:29Z)
LeanProgress: Guiding Search for Neural Theorem Proving via Proof Progress Prediction [74.79306773878955]
証明の進捗を予測する手法であるLeanProgressを紹介します。実験の結果、LeanProgressは全体の予測精度が75.1%に達することがわかった。
論文参考訳（メタデータ） (2025-02-25T07:46:36Z)
Automated Proof Generation for Rust Code via Self-Evolution [69.25795662658356]
私たちは、Rustコードの自動証明生成を可能にする、人書きスニペットの欠如を克服するフレームワークであるSAFEを紹介します。 SAFEは、細調整されたモデルの自己老化能力を訓練するために、多数の合成不正確な証明を再利用する。我々は、人間の専門家によるベンチマークで52.52%の精度で達成し、GPT-4oのパフォーマンス14.39%を大きく上回った。
論文参考訳（メタデータ） (2024-10-21T08:15:45Z)
Lean-STaR: Learning to Interleave Thinking and Proving [53.923617816215774]
証明の各ステップに先立って,非公式な思考を生成するために,言語モデルをトレーニングするフレームワークであるLean-STaRを紹介します。 Lean-STaRは、Lean定理証明環境内のminiF2F-testベンチマークで最先端の結果を達成する。
論文参考訳（メタデータ） (2024-07-14T01:43:07Z)
Improving Autoformalization using Type Checking [15.58948808529849]
我々は、現在の自己形式化手法とそれらの評価に使用されるプロセスの両方を分析し、特にLean 4の定理証明言語に注目します。 ProofNetの絶対精度は18.4%まで向上し,既存の手法上での自己整合性による型チェックフィルタリングが性能を著しく向上することを示した。我々はまた、新しい研究レベルの数学データセット RLM25、修正されたProofNet、ラベル付き正誤オートフォーマライゼーションペアでメトリクスを評価するProofNetVerifといった新しいベンチマークもリリースした。
論文参考訳（メタデータ） (2024-06-11T13:01:50Z)
Neuro-Symbolic Integration Brings Causal and Reliable Reasoning Proofs [95.07757789781213]
LLMの複雑な推論には2行のアプローチが採用されている。 1行の作業は様々な推論構造を持つLLMを誘導し、構造出力は自然に中間推論ステップと見なすことができる。他方の行では、LCMのない宣言的解法を用いて推論処理を行い、推論精度は向上するが、解法のブラックボックスの性質により解釈性に欠ける。具体的には,Prologインタプリタが生成した中間検索ログにアクセスし,人間可読推論に解釈可能であることを示す。
論文参考訳（メタデータ） (2023-11-16T11:26:21Z)
Distributional Inclusion Hypothesis and Quantifications: Probing for Hypernymy in Functional Distributional Semantics [50.363809539842386]
関数分布意味論(FDS)は、真理条件関数による単語の意味をモデル化する。 FDSモデルは分布包含仮説(DIH)に厳格に従う制限されたコーパスのクラスでハイパーネミーを学ぶことを示す。
論文参考訳（メタデータ） (2023-09-15T11:28:52Z)
LeanDojo: Theorem Proving with Retrieval-Augmented Language Models [72.54339382005732]
大規模言語モデル(LLM)は、Leanのような証明アシスタントを使って形式的な定理を証明することを約束している。既存のメソッドは、プライベートコード、データ、計算要求のために、複製や構築が難しい。本稿では、ツールキット、データ、モデルからなるオープンソースのリーンツールキットであるLeanDojoを紹介します。本研究では,LLM ベースの証明器 ReProver を開発した。
論文参考訳（メタデータ） (2023-06-27T17:05:32Z)

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