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

AI summary

Authors: Qiyuan Xu, Xiaokun Luan, Renxi Wang, Joshua Ong Jun Leang, Peixin Wang, Haonan Li, Wenda Li, Conrad Watt (NTU, MBZUAI, Peking University, Imperial College London, University of Edinburgh, East China Normal University) arXiv: 2601.18944v2 [cs.AI], 28 Jan 2026 | License: CC BY 4.0

Overview

Research area: Neural theorem proving (NTP), formal program verification, automated reasoning with large language models, and benchmark construction for interactive theorem provers (ITPs).

Technical level: Advanced. The paper assumes familiarity with verification conditions (VCs), verification condition generators, industrial verifiers (Why3, Frama-C), interactive theorem prover languages (Lean, Isabelle, Rocq), and ATP/hammer tooling.

Scope: The paper defines the NTP4VC task, builds the first real-world, multi-language benchmark of 600 verification conditions extracted from industrial and algorithmic verification projects, and evaluates state-of-the-art neural provers and classical hammers on it.

What This Paper Is About

In program verification, a verifier generates logical propositions called verification conditions (VCs) and then asks a theorem prover to prove them. Existing automated theorem provers (ATPs) fail on many real-world VCs, forcing developers to write large amounts of manual proofs and annotations. The goal of this paper is to establish whether neural theorem proving (proving theorems with machine-learning models) can automate VC proving, and to provide a benchmark that measures progress on exactly that bottleneck across three proof languages.

Key Contributions

1. Task definition (NTP4VC): The authors formally define Neural Theorem Proving for Verification Conditions as the task of applying machine-learning-based proof generation directly to the theorem proving of VCs, which they identify as a key bottleneck in automated program verification.
2. A reliable, automatic corpora extraction method: They reuse industrial verification pipelines (Why3 and Frama-C) and over 2,400 expert-written mapping and rewriting rules (approximately 800 per target language for Isabelle, Lean, and Rocq; about 3 × 800 in total) to translate Why3 VCs into semantically equivalent ITP statements, with the implementation open-sourced.
3. The first real-world, multi-language NTP4VC benchmark: 600 VCs selected from more than 7.5k extracted VCs, split 50/50 into Pearls of Programs (300 cases) and Real C Verification (300 cases), each balanced across sub-categories to target roughly a 20%–25% ATP pass rate.
4. Extensive evaluation: Seven models plus hammer baselines (Sledgehammer for Isabelle/HOL, CoqHammer for Rocq) are evaluated, with qualitative error analysis of generated proofs.

Main Findings

• Neural provers perform far below their mathematics benchmarks. On NTP4VC, no NTP model exceeds a pass@8 of 12% across Lean, Rocq, and Isabelle. For comparison, the paper reports DeepSeek-Prover-V2 achieving 55.5% pass@1 on miniF2F and Goedel-Prover-V2-32B achieving 88.1% pass@32, with 7.15% and 13.09% pass rates respectively on PutnamBench.
• The strongest fine-tuned prover reaches only 2.08% pass@1. The best language-specific fine-tuned prover obtains 2.08% pass@1 (Minilang on Isabelle; Table 5 lists 2.08 / 7.29 / 11.46 for pass@1 / pass@4 / pass@8). General-purpose models are lower, with GPT-o4-mini-high achieving 1.19% pass@1 on Isabelle, 0.50% on Lean, and 0.00% on Rocq.
• Hammers beat every neural prover. Sledgehammer reaches 18.00% on Isabelle while CoqHammer reaches 5.67% on Rocq, compared with 114/600 (19.00%) overall for hammers versus 34/600 (5.67%) overall for NTP models in the category breakdown.
• The gap is largest on industrial C verification. NTP models solve 15/300 (5.00%) of Pearls of Programs and 16/300 (5.33%) of Real C Verification, whereas hammers solve 32/300 (10.67%) and 82/300 (27.33%) respectively. Category-level hammer results include 30.86% on Function, 23.46% on Loop, 24.32% on Memory, and 31.25% on Invalid Arg.
• Complication makes VCs genuinely hard. Erasing assert, lemma, and lemma-application annotations reduces Why3's strongest ATP pass rate from approximately 99% to approximately 62% on Why3's bundled examples, without affecting provability by a strong enough prover.
• Syntactic coherence is a major failure mode. More than 24% of generated Isabelle proofs contain syntactic errors (for example, a proof for an AVL tree VC failed to parse due to mismatched parentheses).
• Models misunderstand the proof paradigm. More than 64% of Lean proofs generated by Goedel-Prover-V2-32B degenerate into repetitive, meaningless tactic applications (such as "have h₁₆ ≔ h₀; have h₁₇ ≔ h₁ …"), and models use imperative-style assignments instead of declarative, tactic-based reasoning.
• Hallucination of non-existent entities is common. At least 9% of proof attempts in Isabelle failed due to undefined constants or lemmas; GPT-o4-mini often invokes a tactic called why3 that does not exist in Rocq.
• The benchmark is designed to be contamination-resistant. Because VCs are generated only transiently, most are unprovable by existing ATPs after complication, and Why3 records only which ATP tools were used rather than storing detailed proofs.
• A caveat on provability: although all cases derive from formally verified projects, the authors state they cannot guarantee actual provability of every case because of possible implementation bugs across Frama-C, Why3, and their translation pipelines.

