Neural Theorem Proving for Verification Conditions: A Real-World Benchmark

• URL: http://arxiv.org/abs/2601.18944v2
• Date: Wed, 28 Jan 2026 18:25:21 GMT
• Title: Neural Theorem Proving for Verification Conditions: A Real-World Benchmark
• Abstract summary: This work introduces Neural Theorem Proving for Verification Conditions (NTP4VC), presenting the first real-world multi-language benchmark for this task.<n>We evaluate large language models (LLMs), both general-purpose and those fine-tuned for theorem proving, on NTP4VC.
• Score: 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.

Related papers

• TCS-BENCH: Benchmarking State-of-the-Art Generative AI Theoretical Computer Science Research Ability [59.079078796751496]
  We introduce TCS-Bench, a benchmark for evaluating Large Language Models (LLMs) on research-level Theoretical Computer Science (TCS) proof generation.<n> TCS-Bench consists of theorem-proving tasks from papers published at top theoretical computer science venues.
  arXiv  Detail & Related papers  (2026-08-10T12:36:16Z)
• Learning to Reason with Insight for Informal Theorem Proving [50.054221663394195]
  In this work, we identify a primary bottleneck in informal theorem proving as a lack of insight.<n>We propose a novel framework designed to cultivate this essential reasoning skill and enable LLMs to perform insightful reasoning.<n>Our experiments on challenging mathematical benchmarks demonstrate that this insight-aware generation strategy significantly outperforms baselines.
  arXiv  Detail & Related papers  (2026-04-17T17:36:21Z)
• Certified Program Synthesis with a Multi-Modal Verifier [5.998029529040967]
  LeetProof is an agentic pipeline built on Velvet, a multi-modal verifier embedded in Lean.<n>It combines dynamic validation, automated proofs, and interactive proof scripting in one foundational framework.<n>We evaluate LeetProof on benchmarks derived from prior work on certified synthesis.
  arXiv  Detail & Related papers  (2026-04-17T14:56:45Z)
• Lemma Discovery in Agentic Program Verification [12.551445518827768]
  Deductive verification provides strong correctness guarantees for code by extracting verification conditions (VCs) and writing formal proofs for them.<n>The expertise-intensive task of VC proving is the main bottleneck in this process, and has been partly automated owing to recent advances in Large Language Model (LLM) agents.<n>We argue that VC proving for program verification is more than a purely mathematical task, and benefits considerably from program comprehension.
  arXiv  Detail & Related papers  (2026-03-23T15:42:07Z)
• Stepwise: Neuro-Symbolic Proof Search for Automated Systems Verification [21.423111823947867]
  This paper introduces a neuro-symbolic proof generation framework designed to automate proof search for systems-level verification projects.<n>The framework performs a best-first tree search over proof states, repeatedly querying an LLM for the next candidate proof step.<n>Results across further benchmarks demonstrate strong generalization, indicating a viable path toward scalable automated software verification.
  arXiv  Detail & Related papers  (2026-03-20T07:45:49Z)
• Can LLMs Reason Like Automated Theorem Provers for Rust Verification? VCoT-Bench: Evaluating via Verification Chain of Thought [1.167370706056905]
  VCoT-Lift lifts low-level solver reasoning into high-level, human-readable verification steps.<n>VCoT-Bench measures performance along three dimensions: robustness to varying degrees of missing proofs, competence across different proof types, and sensitivity to the proof locations.
  arXiv  Detail & Related papers  (2026-03-18T22:42:20Z)
• TorchLean: Formalizing Neural Networks in Lean [71.68907600404513]
  We introduce TorchLean, a framework that treats learned models as first-class mathematical objects with a single, precise semantics shared by execution and verification.<n>We validate TorchLean end-to-end on certified robustness, physics-informed residual bounds for PINNs, and Lyapunov-style neural controller verification.
  arXiv  Detail & Related papers  (2026-02-26T05:11:44Z)
• Towards Real-World Industrial-Scale Verification: LLM-Driven Theorem Proving on seL4 [14.340488105076062]
  Formal methods (FM) are reliable but costly to apply.<n>Recent advances in large language models (LLMs) have made automated theorem proving increasingly feasible.<n>We propose AutoReal, an LLM-driven theorem proving method for real-world industrial-scale systems.
  arXiv  Detail & Related papers  (2026-02-09T08:35:54Z)
