Isabelle and neural theorem proving

Stream: Machine Learning for Theorem Proving

[Jason Rute]

There are two (well three) papers recently on neural theorem proving for Isabelle which is great. In many ways Isabelle, with its powerful Sledgehammer was at the front of automated theorem proving applied to interactive theorem proving. But now there are works taking this to the next level by integrating neural tools into Isabelle. I have to admit I haven't looked at either of these papers in detail yet, but I want to mention them here:

[Jason Rute]

• Isabelle ENIGMA
  • Title: The Isabelle ENIGMA
  • Authors: @Zar Goertzel, Jan Jakubův, Cezary Kaliszyk, @Miroslav Olšák, Jelle Piepenbrock, @Josef Urban
  • arXiv: https://arxiv.org/abs/2205.01981
• Thor:
  • Title: Thor: Wielding Hammers to Integrate Language Models and Automated Theorem Provers
  • Authors: @Albert Jiang, @Wenda Li, @Szymon Kitowski, Konrad Czechowski, Tomasz Odrzygóźdź, Piotr Miłoś, @Yuhuai Tony Wu , Mateja Jamnik
  • Twitter announcement: https://twitter.com/AlbertQJiang
  • arXiv paper: https://arxiv.org/abs/2205.10893

[Jason Rute]

My very quick understanding is that the first uses machine learning inside Sledgehammer to improve the first order theorem prover and premise selector (lemma selector) used by Sledgehammer. This is similar to the previous ENGIMA projects but focusing on Isabelle and the Archive of Formal Proofs. The second on the other hand uses machine learning outside Sledgehammer more similar to GPT-f and other neural tactic-guiding tools to guide tactics and Sledgehammer, but also to delegate to Sledgehammer for certain tasks like premise selection. Superficially it looks like they are orthogonal and can be combined.

[Jason Rute]

The third paper is on autoformalization in Isabelle and deserves its own topic.

[Albert Jiang]

Jason Rute said:

• Isabelle ENIGMA
  • Title: The Isabelle ENIGMA
  • Authors: Zar Goertzel, Jan Jakubův, Cezary Kaliszyk, Miroslav Olšák, Jelle Piepenbrock, Josef Urban
  • arXiv: https://arxiv.org/abs/2205.01981
• Thor:
  • Title: Thor: Wielding Hammers to Integrate Language Models and Automated Theorem Provers
  • Authors: Albert Jiang, Yuhuai Tony Wu, Szymon Kitowski, Konrad Czechowski, Tomasz Odrzygóźdź, Piotr Miłoś, Yuhuai Tony Wu , Mateja Jamnik
  • Twitter announcement: https://twitter.com/AlbertQJiang
  • arXiv paper: https://arxiv.org/abs/2205.10893

I think for Thor, you meant @Wenda Li as the second author :)

[Jason Rute]

Fixed.

[Albert Jiang]

Jason Rute said:

My very quick understanding is that the first uses machine learning inside Sledgehammer to improve the first order theorem prover and premise selector (lemma selector) used by Sledgehammer. This is similar to the previous ENGIMA projects but focusing on Isabelle and the Archive of Formal Proofs. The second on the other hand uses machine learning outside Sledgehammer more similar to GPT-f and other neural tactic-guiding tools to guide tactics and Sledgehammer, but also to delegate to Sledgehammer for certain tasks like premise selection. Superficially it looks like they are orthogonal and can be combined.

I've read the Isabelle ENIGMA paper and agree with your understanding on both papers. The ENIGMA paper came out just when we were about to wrap up Thor. Otherwise we would have reached out to see if we can combine the two. It remains a future direction to get neural and symbolic components firmly weaved together in great granularity :)