Class 23: Language Models for Proofs

For the twenty-third class, we will skim two papers: Generative Language Modeling for Automated Theorem Proving [PDF] by Stanislas Polu and Ilya Sutskever, and Mathematical Reasoning via Self-supervised Skip-tree Training [PDF] by Markus N. Rabe, Dennis Lee, Kshitij Bansal, and Christian Szegedy.

We are super lucky to have two guest speakers today---Stanislas Polu and Christian Szegedy! So skimming these papers is mostly a way to prepare for their short talks, so it's easier to follow and ask informed questions. We will have time for an open discussion after the talk and Q&A.

You can find a reading guide and the discussion questions 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.

Since this is to prepare for two talks, I recommend focusing just on understanding enough to follow the talk and asked informed questions to the speaker. This is especially true since there are two papers and two speakers this week, which is unusual. So perhaps just skim enough to get some familiarty with some of Stan's work and some of Christian's work. Again, it may help to focus on understanding something you find interesting, or on thinking of questions to ask the speaker.

Since we have two guest speakers, this week will be a bit different, just like it was when Leonidas gave a talk. Please write a short paragraph as a comment in the class forum thread with a single question or comment you would relay to each speaker (so, two questions or comments total) based on the corresponding reading. It's okay if the speaker ends up answering the question or addressing the comment in the talk---sometimes that's actually a good sign!

Here are some example things you may wish to include in such a question or comment:

1. Confusions about how things work, including technical details.
2. Ideas for future work---and questions about whether the speaker has thought about implementing them.
3. Concerns for how things may go wrong, and questions about how the speaker handles those situations.
4. Curiosities about things you found particularly impressive or interesting, and would like to hear a lot more about.

I strongly encourage you to ask questions after the talk, though it's fine if they are not the questions you originally write in the discussion board. You may want to look at other people's responses before class in order to shape the discussion. And again remember that you need to write just one paragraph to get credit, though you are free to write more if interested.