論文の概要: 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（参考訳）: ステップワイズ:自動システム検証のためのニューロシンボリック証明探索
• Authors: Baoding He, Zenan Li, Wei Sun, Yuan Yao, Taolue Chen, Xiaoxing Ma, Zhendong Su,
• 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 をはるかに上回り、さらに多段階の証明を解く。 さらなるベンチマークの結果は強力な一般化を示し、スケーラブルな自動ソフトウェア検証への道のりを示している。

関連論文リスト

• DiffuRank: Effective Document Reranking with Diffusion Language Models [71.16830004674513]
  拡散言語モデル(dLLM)に基づいて構築されたフレームワークであるDiffuRankを提案する。 dLLMは、左から右への順序に制約されないより柔軟なデコーディングと生成プロセスをサポートする。 モデルサイズが類似した自己回帰LDMに匹敵する性能を示す。
  論文  参考訳（メタデータ） (2026-02-13T02:18:14Z)
• 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)
• 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)

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

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