論文の概要: Stepwise: Neuro-Symbolic Proof Search for Automated Systems Verification
- arxiv url: http://arxiv.org/abs/2603.19715v1
- Date: Fri, 20 Mar 2026 07:45:49 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-03-23 19:48:39.044626
- Title: Stepwise: Neuro-Symbolic Proof Search for Automated Systems Verification
- Title（参考訳）: ステップワイズ:自動システム検証のためのニューロシンボリック証明探索
- Abstract要約: 本稿では,システムレベルの検証プロジェクトの証明検索の自動化を目的とした,ニューロシンボリックな証明生成フレームワークを提案する。
このフレームワークは、証明状態に対して最優先のツリー探索を行い、次の候補証明ステップのためにLLMを何度もクエリする。
さらなるベンチマークの結果は強力な一般化を示し、スケーラブルな自動ソフトウェア検証への道のりを示している。
- 参考スコア（独自算出の注目度）: 21.423111823947867
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Formal verification via interactive theorem proving is increasingly used to ensure the correctness of critical systems, yet constructing large proof scripts remains highly manual and limits scalability. Advances in large language models (LLMs), especially in mathematical reasoning, make their integration into software verification increasingly promising. This paper introduces a neuro-symbolic proof generation framework designed to automate proof search for systems-level verification projects. The framework performs a best-first tree search over proof states, repeatedly querying an LLM for the next candidate proof step. On the neural side, we fine-tune LLMs using datasets of proof state-step pairs; on the symbolic side, we incorporate a range of ITP tools to repair rejected steps, filter and rank proof states, and automatically discharge subgoals when search progress stalls. This synergy enables data-efficient LLM adaptation and semantics-informed pruning of the search space. We implement the framework on a new Isabelle REPL that exposes fine-grained proof states and automation tools, and evaluate it on the FVEL seL4 benchmark and additional Isabelle developments. On seL4, the system proves up to 77.6\% of the theorems, substantially surpassing previous LLM-based approaches and standalone Sledgehammer, while solving significantly more multi-step proofs. Results across further benchmarks demonstrate strong generalization, indicating a viable path toward scalable automated software verification.
- Abstract（参考訳）: 対話的定理証明による形式的検証は、重要なシステムの正当性を保証するためにますます利用されているが、大きな証明スクリプトの構築は手作業で行われ、スケーラビリティが制限されている。
大規模言語モデル(LLM)の進歩は、特に数学的推論において、ソフトウェア検証への統合をますます有望なものにしている。
本稿では,システムレベルの検証プロジェクトの証明検索の自動化を目的とした,ニューロシンボリックな証明生成フレームワークを提案する。
このフレームワークは、証明状態に対して最優先のツリー探索を行い、次の候補証明ステップのためにLLMを何度もクエリする。
ニューラル側では,証明状態-ステップペアのデータセットを用いて微調整し,シンボル側では,削除されたステップの修復やフィルタ,証明状態のランク付け,探索進行が停止した場合のサブゴールの自動排出など,様々なITPツールを組み込んだ。
このシナジーにより、データ効率のよいLLM適応とセマンティックスインフォームドプルーニングが可能となる。
我々は,Isabelle REPLにフレームワークを実装し,詳細な証明状態と自動化ツールを公開し,FVEL seL4ベンチマークと追加のIsabelle開発で評価する。
seL4 では、定理の77.6 %までを証明し、従来の LLM ベースのアプローチやスタンドアローンの Sledgehammer をはるかに上回り、さらに多段階の証明を解く。
さらなるベンチマークの結果は強力な一般化を示し、スケーラブルな自動ソフトウェア検証への道のりを示している。
関連論文リスト
- LLM-as-a-Verifier: A General-Purpose Verification Framework [74.40111651545979]
本稿では,汎用検証フレームワーク LLM-as-a-Verifier を紹介する。
追加のトレーニングを必要とせずに、エージェントタスクに対してきめ細かいフィードバックを提供する。
いくつかのベンチマークで最先端のパフォーマンスを達成する。
論文 参考訳（メタデータ） (2026-07-06T17:59:35Z) - PROMISE: Proof Automation as Structural Imitation of Human Reasoning [15.113069562646302]
ProMISEは,証明状態遷移に対するステートフルな探索として,証明生成を再構成する構造認識フレームワークである。
複数のLLMバックエンドにまたがるSEL4ベンチマークのPROMISEを評価し,SeleneやRangoといった先行システムと比較した。
論文 参考訳（メタデータ） (2026-04-07T03:49:12Z) - WybeCoder: Verified Imperative Code Generation [22.401681809856896]
WybeCoderはエージェントコード検証フレームワークである。
コード、不変性、そして証明が共進化する所で、証明・アズ・ユー・ジェネレーション開発を可能にする。
論文 参考訳（メタデータ） (2026-03-31T00:06:44Z) - DiffuRank: Effective Document Reranking with Diffusion Language Models [71.16830004674513]
拡散言語モデル(dLLM)に基づいて構築されたフレームワークであるDiffuRankを提案する。
dLLMは、左から右への順序に制約されないより柔軟なデコーディングと生成プロセスをサポートする。
モデルサイズが類似した自己回帰LDMに匹敵する性能を示す。
論文 参考訳（メタデータ） (2026-02-13T02:18:14Z) - Prism: Efficient Test-Time Scaling via Hierarchical Search and Self-Verification for Discrete Diffusion Language Models [96.0074341403456]
LLM推論を改善するための実用的な方法として、推論時計算が再導入されている。
テスト時間スケーリング(TTS)アルゴリズムの多くは、自動回帰デコーディングに依存している。
そこで我々は,dLLM のための効率的な TTS フレームワーク Prism を提案する。
論文 参考訳（メタデータ） (2026-02-02T09:14:51Z) - CompassVerifier: A Unified and Robust Verifier for LLMs Evaluation and Outcome Reward [50.97588334916863]
評価と結果報酬のための正確で堅牢な軽量検証モデルであるCompassVerifierを開発した。
数学、知識、多種多様な推論タスクにまたがる多分野の能力を示し、様々な答えの型を処理する能力を示す。
我々は,複数のデータソースから収集したモデル出力からなるVerifierBenchベンチマークを導入し,メタエラーパターンを手動で解析してCompassVerifierを強化する。
論文 参考訳（メタデータ） (2025-08-05T17:55:24Z) - APOLLO: Automated LLM and Lean Collaboration for Advanced Formal Reasoning [16.8655558789989]
本稿では,自動定理証明のためのモデルに依存しないエージェントフレームワークであるAPOLLO (Automated PrOof repair viaLLM and Lean cOllaboration)を提案する。
エージェントのセットは、証明を分析し、シンタックスのエラーを修正し、リーンを使って証明の誤りを特定し、失敗するサブレムマを分離し、自動化されたソルバを利用し、残りの目標に対してLLMを呼び出す。
この結果から,LLM出力を目標としたコンパイラ誘導型修復は,効率と正確性の両方において劇的に向上することが示された。
論文 参考訳（メタデータ） (2025-05-09T03:38:31Z) - APE-Bench I: Towards File-level Automated Proof Engineering of Formal Math Libraries [5.227446378450704]
APE-Bench Iは、Mathlib4の実際のコミット履歴から構築された最初の現実的なベンチマークである。
Eleansticはスケーラブルな並列検証インフラストラクチャで、Mathlibの複数バージョンにわたる検証に最適化されている。
論文 参考訳（メタデータ） (2025-04-27T05:04:02Z) - Neural Theorem Proving: Generating and Structuring Proofs for Formal Verification [0.26763498831034044]
組込み戦術の力と既製の自動定理プローバーを利用するシステム内で使用される形式言語で全ての証明を生成するフレームワークを導入する。
LLMのトレーニングには2段階の微調整プロセスを使用し、まずSFTベースのトレーニングを使用して、モデルが構文的に正しいIsabelleコードを生成する。
我々は,MiniF2F-testベンチマークとIsabelle証明アシスタントを用いてフレームワークを検証し,S3バケットアクセスポリシーコードの正当性を検証するためのユースケースを設計する。
論文 参考訳（メタデータ） (2025-04-23T18:04:38Z) - ProofAug: Efficient Neural Theorem Proving via Fine-grained Proof Structure Analysis [50.020850767257095]
本稿では,LLMに様々な粒度で自動化手法を付加するProofAugを提案する。
本手法は,オープンソースのDeep-math-7bベースモデルとIsabelle証明アシスタントを用いて,MiniF2Fベンチマークで検証した。
また、ProofAugのLean 4バージョンを実装し、Kimina-Prover-seek-Distill-1.5Bのパス@1のパフォーマンスを44.3%から50.4%に改善します。
論文 参考訳（メタデータ） (2025-01-30T12:37:06Z) - FVEL: Interactive Formal Verification Environment with Large Language Models via Theorem Proving [53.43068330741449]
大規模言語モデル(LLM)を用いた対話型形式検証環境FVELを提案する。
FVELは、検証対象のコードをIsabelleに変換し、LLMで証明された神経自動定理を用いて検証を行う。
FVELERデータセットには、Isabelleで定式化されたコード依存関係と検証プロセスが含まれており、758の理論、29,125のレムマ、200,646の証明ステップが含まれている。
論文 参考訳（メタデータ） (2024-06-20T15:31:05Z) - Selene: Pioneering Automated Proof in Software Verification [62.09555413263788]
実世界の産業レベルのマイクロカーネルであるseL4をベースとした,最初のプロジェクトレベルの自動証明ベンチマークであるSeleneを紹介する。
GPT-3.5-turbo や GPT-4 のような先進的な大規模言語モデル (LLM) による実験結果から, 自動証明生成領域における LLM の機能を強調した。
論文 参考訳（メタデータ） (2024-01-15T13:08:38Z) - Leveraging Large Language Models for Automated Proof Synthesis in Rust [6.202137610101939]
大規模言語モデル(LLM)は、コード解析と合成に成功している。
我々は、LLMと静的解析を組み合わせることで、Verusと呼ばれるRustベースの形式検証フレームワークの不変性、アサーション、その他の証明構造を合成する。
プロトタイプでは,検証タスクを複数の小さなタスクに分割し,反復的にGPT-4をクエリし,その出力と軽量な静的解析を組み合わせる。
論文 参考訳（メタデータ） (2023-11-07T05:47:47Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。