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

TL;DR

This work targets the bottleneck of automated Verification Condition ($VC$) proving in real-world software verification. It introduces NTP4VC, the first real-world, multi-language benchmark for VC proving, built by translating Why3/Frama-C VCs into Isabelle, Lean, and Rocq via hundreds of expert rules and a complication step that erases annotations to produce harder goals. A reliable corpus-generation pipeline and open-source artifacts extract more than $7.5k$ VCs and produce a diverse set of 600 benchmark cases, enabling cross-language evaluation. Empirical results show neural theorem provers lag far behind traditional provers (best $P@1$ around $2.08 ext{ extdiv}1$) and highlight substantial domain-specific challenges, particularly for Real C Verification, motivating future work on neural and hybrid approaches for automated program verification.

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.

Figures (6)

• Figure 1: The conventional and NTP-based workflow of program verification.
• Figure 2: Our pipeline for extracting benchmark cases.
• Figure 3: The generation process of the benchmark cases and potentially training corpora.
• Figure 4: An Isabelle proof generated by DeepSeek-V3.1 for a VC in the benchmark. This proof contains syntax errors, including a missing closing parenthesis and two redundant closing parentheses. The seq returns a tree's elements as a sequence in order; the hgt gives a tree's height; balancing is the balancing factor of AVL tree. The full example is provided in Appendix \ref{['appendix:failure_cases']}.
• Figure 5: (Left) A Why3 program for binary search, with the functional correctness property in cyan and annotations in orange. (Right) One of the generated VCs for its functional correctness (simplified).

Theorems & Definitions (1)

• Definition 1