Read an article in MIT Tech Review (Google’s DeepMind’s new AI systems can solve complex geometry problems) about AlphaGeometry which is a new AI tool that DeepMind has come up with that can be used to solve geometry problems. The article was referring to a Nature article (Solving olympiad geometry without human demonstrations) about the technology.
DeepMind has tested AlphaGeometry on International Mathematics Olympiad (IMO) geometry problems and have shown that it was capable of performing expert level geometry proofs.
There’s a number of interesting capabilities DeepMind used in AlphaGeometry. But the ones of most interest from my perspective
- How they generated their (synthetic) data to train their solution.
- Their use a Generative AI LLM which is prompted with a plane geometry figure, theorem to prove and generates proof steps and if needed, auxiliary constructions.
- The use of a deduction rule engine (DD) plus algebraic rule engine (AR), which when combined into a symbolic engine (DD+AR) can exhaustively generate all the proofs that can be derived from a figure.
First the data
DeepMind team came up with a set of rules or actions that could be used to generate new figures. Once this list was created it could randomly select each of these actions with some points to create a figure.
Some examples of actions (given 3 points A, B and C):
- Construct X such that XA is parallel to BC
- Construct X such that XA is perpendicular to BC
- Construct X such that XA=BC
There’s sets of actions for 4 points, for 2 points, actions that just use the 3 points and create figures such as (isosceles, equilateral) triangles, circles, parallelograms. etc.
With such actions one can start out with 2 random points on a plane to create figures of arbitrary complexity. They used this to generate millions of figures.
They then used their DD+AR symbolic engine to recursively and exhaustively deduce a set of all possible premises based on that figure. Once they had this set, they could select one of these premises as a conclusion and trace back through the set of all those other premises to find those which were used to prove that conclusion.
With this done they had a data item which included a figure, premises derived from that figure, proof steps and conclusion based on that figure or ([figure], premises, proof steps, conclusion) or as the paper uses (premises, conclusion, proof steps). This could be transformed into a text sequence of <premises> <conclusion> <proof steps>. They generated 100M of these (premises, conclusion, proof steps) text sequences
They then trained their LLM to input premises and conclusions as a prompt to generate proof steps as a result. As trained, the LLM would accept premises and conclusion and generate additional proof steps.
The challenge with geometry and other mathematical domains is that one often has to add auxiliary constructions (lines, points, angles, etc.) to prove some theory about a figure.
The team at DeepMind were able to take all the 100M <premises> <conclusion> <proof steps> they had and select only those that involved auxiliary constructions in their proof steps. This came down to 9M text sequences which they used to fine tune the LLM so that it could be used to generate possible auxiliary constructions for any figure and theorem
AlphaGeometry in action
The combination of (DD+AR) and trained LLM (for auxiliary constructions) is AlphaGeometry.
AlphaGeometry’s proof process looks like this:
- Take the problem statement (figure, conclusion [theorem to prove]),
- Generate all possible premises from that figure.
- If it has come up with the conclusion (theorem to prove), trace back and generate the proof steps,
- If not, use the LLM to add an auxiliary construction to the figure and recurse.
In reality AlphaGeometry generates up to 512 of the best auxiliary constructions (out of an infinite set) for the current figure and uses each of these 512 new figures to do an exhaustive premise generation (via DD+AR) and see if any of these solves the problem statement.
Please read the Nature article for more information on AlphaGeometry.
~~~~
IMHO what’s new here is their use of synthetic data to generate millions of new training datums, fine tuning their LLM to produce auxiliary constructions, combining the use of DD and AR in their symbolic engine and then using both the DD+AR and the LLM to prove the theorem.
But what’s even more important here is that a combination of methods such as a symbolic engine and LLM points the way forward to create domain specific intelligent agents. One supposes, with enough intelligent agents, that could be combined to work in tandem, one could construct an AGI ensemble that masters a number of domains.
Picture Credit(s):
- From Nature article, Solving olympiad geometry without human demonstrations
- From Euclid’s proof of Pythagorean Theorem
