For this, we will read Diversity-Driven Automated Formal Verification [PDF] [DOI] by Emily First and Yuriy Brun.
This paper takes a look at tactic prediction models---models that predict the next tactic in your proof---in the Coq proof assistant. Traditionally in this space, researchers use benchmarks to measure the success of these proof models, with higher scores (more proofs proven) corresponding to better results. But this paper shows that different models don't just prove more or fewer proofs---they prove different proofs. So, by bringing diverse models together, you get better performance than with any single model---by a lot!
Machine learning tools for proofs are surging in popularity these days. Next week, you'll see a talk from a researcher at Google about other machine learning tools for proofs!
You can find a reading guide and the discussion questions for this class below. The public version of the slides for this class are here.
Please note that this is due the morning before class, so that we can discuss it in person. And please install the artifact before Thursday's class.