論文の概要: Neural Theorem Proving for Verification Conditions: A Real-World Benchmark

• arxiv url: http://arxiv.org/abs/2601.18944v2
• Date: Wed, 28 Jan 2026 18:25:21 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-01-29 15:46:06.579721
• Title: Neural Theorem Proving for Verification Conditions: A Real-World Benchmark
• Title（参考訳）: 検証条件のニューラルネットワークによる検証 - 実世界のベンチマーク
• Authors: Qiyuan Xu, Xiaokun Luan, Renxi Wang, Joshua Ong Jun Leang, Peixin Wang, Haonan Li, Wenda Li, Conrad Watt,
• Abstract要約: この研究は、NTP4VC(Neural Theorem Proving for Verification Conditions)を導入し、このタスクのための最初の実世界のマルチ言語ベンチマークを示す。 NTP4VC を用いて,大言語モデル (LLM) の評価を行った。
• 参考スコア（独自算出の注目度）: 9.350519191460018
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Theorem proving is fundamental to program verification, where the automated proof of Verification Conditions (VCs) remains a primary bottleneck. Real-world program verification frequently encounters hard VCs that existing Automated Theorem Provers (ATPs) cannot prove, leading to a critical need for extensive manual proofs that burden practical application. While Neural Theorem Proving (NTP) has achieved significant success in mathematical competitions, demonstrating the potential of machine learning approaches to formal reasoning, its application to program verification--particularly VC proving--remains largely unexplored. Despite existing work on annotation synthesis and verification-related theorem proving, no benchmark has specifically targeted this fundamental bottleneck: automated VC proving. This work introduces Neural Theorem Proving for Verification Conditions (NTP4VC), presenting the first real-world multi-language benchmark for this task. From real-world projects such as Linux and Contiki-OS kernel, our benchmark leverages industrial pipelines (Why3 and Frama-C) to generate semantically equivalent test cases across formal languages of Isabelle, Lean, and Rocq. We evaluate large language models (LLMs), both general-purpose and those fine-tuned for theorem proving, on NTP4VC. Results indicate that although LLMs show promise in VC proving, significant challenges remain for program verification, highlighting a large gap and opportunity for future research.
• Abstract（参考訳）: 定理証明は、検証条件の自動証明(VC)が主要なボトルネックであるプログラム検証の基礎となる。 実世界のプログラム検証は、既存のAutomated Theorem Provers(ATP)が証明できないハードVCに頻繁に遭遇する。 Neural Theorem Proving (NTP) は数学の競争で大きな成功を収め、フォーマルな推論への機械学習アプローチの可能性を示す一方で、その検証プログラムへの応用(特にVCの証明)は、ほとんど探索されていない。 アノテーション合成と検証関連の定理証明に関する既存の研究にもかかわらず、この基本的なボトルネックを特に狙うベンチマークは、特にない。 この研究は、NTP4VC(Neural Theorem Proving for Verification Conditions)を導入し、このタスクのための最初の実世界のマルチ言語ベンチマークを示す。 LinuxやContiki-OSカーネルのような実世界のプロジェクトから、我々のベンチマークは産業用パイプライン(Why3とFrama-C)を利用して、Isabelle、Lean、Rocqといった形式言語で意味的に等価なテストケースを生成する。 NTP4VC を用いて,大言語モデル (LLM) の評価を行った。 結果は、LCMはVCの実証に有望であることを示しているが、プログラム検証には大きな課題が残っており、将来の研究における大きなギャップと機会が浮かび上がっていることを示している。

関連論文リスト

• The 4/$δ$ Bound: Designing Predictable LLM-Verifier Systems for Formal Method Guarantee [5.345468714252351]
  この研究は LLM-Verifier Convergence Theorem の開発によってギャップを埋める。 LLMと検証器の相互作用を離散時間マルコフ連鎖としてモデル化する。 われわれはこの予測を90,000件以上の治験を含む広範囲な実証キャンペーンでストレステストした。
  論文  参考訳（メタデータ） (2025-11-30T22:19:09Z)
• Evaluating Program Semantics Reasoning with Type Inference in System F [5.6064011695311455]
  大規模言語モデル(LLM)は、ソフトウェアエンジニアリングエコシステムにますます統合されています。 本稿では,システムFの型推論に基づいてLLM推論を評価するベンチマークであるTF-Benchを紹介する。 TF-Bench_pureは、純粋に意味論的に駆動されるTF-Benchの変種である。
  論文  参考訳（メタデータ） (2025-09-28T06:57:42Z)
• Lean Meets Theoretical Computer Science: Scalable Synthesis of Theorem Proving Challenges in Formal-Informal Pairs [41.29431283264807]
  本稿では、厳密な証明問題のスケーラブルな情報源として理論計算機科学(TCS)を活用することを提案する。 本稿では,2つのTCS領域に対して,チューリング機械停止動作の証明を含むベイジービーバー問題(Busy Beaver problem)と,論理と算術の推論を組み合わせた混合ブール算術問題(Mixed Boolean Arithmetic problem)を提案する。 我々のフレームワークは,並列形式 (Lean4) と非公式 (Markdown) 仕様で問題を自動生成し,検証問題を生成するスケーラブルなパイプラインを作成する。
  論文  参考訳（メタデータ） (2025-08-21T14:15:40Z)
• DeepTheorem: Advancing LLM Reasoning for Theorem Proving Through Natural Language and Reinforcement Learning [67.93945726549289]
  DeepTheoremは、数学的推論を強化するために自然言語を活用する包括的な非公式な定理証明フレームワークである。 DeepTheoremには、121Kの高品質なIMOレベルの非公式な定理と証明からなる大規模なベンチマークデータセットが含まれている。 我々は、証明された定理の変種を利用して堅牢な数学的推論を動機付けることによって、非公式な定理証明に適した新しい強化学習戦略(RL-Zero)を考案する。
  論文  参考訳（メタデータ） (2025-05-29T17:59:39Z)
• Lean-STaR: Learning to Interleave Thinking and Proving [53.923617816215774]
  証明の各ステップに先立って,非公式な思考を生成するために,言語モデルをトレーニングするフレームワークであるLean-STaRを紹介します。 Lean-STaRは、Lean定理証明環境内のminiF2F-testベンチマークで最先端の結果を達成する。
  論文  参考訳（メタデータ） (2024-07-14T01:43:07Z)

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

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