Math-AI@ICLR

Stream: Machine Learning for Theorem Proving

[Jason Rute]

There is a workshop tomorrow on Math and AI. I won't personally be attending (I have work), but I look forward to reading the papers and posters and watching the talks when they appear on YouTube in about a month. There are some big names in deep learning there (Bengio, Szegedy), as well as mathematics (Gowers). Also, a lot of familiar faces giving talks and papers, like Josef Urban, Markus Rabe, @Daniel Selsam, @Stanislas Polu, @Yuhuai Tony Wu, @Minchao Wu, and @Jesse Michael Han (talking about Lean GPT-f or course :smile:).

[Yuhuai Tony Wu]

Thanks Jason for helping to advertise the workshop! Yes -- to attend the workshop you need to register at https://iclr.cc/Register/view-registration. You can then follow the program at https://iclr.cc/virtual/2021/workshop/2124.

I would like to specifically mention the panel discussion tomorrow at 10am PT/ 1pm ET. It'll be a discussion on general reasoning, the role of math in general intelligence, and the challenges ahead. We will leave 10-20 min in the end for questions from the audience. You can join zoom or leave questions on the rocket chat.

The panel features Fields Medalist Tim Gowers, Turing Award winner Yoshua Bengio, neural network founding father Jay McClelland, Cambridge AI Professor Mateja Jamnik, neural network guru Christian Szegedy, formal reasoning expert Josef Urban, and math philosopher Alison Pease.

Hope to see you there!

[Jason Rute]

Some things which look interesting to me in the papers and posters:

• Proof Artifact Co-training for Theorem Proving With Language Models of course! (Although I would recommend looking at the arXiv version or the Harvard YouTube talk. Or Jesse's talk when it becomes available.)
  
• @Daniel Selsam has a paper and poster about his non-deterministic tactics. I look forward to learning more about how those actually work (especially now that the examples seem to be written in Lean code).
• I'm particularly interested in the REFACTOR paper where they extract "Modular and Reusable" theorems from MetaMath proofs.
• A lot of papers on transformers and mathematical tasks.
• "Pretrained Transformers as Universal Computation Engines " is a really interesting paper. The main idea is that a pertrained Transformer model (an advanced type of language model) are good for all sorts of things having nothing to do with the original task it was trained on. Also like pretrained image models, one can get away with just fine tuning on a much smaller subset of parameters. (Here is a video on the paper.)
  
• Also, in a similar idea is the LIME paper, which is a particular mathematical method of pertaining transformers on a synthetic dataset. (It reminds me of another paper where they pretrain image models on synthetic fractals. Maybe we can get away with having pretrained language models which don't contain data, just synthetically created computational primitives.)

As for the invited talks, I'm always excited to hear what Google (@Markus Rabe) and OpenAI (@Stanislas Polu) have been up to. The panel discussion also looks pretty interesting.

Actually, I have to admit all the papers and invited talks look really interesting. (I'm starting to really regret not taking off work to attend this virtual workshop. :frown:.)

[Daniel Selsam]

OpenAI has an interesting one on "grokking". The picture says it all: grokking.png Wild.

[Yuhuai Tony Wu]

Something I'd like to mention about the REFACTOR work @Jason Rute mentioned. One of the inspiration of the work also comes from dreamcoder, where we found that the algorithm for extracting reusable components is very hard to scale to realistic problems (it's using something called fragment grammer -- check their supplementary materials for details). We instead went with a data-driven way, by creating synthetic data points to train a GNN agent for extracting reusable components. Hence it might be interesting for people who were discussing the dreamcoder paper on another thread of this stream.

[Daniel Selsam]

Yuhuai Tony Wu said:

One of the inspiration of the work also comes from dreamcoder, where we found that the algorithm for extracting reusable components is very hard to scale to realistic problems

Which variables did you find it scaled poorly in? The beam-search abstraction algorithm of S4.5.3 is at least nominally linear in the number of programs/proofs.

[Yuhuai Tony Wu]

We did some experiments with his repo: https://github.com/ellisk42/ec/tree/master/dreamcoder, and I remember the algorithm couldn't cope with large programs/graphs, and also generated poor fragments after all. Also to me the experiments presented in the paper is quite toy-ish, I would guess this is their bottleneck.

[Jason Rute]

I also had trouble with that step in their repo. I was running out of memory if I had more than 20 examples. Honestly I didn’t troubleshoot it much and could have went to a higher resource machine, so I wasn’t sure if it was just user error on my part.

[Jason Rute]

@Daniel Selsam I wonder how that Grokking paper is related to the double descent phenomenon

[Jason Rute]

Yuhuai Tony Wu said:

We did some experiments with his repo: https://github.com/ellisk42/ec/tree/master/dreamcoder, and I remember the algorithm couldn't cope with large programs/graphs, and also generated poor fragments after all. Also to me the experiments presented in the paper is quite toy-ish, I would guess this is their bottleneck.

Do you think your REFACTOR approach could fit into a program synthesis engine (similar in purpose to DreamCoder), but one that scales beyond "toyish" examples? I have been collecting problems that I think would be a good test of a DreamCoder-like-system.

[Yuhuai Tony Wu]

Jason Rute said:

Yuhuai Tony Wu said:

We did some experiments with his repo: https://github.com/ellisk42/ec/tree/master/dreamcoder, and I remember the algorithm couldn't cope with large programs/graphs, and also generated poor fragments after all. Also to me the experiments presented in the paper is quite toy-ish, I would guess this is their bottleneck.

Do you think your REFACTOR approach could fit into a program synthesis engine (similar in purpose to DreamCoder), but one that scales beyond "toyish" examples? I have been collecting problems that I think would be a good test of a DreamCoder-like-system.

Yes definitely, we started doing some early experiments with @Albert Jiang, but we didn't finish the effort -- happy to chat if someone wants to continue our effort.

[Jason Rute]

How did the conference workshop go? Any highlights?

[Oliver Nash]

Jason Rute said:

Although I would recommend looking at the arXiv version or the Harvard YouTube talk. Or Jesse's talk when it becomes available.)

I just watched this talk. Very nice. I laughed out loud when I saw that you used my "Human-written proof" as the example (c.45:00) of where GPTf crushed it!

[Jason Rute]

The talks for Math-AI are out now. I haven't had a time to watch them yet. https://mobile.twitter.com/Yuhu_ai_/status/1402832506177609729

All talks and the panel discussion is now released at https://iclr.cc/virtual/2021/workshop/2124. The panel discussion starts at 4:33:47. Enjoy! https://twitter.com/Yuhu_ai_/status/1390649168868245504

- Yuhuai (Tony) Wu (@Yuhu_ai_)