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

arXiv: https://arxiv.org/abs/2601.18944 · HTML: https://mlsanity.com/paper/2601.18944/

## Key facts

- Cited by 4 papers in the map (data through 14 Oct 2026).
- Builds on 27 of its 83 references that are in the map.
- First posted on arXiv 26 Jan 2026.

## Builds on (most cited first, 27 of 27)

- [Qwen3 Technical Report](https://mlsanity.com/paper/2505.09388/) (2025)
- [LeanDojo: Theorem Proving with Retrieval-Augmented Language Models](https://mlsanity.com/paper/2306.15626/) (2023)
- [MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics](https://mlsanity.com/paper/2109.00110/) (2021)
- [DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decomposition](https://mlsanity.com/paper/2504.21801/) (2025)
- [PutnamBench: Evaluating Neural Theorem-Provers on the Putnam Mathematical Competition](https://mlsanity.com/paper/2407.11214/) (2024)
- [Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Proving](https://mlsanity.com/paper/2502.07640/) (2025)
- [Learning to Prove Theorems via Interacting with Proof Assistants](https://mlsanity.com/paper/1905.09381/) (2019)
- [Clover: Closed-Loop Verifiable Code Generation](https://mlsanity.com/paper/2310.17807/) (2023)
- [DafnyBench: A Benchmark for Formal Software Verification](https://mlsanity.com/paper/2406.08467/) (2024)
- [Verus: Verifying Rust Programs using Linear Ghost Types (extended version)](https://mlsanity.com/paper/2303.05491/) (2023)
- [AutoVerus: Automated Proof Generation for Rust Code](https://mlsanity.com/paper/2409.13082/) (2024)
- [GamePad: A Learning Environment for Theorem Proving](https://mlsanity.com/paper/1806.00608/) (2018)
- [TacticToe: Learning to Prove with Tactics](https://mlsanity.com/paper/1804.00596/) (2018)
- [CLEVER: A Curated Benchmark for Formally Verified Code Generation](https://mlsanity.com/paper/2505.13938/) (2025)
- [Rango: Adaptive Retrieval-Augmented Proving for Automated Software Verification](https://mlsanity.com/paper/2412.14063/) (2024)
- [HolStep: A Machine Learning Dataset for Higher-order Logic Theorem Proving](https://mlsanity.com/paper/1703.00426/) (2017)
- [FVEL: Interactive Formal Verification Environment with Large Language Models via Theorem Proving](https://mlsanity.com/paper/2406.14408/) (2024)
- [Proving the Coding Interview: A Benchmark for Formally Verified Code Generation](https://mlsanity.com/paper/2502.05714/) (2025)
- [miniCodeProps: a Minimal Benchmark for Proving Code Properties](https://mlsanity.com/paper/2406.11915/) (2024)
- [Towards Neural Theorem Proving at Scale](https://mlsanity.com/paper/1807.08204/) (2018)
- [Laurel: Unblocking Automated Verification with Large Language Models](https://mlsanity.com/paper/2405.16792/) (2024)
- [K2-Think: A Parameter-Efficient Reasoning System](https://mlsanity.com/paper/2509.07604/) (2025)
- [APE-Bench: Evaluating Automated Proof Engineering for Formal Math Libraries](https://mlsanity.com/paper/2504.19110/) (2025)
- [Deductive Verification of Unmodified Linux Kernel Library Functions](https://mlsanity.com/paper/1809.00626/) (2018)
- [RAG-Verus: Repository-Level Program Verification with LLMs using Retrieval Augmented Generation](https://mlsanity.com/paper/2502.05344/) (2025)
- [A Minimalist Proof Language for Neural Theorem Proving over Isabelle/HOL](https://mlsanity.com/paper/2507.18885/) (2025)
- [Cameleer: a Deductive Verification Tool for OCaml (extended version)](https://mlsanity.com/paper/2104.11050/) (2021)

## Built on by (most cited first, 4 of 4)

- [Pythagoras-Prover: Advancing Efficient Formal Proving via Augmented Lean Formalisation](https://mlsanity.com/paper/2606.12594/) (2026)
- [Automated Lemma Discovery in Agentic Program Verification](https://mlsanity.com/paper/2603.22114/) (2026)
- [s2n-bignum-bench: A practical benchmark for evaluating low-level code reasoning of LLMs](https://mlsanity.com/paper/2603.14628/) (2026)
- [AoA: Theorem Proving Agent over Abstract Syntax Tree of Redesigned Language](https://mlsanity.com/paper/2607.16372/) (2026)

## Abstract (arXiv)

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.