AlphaProof is a new reinforcement-learning based system for formal math reasoning from DeepMind. AlphaProof + AlphaGeometry 2, an improved version of DeepMind's geometry system, solved 4 out of 6 problems from this year's International Mathematical Olympiad (IMO), achieving the same level as a silver medalist.
"AlphaProof solved two algebra problems and one number theory problem by determining the answer and proving it was correct. This included the hardest problem in the competition, solved by only five contestants at this year's IMO. AlphaGeometry 2 proved the geometry problem, while the two combinatorics problems remained unsolved."
"AlphaProof is a system that trains itself to prove mathematical statements in the formal language Lean. It couples a pre-trained language model with the AlphaZero reinforcement learning algorithm, which previously taught itself how to master the games of chess, shogi and Go."
"Formal languages offer the critical advantage that proofs involving mathematical reasoning can be formally verified for correctness."
"When presented with a problem, AlphaProof generates solution candidates and then proves or disproves them by searching over possible proof steps in Lean. Each proof that was found and verified is used to reinforce AlphaProof's language model, enhancing its ability to solve subsequent, more challenging problems."
"We trained AlphaProof for the IMO by proving or disproving millions of problems, covering a wide range of difficulties and mathematical topic areas over a period of weeks leading up to the competition. The training loop was also applied during the contest, reinforcing proofs of self-generated variations of the contest problems until a full solution could be found."
The blog post seems to have revealed few details of how AlphaProof works. But it sounds like we're about to enter a new era of math proofs, where all kinds of theorems will be discovered and proved.
AI achieves silver-medal standard solving International Mathematical Olympiad problems
#solidstatelife #ai #genai #llms #reinforcementlearning #rl #mathematics #proofs
