A Case Study on the Effectiveness of LLMs in Verification with Proof Assistants
summary
Evaluation uses two Rocq codebases hs-to-coq (187 proofs) and Verdi (579 proofs), calling LLMs (GPT-4o-mini and DeepSeek/DeepSec family) once per goal and requiring Coq check to QED without admits. Results show 51–52% success on hs-to-coq and ~30% on Verdi, with success rising when external dependencies and prior in-file lines are provided and crashing when omitted. Token costs reach 3,300–7,000 tokens per proof. LLMs produce concise, sometimes smarter proofs but also make odd repeated or syntax mistakes.
AI-written summary · about
chapters (15)
- 0:00Software verification intro
- 1:05Rock proof assistant
- 2:10Automated proof challenges
- 3:55Study setup and selection
- 5:00LLM dependencies and context
- 6:07Models and ablations
- 6:51Key results and accuracy
- 7:35Context and syntax impact
- 8:38Cost and token limits
- 9:20LLMs copying proofs
- 10:23Project structure effects
- 11:06Proof quality evaluation
- 13:56Limitations and failures
- 14:18Conclusions and future work
- 16:45Q&A
related talks
53mSemantics-based program manipulation in the age of LLMs
22mTowards Verified Code Reasoning by LLMs
01h 01mDiscussion
01h 03mImproved Assistance for Interactive Proof
26mInteractive Theorem Provers for Proof Education
01h 02mHow can Machine Learning Help Formal Proving ?
25mEvaluating An LLM's Ability To Code
35mEvaluating LLM systems: the nuts and bolts