mlsanityData to 14 Oct 2026

Generating Correctness Proofs with Neural Networks

arXiv 1907.07794 ↗First posted 17 Jul 2019cs.PLcited by 37

Not on the map. Why?

Abstract (arXiv)

Foundational verification allows programmers to build software which has been empirically shown to have high levels of assurance in a variety of important domains. However, the cost of producing foundationally verified software remains prohibitively high for most projects,as it requires significant manual effort by highly trained experts. In this paper we present Proverbot9001,a proof search system using machine learning techniques to produce proofs of software correctness in interactive theorem provers. We demonstrate Proverbot9001 on the proof obligations from a large practical proof project,the CompCert verified C compiler,and show that it can effectively automate what were previously manual proofs,automatically producing proofs for 27.5% of theorem statements in our test dataset, when combined with solver-based tooling. Without any additional solvers,we exhibit a proof completion rate that is a 4X improvement over prior state-of-the-art machine learning models for generating proofs in Coq.

Key facts. Cited by 37 papers in the map (data through 14 Oct 2026). First posted on arXiv 17 Jul 2019.

Builds on

No reference list yet.

Built on by

Cited by year (2026 to 14 Oct)

Citing papers per year: 2021: 3; 2022: 0; 2023: 3; 2024: 16; 2025: 6; 2026: 9.

37 papers.

Sort:

By area:

  1. 2024PutnamBench: Evaluating Neural Theorem-Provers on the Putnam Mathematical Competitioncited by 165
  2. 2021Proof Artifact Co-training for Theorem Proving with Language Modelscited by 132
  3. 2023Baldur: Whole-Proof Generation and Repair with Large Language Modelscited by 119
  4. 2023An In-Context Learning Agent for Formal Theorem-Provingcited by 82
  5. 2024Formal Mathematical Reasoning: A New Frontier in AIcited by 81
  6. 2024A Survey on Deep Learning for Theorem Provingcited by 57
  7. 2024AutoVerus: Automated Proof Generation for Rust Codecited by 49
  8. 2021TacticZero: Learning to Prove Theorems from Scratch with Deep Reinforcement Learningcited by 37
  9. 2024Rango: Adaptive Retrieval-Augmented Proving for Automated Software Verificationcited by 27
  10. 2024Proof Automation with Large Language Modelscited by 22
  11. 2024Towards Neural Synthesis for SMT-Assisted Proof-Oriented Programmingcited by 20
  12. 2024miniCodeProps: a Minimal Benchmark for Proving Code Propertiescited by 18
25 more
  1. 2023Can Transformers Learn to Solve Problems Recursively?cited by 17
  2. 2024Graph2Tac: Online Representation Learning of Formal Math Conceptscited by 15
  3. 2024Transformer-Based Models Are Not Yet Perfect At Learning to Emulate Structural Recursioncited by 14
  4. 2024CoqPilot, a plugin for LLM-based generation of proofscited by 11
  5. 2024Cobblestone: A Divide-and-Conquer Approach for Automating Formal Verificationcited by 9
  6. 2024Learning Guided Automated Reasoning: A Brief Surveycited by 7
  7. 2025Agentic Verification of Software Systemscited by 6
  8. 2025RocqStar: Leveraging Similarity-driven Retrieval and Agentic Systems for Rocq generationcited by 4
  9. 2025LeanTutor: Towards a Verified AI Mathematical Proof Tutorcited by 4
  10. 2021Graph Contrastive Pre-training for Effective Theorem Reasoningcited by 3
  11. 2024QEDCartographer: Automating Formal Verification Using Reward-Free Reinforcement Learningcited by 3
  12. 2025A Case Study on the Effectiveness of LLMs in Verification with Proof Assistantscited by 3
  13. 2024Application of AI to formal methods - an analysis of current trendscited by 2
  14. 2026Automated Lemma Discovery in Agentic Program Verificationcited by 2
  15. 2024The Tactician's Web of Large-Scale Formal Knowledgecited by 1
  16. 2025ProofWala: A Framework for Multilingual Proof Data Synthesis and Theorem-Provingcited by 1
  17. 2025Hierarchical Attention Generates Better Proofscited by 1
  18. 2026Neuro-Symbolic Proof Generation for Scaling Systems Software Verificationcited by 1
  19. 2026Harnessing Code Agents for Automatic Software Verificationcited by 1
  20. 2026LeanTutor: Towards a Verified AI Mathematical Proof Tutorcited by 0
  21. 2026ProofSketcher: Hybrid LLM + Lightweight Proof Checker for Reliable Math/Logic Reasoningcited by 0
  22. 2026Can Open-Weight LLMs Produce Kernel-Verified Coq Proofs? A Pilot Studycited by 0
  23. 2026PROVE-RT: Generating Mechanized Theorem Prover Scripts for Real-Time Systems using LLMscited by 0
  24. 2026Governed Deduction: Policy-Grounded Premise Authorization Beyond Relevancecited by 0
  25. 2026ProsaBuddy: Assisting Mechanized Real-Time Schedulability Analysis with LLM-based Agentscited by 0