For the twenty-first class, 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 talks from researchers at both Google and OpenAI about other machine learning tools for proofs!
You can find a reading guide and the discussion questions for this class below.
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.