Discussion: Posts on AI, Lean, Mathematics

Stream: Machine Learning for Theorem Proving

[Siddhartha Gadgil]

Over the last few months I wrote three longish posts in my blog on AI-Lean-Mathematics and shared them in other fora. Am sharing them here in case of interest as well as for comments:

• When AI struck Gold at the Maths Olympiad
• Integrating AI with the Lean Prover: How and Why
• Mathematics as Natural Science in the Era of AI - posted a couple of days ago

[Shreyas Srinivas]

I find the first blogpost’s dunk on symbolic AI extremely condescending and at least partly ill-informed.

[Shreyas Srinivas]

For one thing, in the ETP, we found modern AI next to useless while classical ATPs excelled. I am involved in another project where modern AI has not been super effective but we cracked an open problem with a sat solver. Neurosymbolic AI is an active area of research. Secondly as you yourself point out LLMs tend to generate and use Python programs for tasks. That’s explicitly symbolic and is done because by themselves LLMs can’t even compose functions properly (it’s a bit more complicated, but that’s the gist).

Classical AI is all around you. You might use lake for working with lean. It has and will eventually have an even more complex dependency management system. You use git which produces diffs that somehow magically match the edits you make to a file. You use lean tactics to write proofs. All that is the product of research in GOFAI. Lean integrates SMT solvers through lean SMT and ships with cadical, a SAT solver. They just don’t get labelled AI because LLMs have hijacked that term.

Outside math, even today, many business use cases of AI are served by traditional ML algorithms. Google maps is not using modern AI for navigation.

[Siddhartha Gadgil]

@Shreyas Srinivas I apologise and should clarify that thus was definitely not a dunk on symbolic AI. I am a great admirer of SAT/SMT solver, grind, work of McCune etc

[Siddhartha Gadgil]

I fully appreciate how apply and other such tactics depend on discrimination trees.

[Siddhartha Gadgil]

My "dunk" was on some individuals who refuse to accept that there are some domains where symbolic AI works well and others where learning is better. This is too public so I will clarify in a DM.

[Shreyas Srinivas]

What I am trying to say is they aren’t entirely wrong. Most deployed AI systems use a hybrid of several AI paradigms. An LLM that formulates a SAT instance and returns the result of a SAT solver is probably going to be more effective at systematically tackling a problem than one that just uses a neural net

[Shreyas Srinivas]

And when you start factoring in energy costs, then in most use cases traditional AI, including traditional learning algorithms will outdo purely deep learning based approaches. In fact in deep learning, ideas like reinforcement learning come from the symbolic world iirc

[Siddhartha Gadgil]

"They" is ambiguous. In my own work too I depend on "grind" and other symbolic systems for completing proofs. I strongly believe that there are many cases where symbolic AI is much better than Deep learning, and many other cases where hybrid systems are the best.

[Shreyas Srinivas]

Fair. But what I am trying to get at is that most AI systems are not purely “learning” or symbolic. They are hybrid systems: either they stitch multiple tools together or their architectures are inspired by each other.

[Siddhartha Gadgil]

However, I do say that there are people from the symbolic AI crowd (cognitive rather than CS side) who have become prominent intellectuals for so called scepticism which is really fraud. These are not people talking about hybrid systems or what works best where.

[Siddhartha Gadgil]

Shreyas Srinivas said:

Fair. But what I am trying to get at is that most AI systems are not purely “learning” or symbolic. They are hybrid systems: either they stitch multiple tools together or their architectures are inspired by each other.

Entirely agree. Did not mean to convey anything different.

[Wrenna Robson]

Had a go with getting Claude to look at my personal repo today and suggest changes. Some impressive stuff but it is not great at proof writing in my view. They work though!

[Ralf Stephan]

Use Gemini to make a plan for the proof. Copy it in a text/md file. Then ask Claude to use the plan file to write the overall structure of the proof, but don't prove yet. Then use the lean skill by cameronfreer/lean4-skills in Claude to fill the sorries. The more context you give LLMs the better. Finally use the skill to golf the result.