Data-driven lemma synthesis for interactive proofs
Abstract
Interactive proofs of theorems often require auxiliary helper lemmas to prove the desired theorem. Existing approaches for automatically synthesizing helper lemmas fall into two broad categories. Some approaches are goal-directed, producing lemmas specifically to help a user make progress from a given proof state, but they have limited expressiveness in terms of the lemmas that can be produced. Other approaches are highly expressive, able to generate arbitrary lemmas from a given grammar, but they are completely undirected and hence not amenable to interactive usage.
Document Details
- Document Type
- Pub Defense Publication
- Publication Date
- Oct 31, 2022
- Source ID
- 10.1145/3563306
Entities
People
- Aishwarya Sivaraman
- Alex Sanchez-Stern
- Bretton Chen
- Sorin Lerner
- Todd Millstein
Organizations
- Defense Advanced Research Projects Agency
- National Science Foundation
- University of California, Los Angeles
- University of California, San Diego
- University of Massachusetts Amherst