Zulip Chat Archive

Stream: IMO-grand-challenge

Topic: AI


view this post on Zulip Jason Rute (Sep 07 2019 at 12:00):

I think the term “AI” means a lot of things to a lot of people. For one, it could just mean “write a program to solve this”. In this case that could be a imo_solver tactic written in Lean’s meta language, or a script which generates Lean code. However, it could also mean using SAT/SMT solvers and other such tools. In other ITPs, these have been built into “hammers”. Last, it could mean using machine learning—possibly neural networks and/or reinforcement learning.

view this post on Zulip Jason Rute (Sep 07 2019 at 12:00):

Does Lean currently have support, or is there going to be support, for hammer-like interfaces with powerful ATPs? Also, on the machine learning side, it seems that the most successful ML for ITP projects rely on having training data in the form of a dataset of proven theorems. This requires proof recording. Also, since Lean has so much syntactic sugar, it makes sense to try to strip that down to the bare bones in the training data, but to still keep the high-level tactic commands. Indeed the best AI for ITP projects, TacticToe, HOList, CoqGym/ASTactic, and ProverBot9001 all seem to rely on a good tactic-level recorded proofs stored in a simple to parse format. Moreover, to do reinforcement learning requires an interface which allows rapid back-and-forth between the proof-checker and some AI interface (attached to TensorFlow, PyTorch, etc. utilizing a GPU or many GPU machines). I think Google Research spent a lot of effort writing their own HOL Light kernel and interface to make it usable for reinforcement learning.

view this post on Zulip Jason Rute (Sep 07 2019 at 12:00):

I would love to see Lean with better tooling for AI, and this will better encourage users to participate. (I wrote some more rambling thoughts on AI and Lean in the AI and theorem proving stream.) I wonder if the organizers of this challenge have any plans to talk to Christian Szegedy, Josef Urban, Cezary Kaliszyk and others about how well Lean is set up for this challenge.

view this post on Zulip Daniel Selsam (Sep 07 2019 at 13:55):

I wonder if the organizers of this challenge have any plans to talk to Christian Szegedy, Josef Urban, Cezary Kaliszyk and others about how well Lean is set up for this challenge.

@Jason Rute Yes, definitely.

view this post on Zulip Daniel Selsam (Sep 07 2019 at 14:00):

I think the term “AI” means a lot of things to a lot of people. For one, it could just mean “write a program to solve this”. In this case that could be a imo_solver tactic written in Lean’s meta language, or a script which generates Lean code. However, it could also mean using SAT/SMT solvers and other such tools. In other ITPs, these have been built into “hammers”. Last, it could mean using machine learning—possibly neural networks and/or reinforcement learning.

@Jason Rute I don't think it is at all clear which if any of the existing paradigms of AI can be leveraged to win. This is one reason why I think it is a worthy grand challenge.


Last updated: Aug 05 2021 at 03:12 UTC