## Reading

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**.