論文の概要: 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の実証に有望であることを示しているが、プログラム検証には大きな課題が残っており、将来の研究における大きなギャップと機会が浮かび上がっていることを示している。

関連論文リスト

• TorchLean: Formalizing Neural Networks in Lean [71.68907600404513]
  本稿では,学習モデルを一級数学的対象として扱うフレームワークであるTorchLeanを紹介する。 我々はTorchLeanのエンドツーエンドを、証明された堅牢性、PINNの物理インフォームド残差、Lyapunovスタイルのニューラルコントローラ検証で検証する。
  論文  参考訳（メタデータ） (2026-02-26T05:11:44Z)
• Towards Real-World Industrial-Scale Verification: LLM-Driven Theorem Proving on seL4 [14.340488105076062]
  形式的手法(FM)は信頼性が高いが、適用にはコストがかかる。 大規模言語モデル(LLM)の最近の進歩により、自動定理はますます実現可能になっている。 実世界の産業規模のシステムにおけるLCMによる定理証明手法であるAutoRealを提案する。
  論文  参考訳（メタデータ） (2026-02-09T08:35:54Z)
• 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)
• BRIDGE: Building Representations In Domain Guided Program Verification [67.36686119518441]
  BRIDGEは、検証をコード、仕様、証明の3つの相互接続ドメインに分解する。 提案手法は, 標準誤差フィードバック法よりも精度と効率を著しく向上することを示す。
  論文  参考訳（メタデータ） (2025-11-26T06:39:19Z)
• 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)
• Re:Form -- Reducing Human Priors in Scalable Formal Software Verification with RL in LLMs: A Preliminary Study on Dafny [78.1575956773948]
  強化学習(RL)で訓練された大規模言語モデル(LLM)は、信頼性も拡張性もない、という大きな課題に直面している。 有望だが、ほとんど報われていない代替手段は、フォーマルな言語ベースの推論である。 生成モデルが形式言語空間(例えばダフニー)で機能する厳密な形式体系におけるLLMの接地は、それらの推論プロセスと結果の自動的かつ数学的に証明可能な検証を可能にする。
  論文  参考訳（メタデータ） (2025-07-22T08:13:01Z)
• 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)
• Alchemy: Amplifying Theorem-Proving Capability through Symbolic Mutation [71.32761934724867]
  この研究は、記号的突然変異を通じて形式的な定理を構成するデータ合成のフレームワークであるAlchemyを提案する。 マドリブにおける各候補定理について、書き直しや適用に使用できるすべてのイベーシブルな定理を同定する。 その結果、マドリブの定理の数は110kから6Mへと桁違いに増加する。
  論文  参考訳（メタデータ） (2024-10-21T08:04:21Z)
• Lean-STaR: Learning to Interleave Thinking and Proving [53.923617816215774]
  証明の各ステップに先立って,非公式な思考を生成するために,言語モデルをトレーニングするフレームワークであるLean-STaRを紹介します。 Lean-STaRは、Lean定理証明環境内のminiF2F-testベンチマークで最先端の結果を達成する。
  論文  参考訳（メタデータ） (2024-07-14T01:43:07Z)

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

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