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

Technical Summary: Neural Theorem Proving for Verification Conditions (NTP4VC)

Problem Statement
Program verification is a cornerstone of software reliability, yet its adoption remains limited to safety-critical domains. A primary bottleneck is the manual effort required to prove Verification Conditions (VCs)—logical propositions encoding program correctness. While Automated Theorem Provers (ATPs) excel in specific domains, they frequently fail on real-world VCs, necessitating extensive manual annotations and proofs. Although Neural Theorem Proving (NTP) has shown promise in mathematical competitions, its application to the specific, high-stakes domain of automated VC proving in program verification remains largely unexplored. Furthermore, existing benchmarks for theorem proving often focus on auxiliary lemmas or mathematical puzzles rather than the direct VCs generated by industrial verification pipelines, and they lack support for multiple formal languages.

Methodology
The authors introduce NTP4VC, a task and benchmark designed to evaluate the ability of Large Language Models (LLMs) to automate VC proving. The methodology involves three core components:

1. Corpus Extraction and Translation:

   • The benchmark leverages existing industrial verification projects (e.g., Linux kernel scheduler, Contiki-OS memory allocator) processed through established pipelines: Frama-C (for C code) and Why3 (as a verification backend).
   • Since native VCs in mainstream NTP languages like Lean are scarce for industrial projects, the authors developed a rule-based translation pipeline. This system extracts VCs from Why3 and translates them into Isabelle, Lean, and Rocq (formerly Coq).
   • The translation relies on approximately 2,400 expert-written mapping and rewriting rules (per language) to ensure semantic preservation and idiomatic expression in the target languages, avoiding the unreliability of LLM-based translation.

2. Complication Process:

   • VCs extracted directly from verified projects are often "too easy" because human developers have already provided sufficient annotations (e.g., assert, lemma, and lemma application annotations) to guide ATPs.
   • To create challenging benchmark cases, the authors implemented a complication process that systematically removes these auxiliary annotations. This restores the VCs to a state closer to fully automated verification, significantly increasing difficulty while maintaining provability (assuming a sufficiently strong prover).

3. Benchmark Construction:

   • The final benchmark consists of 600 carefully selected VCs drawn from over 7,500 candidates.
   • The set is balanced between two categories:
     • Pearls of Programs (50%): Minimal working programs capturing verification pain points (algorithms, data structures, competition problems like VerifyThis).
     • Real C Verification (50%): VCs derived from industrial C projects (e.g., Contiki-OS, Linux kernel, X.509 parsers).
   • The difficulty is calibrated such that the strongest predefined ATP tactic in Why3 (Auto_Level_3) achieves a pass rate between 20% and 25%, ensuring a mix of solvable and open problems.

Key Contributions

• Definition of NTP4VC: The paper formally defines the task of applying machine-learning-based proof generation to automate VC proving, identifying it as a critical bottleneck in program verification.
• Reliable Extraction Method: A novel, open-sourced method for extracting and translating VCs from industrial verification pipelines into multiple ITP languages using expert-written rules rather than LLMs, ensuring semantic fidelity.
• First Real-World Multi-Language Benchmark: The introduction of NTP4VC, the first benchmark specifically targeting automated VC proving across Isabelle, Lean, and Rocq, featuring a diverse mix of algorithmic and industrial cases.
• Comprehensive Evaluation: An extensive evaluation of seven models, including general-purpose LLMs (e.g., GPT-4o-mini, Qwen3) and specialized theorem provers (e.g., DeepSeek-Prover-V2, Goedel-Prover), alongside classical "hammer" provers (Sledgehammer, CoqHammer).

Results
The evaluation reveals significant challenges for current NTP models in program verification:

• Low Pass Rates: Even the best-performing models achieve very low success rates. The top language-specific fine-tuned model (Minilang) achieves only 2.08% pass@1 on Isabelle. General-purpose models perform even worse (e.g., GPT-o4-mini-high at 1.19% pass@1).
• Comparison with Hammers: Classical hammer-based provers significantly outperform neural models. Sledgehammer achieves 18.00% pass@1 on Isabelle, and CoqHammer achieves 5.67% on Rocq.
• Error Analysis: Failure modes differ from mathematical benchmarks. NTP models struggle with:
  • Syntactic Errors: ~24% of Isabelle proofs fail due to mismatched parentheses or syntax issues in deeply nested formulas.
  • Semantic Confusion: Models often produce pragmatically incorrect code (e.g., imperative assignments in Lean instead of declarative tactics) or repetitive, meaningless tactic applications.
  • Hallucination: Models frequently invoke non-existent tactics (e.g., why3 in Rocq) or undefined constants.
• Domain Specificity: Hammers perform markedly better on "Real C Verification" tasks than on "Pearls of Programs," suggesting that classical reasoning techniques (SMT solvers) are highly optimized for industrial verification scenarios, whereas NTP models struggle across both domains.

Significance and Claims
The paper claims that NTP4VC establishes a foundational benchmark for advancing neural approaches to program verification. The results highlight a substantial gap between current NTP capabilities and the requirements of real-world program verification, indicating that program verification demands fundamentally different reasoning capabilities than mathematical competition problems. The authors assert that while LLMs show promise, significant progress is needed in handling the long, deeply nested, and syntactically rigid nature of VCs. The work provides a necessary infrastructure (benchmark and extraction pipeline) to drive future research toward closing this gap, potentially leading to breakthroughs in automated program verification. The authors remain modest, noting that the benchmark cases are derived from formally verified projects but acknowledging that implementation bugs in the translation pipeline could theoretically render some cases unprovable, though they have taken extensive measures to mitigate this.