論文の概要: ProofEvolve: Neuro-Symbolic Evolution for Formal Automated Theorem Proving
- arxiv url: http://arxiv.org/abs/2608.26334v1
- Date: Wed, 26 Aug 2026 19:15:27 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-08-28 16:30:58.161505
- Title: ProofEvolve: Neuro-Symbolic Evolution for Formal Automated Theorem Proving
- Title（参考訳）: ProofEvolve: 形式的自動定理証明のための神経・筋肉の進化
- Abstract要約: 本稿では, 明示的, 正式に証明された記号的証明構造を進化させる, ニューロシンボリック・フレームワークProofEvolveを提案する。
それぞれの問題の中でProofEvolveは、振る舞いインデックス付きアーカイブで部分的なAND-OR証明DAGを進化させる。
この進化過程は不完全な試みから検証結果を保存し、後の証明に利用できるようにする。
- 参考スコア（独自算出の注目度）: 31.00212239114582
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Automated theorem proving offers a natural foundation for recursive self-improvement in scientific discovery. However, existing neural provers do not fully preserve this recursive structure, where the learning process should be self-improving over time. Existing methods either embed proof experience into model parameters through expensive weight updates, or keep verified intermediate deductions only within the current problem. In addition, these methods also heavily rely on sparse whole-proof feedback, even when unsuccessful partial attempts contain useful discoveries. To close the gap, we propose ProofEvolve, a neuro-symbolic framework that evolves explicit, formally verified symbolic proof structures with neural models to decisively expand the knowledge boundary. In this framework, the neural model proposes variation operators, including decompositions, repairs, and schema recombinations. The symbolic Lean kernel verifies every proof transition. Over the evolution loops, ProofEvolve computes verified closure over the resulting proof directed acyclic graphs (DAGs). Within each problem, ProofEvolve evolves partial AND-OR proof DAGs in a behaviorally indexed archive. Across problems, kernel-checked schema extraction adds newly proved sub-DAGs to a persistent schema library. Proof DAGs inherit the solved results through typed schema recombination, with every residual premise exposed as a new subgoal. This evolutionary process preserves verified results from incomplete attempts and makes them available for later proofs without weakening formal soundness. Across three competition-level Lean benchmarks, ProofEvolve achieves the highest average solve rate among the evaluated proof systems.
- Abstract（参考訳）: 自動定理証明は、科学的発見における再帰的な自己改善の自然な基礎を提供する。
しかし、既存のニューラル・プローバーは、学習プロセスが時間とともに自己改善されるべきであるこの再帰的構造を完全に保存していない。
既存の手法は、高価な重み付け更新を通じてモデルパラメータに証明経験を埋め込むか、現在の問題に限って検証された中間減算を保持するかのどちらかである。
さらにこれらの手法は、部分的な試みが失敗したとしても、スパース全体のフィードバックに大きく依存する。
このギャップを埋めるために,ニューラルネットワークを用いた明示的で正式に証明された記号的証明構造を進化させ,知識境界を決定的に拡張するProofEvolveを提案する。
このフレームワークでは、ニューラルネットワークは、分解、修復、スキーマの再結合を含む変動演算子を提案する。
シンボリックなLeanカーネルは、すべての証明遷移を検証する。
進化ループの間、ProofEvolve は証明された証明非巡回グラフ (DAG) の閉包を計算する。
それぞれの問題の中でProofEvolveは、振る舞いインデックス付きアーカイブで部分的なAND-OR証明DAGを進化させる。
問題全体では、カーネルチェックされたスキーマ抽出は、新しい証明されたサブDAGを永続的なスキーマライブラリに追加する。
Proof DAGは、すべての残留前提が新しいサブゴールとして公開され、型付けされたスキーマ再結合によって解決された結果を継承する。
この進化過程は不完全な試みによる検証結果を保存し、形式的な健全性を弱めることなく後の証明に利用できるようにする。
ProofEvolveは、競争レベルの3つのリーンベンチマークの中で、評価された証明システムの中で、最も高い平均的な問題解決率を達成する。
関連論文リスト
- Influence-Guided Symbolic Regression: Scientific Discovery via LLM-Driven Equation Search with Granular Feedback [56.69850045068714]
逐次的2段階プロセスとして方程式発見をフレーム化する方法である textitInfluence-Guided Regression (IGSR) を導入する。
LLM-SRBench, 薬理学的PKPDモデル, 疫学シミュレーション, 実世界のゲノムデータなど, IGSRの有効性を示す。
論文 参考訳（メタデータ） (2026-05-27T23:48:01Z) - FormalEvolve: Neuro-Symbolic Evolutionary Search for Diverse and Prover-Effective Autoformalization [7.641987396532518]
我々は、意味的に一貫性のあるレパートリーの予算付きテストタイム検索として、オートフォーマル化を定式化する。
本稿では,コンパイル型ニューロシンボリック進化フレームワークであるFormalEvolveを提案する。
CombiBenchとProofNetでは、FormalEvolveは58.0%と84.9%のセマンティックヒット率(SH@100)に達し、セマンティック成功のクロスプロブレム濃度を低下させる。
論文 参考訳（メタデータ） (2026-03-20T10:14:00Z) - Simulating Evolvability as a Learning Algorithm: Empirical Investigations on Distribution Sensitivity, Robustness, and Constraint Tradeoffs [0.0]
進化可能性の理論は、ラベル付き例や構造知識なしで動作する制約付き学習アルゴリズムとして進化を定式化する。
本研究では,ヴァリアントのモデルを忠実にシミュレートする遺伝的アルゴリズムを実装し,ブール関数のクラスをまたいだ実験を行う。
以上の結果から,中間次元における急激なパフォーマンス低下が明らかとなり,フィットネスプラトーの脱落に中性変異が不可欠であることが明らかとなった。
論文 参考訳（メタデータ） (2025-07-24T04:32:31Z) - ProofNet++: A Neuro-Symbolic System for Formal Proof Verification with Self-Correction [0.0]
本稿では,自動定理証明を強化するニューロシンボリックフレームワークProofNet++を提案する。
ProofNet++は,従来のモデルよりも検証精度,正確性,形式的妥当性を著しく向上することを示す。
論文 参考訳（メタデータ） (2025-05-30T05:44:34Z) - LeanProgress: Guiding Search for Neural Theorem Proving via Proof Progress Prediction [74.79306773878955]
証明の進捗を予測する手法であるLeanProgressを紹介します。
実験の結果、LeanProgressは全体の予測精度が75.1%に達することがわかった。
論文 参考訳（メタデータ） (2025-02-25T07:46:36Z) - Reward-Guided Iterative Refinement in Diffusion Models at Test-Time with Applications to Protein and DNA Design [87.58981407469977]
進化的アルゴリズムにインスパイアされた拡散モデルを用いた推論時間報酬最適化のための新しいフレームワークを提案する。
当社のアプローチでは,各イテレーションにおける2つのステップ – ノイズ発生と報酬誘導という,反復的な改善プロセスを採用しています。
論文 参考訳（メタデータ） (2025-02-20T17:48:45Z) - Rao-Blackwell Gradient Estimators for Equivariant Denoising Diffusion [55.95767828747407]
分子やタンパク質の生成のようなドメインでは、物理系はモデルにとって重要な固有の対称性を示す。
学習のばらつきを低減し、確率的に低い分散勾配推定器を提供するフレームワークを提案する。
また,軌道拡散法(Orbit Diffusion)と呼ばれる手法を用いて,損失とサンプリングの手順を取り入れた推定器の実用的実装を提案する。
論文 参考訳（メタデータ） (2025-02-14T03:26:57Z) - Data-Driven Abstractions via Binary-Tree Gaussian Processes for Formal Verification [0.22499166814992438]
ガウス過程(GP)回帰に基づく抽象的解は、量子化された誤差を持つデータから潜在システムの表現を学習する能力で人気を博している。
二分木ガウス過程(BTGP)により未知系のマルコフ連鎖モデルを構築することができることを示す。
BTGPの関数空間に真の力学が存在しない場合でも、統一公式による非局在誤差量子化を提供する。
論文 参考訳（メタデータ） (2024-07-15T11:49:44Z) - Consistency of Neural Causal Partial Identification [17.503562318576414]
因果モデル(Causal Models)の最近の進歩は、因果効果の同定と部分的同定が神経生成モデルによって自動的に行われるかを示した。
連続変数とカテゴリー変数の両方を持つ一般設定において、NCMによる部分的識別の整合性を証明する。
結果は、深さと接続性の観点から、基盤となるニューラルネットワークアーキテクチャの設計の影響を強調している。
論文 参考訳（メタデータ） (2024-05-24T16:12:39Z) - Proving Theorems Recursively [80.42431358105482]
本稿では、定理をレベル・バイ・レベルで証明するPOETRYを提案する。
従来のステップバイステップメソッドとは異なり、POETRYは各レベルで証明のスケッチを検索する。
また,POETRYが検出した最大証明長は10～26。
論文 参考訳（メタデータ） (2024-05-23T10:35:08Z) - DynGFN: Towards Bayesian Inference of Gene Regulatory Networks with
GFlowNets [81.75973217676986]
遺伝子調節ネットワーク(GRN)は、遺伝子発現と細胞機能を制御する遺伝子とその産物間の相互作用を記述する。
既存の方法は、チャレンジ(1)、ダイナミックスから循環構造を識別すること、あるいはチャレンジ(2)、DAGよりも複雑なベイズ後部を学習することに焦点を当てるが、両方ではない。
本稿では、RNAベロシティ技術を用いて遺伝子発現の「速度」を推定できるという事実を活用し、両方の課題に対処するアプローチを開発する。
論文 参考訳（メタデータ） (2023-02-08T16:36:40Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。