Methodology in Plain English

The researchers did not write VCs from scratch. Instead, they took existing verification projects that already pass industrial verifiers, ran those verifiers' verification condition generators, and captured the resulting VCs as abstract syntax trees in XML. A Python framework then maps those trees into Isabelle, Lean, and Rocq using rules written by human ITP experts, including pretty-printing rules and rewriting rules that turn combinations of terms into more idiomatic target-language expressions. This lets the team extract VCs from projects such as the Linux kernel scheduler, Linux kernel library functions, and the Contiki OS memory allocator and linked-list library.

Because VCs from already-verified projects are usually easy for ATPs — the developers added annotations precisely to make them easy — the authors introduce a "complication process" that simply erases three kinds of simplifying annotations: assert annotations, lemma annotations, and explicit lemma-application annotations. This restores the tasks to what they would look like under a stronger prover while keeping them provable in principle.

The team extracted over 7.5k VCs, ran a three-round selection process (domain selection across 224 Toccata Team projects, of which 100 were kept for the benchmark and 124 reserved as potential training data; initial screening to about 1.5k candidates, including roughly 1.2k hard VCs and roughly 350 easy VCs; then collaborative expert evaluation), and settled on 600 cases. Each case is a single proof goal in its own theory file, and difficulty is measured by whether Why3's hybrid tactic Auto_Level_3 (AL3, combining Z3, CVC4, SPASS, Alt-Ergo, and E-prover) fails to solve a VC within 10 minutes on a 12-core workstation. Models were queried zero-shot at temperature 1.0 with a 32,000-token generation limit, most with 8 attempts per problem, and proofs were checked with Lean 4.21.0, Rocq 8.20.1, and Isabelle 2024 under a 10-minute per-attempt timeout on an AMD Ryzen 9 7900X with 64GB RAM.

Why This Matters

Impact on research: The paper separates the annotation-synthesis problem from the VC-proving problem and shows that current neural provers are not merely behind classical automation — they have not yet surpassed it in this domain at all. It provides a measurable target for the NTP community in a domain where the paper argues VCs are long, deeply nested, machine-generated formulas that stress long-range syntactic coherence rather than the semantic insight that mathematics benchmarks reward.

Real-world applications:

• Safety-critical and embedded software verification, where the paper notes adoption is limited to such domains and where annotations can balloon (about 600 lines of annotations for a linked-list library in Frama-C, nearly matching the original C code length).
• Operating system and kernel component verification, since the benchmark draws on the Contiki OS memory allocator and linked-list library and the Linux kernel scheduler and library functions.
• Cryptographic and protocol software, including the X.509 parser (9 VCs, 5,044 lines of C code) and the Paparazzi UAV autopilot math library (16 VCs, 3,159 lines of C code).
• Reducing manual proof burden in industrial C verification, where the Real C Verification half of the benchmark shows hammers already reaching 27.33% versus 5.33% for neural models.

Industry relevance: Because the benchmark is built on Why3 and Frama-C — pipelines already used for air traffic management algorithms, embedded operating systems, cryptographic modules, the Linux kernel scheduler, and the JavaCard virtual machine — improvements measured on NTP4VC map directly onto tools that industry already deploys. The code and benchmark are released at https://github.com/xqyww123/NTP4VC under an MIT license for the authors' code, with VCs released under the licenses of their source projects.

Future Directions

• Close the gap to classical automation. Current NTP models stay below the hammer baselines; the paper frames surpassing Sledgehammer's 18.00% on Isabelle as the immediate bar.
• Train on the reserved corpora. The extraction method is described as producing "potentially training corpora," and 124 Toccata projects were explicitly left aside for potential use as training data.
• Handle long, deeply nested VC structure. Beyond 24% syntactic errors and over 64% degenerate Lean proofs point to architecture and training objectives suited to large machine-generated formulas rather than competition mathematics.
• Combine neural and classical reasoning. The paper reports that incorporating Sledgehammer into Minilang's model yields an 11.56% pass rate in the text (Table 5 lists Minilang at 11.46% pass@8 on Isabelle), which still does not beat Sledgehammer alone; it also notes NTP4VC and annotation synthesis are complementary and can be applied orthogonally.
• Extend and harden the benchmark. The authors flag provability caveats and note the translation approach could target potentially other languages beyond Isabelle, Lean, and Rocq.

Target Audience

Researchers and graduate students in neural theorem proving, automated reasoning, and formal verification; engineers building or evaluating verifiers based on Why3, Frama-C, Lean, Isabelle, and Rocq; and machine-learning practitioners interested in benchmarks where LLM reasoning performance diverges sharply from mathematics competitions. Readers need working knowledge of ITP proof languages and the VC pipeline to get the most from the paper.

Authors’ 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.