• The 4/$δ$ Bound: Designing Predictable LLM-Verifier Systems for Formal Method Guarantee [5.345468714252351]
  This work bridges the gap by developing an LLM-Verifier Convergence Theorem.<n>We model the interaction between the LLM and the verifier as a discrete-time Markov Chain.<n>We stress-tested this prediction in an extensive empirical campaign comprising more than 90,000 trials.
  arXiv  Detail & Related papers  (2025-11-30T22:19:09Z)
• BRIDGE: Building Representations In Domain Guided Program Verification [67.36686119518441]
  BRIDGE decomposes verification into three interconnected domains: Code, Specifications, and Proofs.<n>We show that this approach substantially improves both accuracy and efficiency beyond standard error feedback methods.
  arXiv  Detail & Related papers  (2025-11-26T06:39:19Z)
• Evaluating Program Semantics Reasoning with Type Inference in System F [5.6064011695311455]
  Large Language Models (LLMs) are increasingly integrated into the software engineering ecosystem.<n>We introduce TF-Bench, a benchmark designed to evaluate LLM reasoning based on type inference in System F.<n>We construct TF-Bench_pure, a purely semantics-driven variant of TF-Bench.
  arXiv  Detail & Related papers  (2025-09-28T06:57:42Z)
• Lean Meets Theoretical Computer Science: Scalable Synthesis of Theorem Proving Challenges in Formal-Informal Pairs [41.29431283264807]
  We propose leveraging theoretical computer science (TCS) as a scalable source of rigorous proof problems.<n>We demonstrate this approach on two TCS domains: Busy Beaver problems, which involve proving bounds on Turing machine halting behavior, and Mixed Boolean Arithmetic problems, which combine logical and arithmetic reasoning.<n>Our framework automatically synthesizes problems with parallel formal (Lean4) and informal (Markdown) specifications, creating a scalable pipeline for generating verified proof challenges.
  arXiv  Detail & Related papers  (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]
  Large Language Models (LLMs) trained with Reinforcement Learning (RL) face a significant challenge: their verification processes are neither reliable nor scalable.<n>A promising yet largely uncharted alternative is formal language-based reasoning.<n>Grounding LLMs in rigorous formal systems where generative models operate in formal language spaces (e.g., Dafny) enables the automatic and mathematically provable verification of their reasoning processes and outcomes.
  arXiv  Detail & Related papers  (2025-07-22T08:13:01Z)
• DeepTheorem: Advancing LLM Reasoning for Theorem Proving Through Natural Language and Reinforcement Learning [67.93945726549289]
  DeepTheorem is a comprehensive informal theorem-proving framework exploiting natural language to enhance mathematical reasoning.<n>DeepTheorem includes a large-scale benchmark dataset consisting of 121K high-quality IMO-level informal theorems and proofs.<n>We devise a novel reinforcement learning strategy (RL-Zero) explicitly tailored to informal theorem proving, leveraging the verified theorem variants to incentivize robust mathematical inference.
  arXiv  Detail & Related papers  (2025-05-29T17:59:39Z)
• Alchemy: Amplifying Theorem-Proving Capability through Symbolic Mutation [71.32761934724867]
  This work proposes Alchemy, a framework for data synthesis that constructs formal theorems through symbolic mutation.<n>For each candidate theorem in Mathlib, we identify all invocable theorems that can be used to rewrite or apply to it.<n>As a result, our method increases the number of theorems in Mathlib by an order of magnitude, from 110k to 6M.
  arXiv  Detail & Related papers  (2024-10-21T08:04:21Z)
• Lean-STaR: Learning to Interleave Thinking and Proving [53.923617816215774]
  We present Lean-STaR, a framework for training language models to produce informal thoughts prior to each step of a proof.<n>Lean-STaR achieves state-of-the-art results on the miniF2F-test benchmark within the Lean theorem proving environment.
  arXiv  Detail & Related papers  (2024-07-14T01:43:07Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.