Towards Mining Robust Coq Proof Patterns
summary
Plans to mine a published Coq dataset for historical breakage and repair patterns, convert Coq scripts into lightweight ASTs, apply tree differencing to extract common edits, and synthesize instantiate repair templates that are validated by actually checking the patched proofs in Coq with iterative refinement. Targets include fixing common tactic and library-renaming regressions that account for much maintenance pain and aiming for roughly 80% automated repair of routine breakages while surfacing hard cases for human patching.
AI-written summary · about
chapters (8)
- 0:00Proof maintenance challenges
- 1:27Fragility of tactical proofs
- 3:35Declarative proofs and proof terms
- 5:24Mining proof repair patterns
- 7:14Data collection for proof evolution
- 8:41Generating proof repair candidates
- 10:05Community collaboration
- 11:32Q&A
related talks
55mProving Theorems and Certifying Programs with Coq
26mData-Driven Lemma Synthesis for Interactive Proofs
32mA Survey of Weak Reasoning Assistants
07mTooling and Sharing Traceability Discussion
01h 07mSufficiently Advanced Testing
22mInducTeX: A MetaCoq plugin for typesetting inductive definitions
05m“Validating Lemmas with Rustdoc [...]”
19mPyDex: Repairing Bugs in Introductory Python Assignments using LLMs