Neural Theorem Proving for Verification Conditions: A Real-World Benchmark
Fuente:
arXiv
Guardado en:
| Autores principales: | , , , , , , , |
|---|---|
| Formato: | Preprint |
| Publicado: |
2026
|
| Materias: | |
| Acceso en línea: | |
| Etiquetas: |
Agregar Etiqueta
Sin Etiquetas, Sea el primero en etiquetar este registro!
|
| _version_ | 1866914287142830080 |
|---|---|
| author | Xu, Qiyuan Luan, Xiaokun Wang, Renxi Leang, Joshua Ong Jun Wang, Peixin Li, Haonan Li, Wenda Watt, Conrad |
| author_facet | Xu, Qiyuan Luan, Xiaokun Wang, Renxi Leang, Joshua Ong Jun Wang, Peixin Li, Haonan Li, Wenda Watt, Conrad |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2601_18944 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | Neural Theorem Proving for Verification Conditions: A Real-World Benchmark Xu, Qiyuan Luan, Xiaokun Wang, Renxi Leang, Joshua Ong Jun Wang, Peixin Li, Haonan Li, Wenda Watt, Conrad Artificial Intelligence Programming Languages Software Engineering I.2.3; F.4.1; I.2.5; I.2.7 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. |
| title | Neural Theorem Proving for Verification Conditions: A Real-World Benchmark |
| topic | Artificial Intelligence Programming Languages Software Engineering I.2.3; F.4.1; I.2.5; I.2.7 |
| url | https://arxiv.org/abs/2601.18944 |