Data-Driven Lemma Synthesis for Interactive Proofs
summary
A tool called lfind as a Coq tactic reduces lemma synthesis to a data-driven program synthesis problem: it generalizes a stuck goal, generates input/output examples from the proof state, fills lemma holes with an example-based synthesizer, filters candidates with property-based testing, and ranks results. Evaluation across 232 benchmark locations from four suites finds useful lemmas in 68% success rate, often matching human lemmas or enabling a full proof; it uses myth synthesizer and QuickCheck and averages about five minutes per query (category‑one stops in ~1 minute).
AI-written summary · about
chapters (10)
- 0:00Foundational verification intro
- 2:52How verification works
- 4:17Goal of lemma synthesis
- 6:00L5 lemma synthesis tool
- 8:26Lemma synthesis challenges
- 13:21L5 performance benchmarking
- 16:55Runtime and optimizations
- 17:58Related work and limits
- 18:41Future directions for L5
- 19:01Conclusion and Q&A
related talks
47mBig Ideas in Program Synthesis
38mProgram Synthesis: A Dream Realized?
55mProving Theorems and Certifying Programs with Coq
16mJust-in-Time Learning for Bottom-Up Enumerative Synthesis
40mType-Driven Program Synthesis
16mFeedback-Driven Semi-supervised Synthesis of Program Transformations
40mAdvances in Deep Learning for Mathematical Theorem Proving
19mTowards Mining Robust Coq Proof Patterns