Katie Collins, a researcher at the University of Cambridge specializing in math and AI, highlights the challenge of training models for mathematics due to the limited availability of formal mathematics data online compared to informal natural language data.
Google DeepMind aimed to address this issue with AlphaProof, a reinforcement-learning-based system designed to prove mathematical statements using the formal programming language Lean. The system utilizes a fine-tuned version of DeepMind’s Gemini AI to translate math problems from natural, informal language into formal statements. This translation process created a substantial library of formal math problems with varying levels of difficulty.
Wenda Li, a lecturer in hybrid AI at the University of Edinburgh who peer-reviewed the research, emphasizes the significance of this advancement for the math community. Automating the translation of data into formal language enhances the confidence in published results and fosters greater collaboration.
AlphaProof operates alongside AlphaZero, DeepMind’s reinforcement-learning model known for mastering games like Go and chess, to tackle millions of mathematical problems. As AlphaProof solves more problems, it becomes increasingly adept at handling complex challenges.
In addition to AlphaProof, DeepMind developed AlphaGeometry 2, an improved system optimized for problems involving movements of objects and equations related to angles, ratios, and distances. Trained on more synthetic data than its predecessor, AlphaGeometry 2 is capable of addressing more advanced geometry questions.
