Meta introduced a new AI system that solves complexes International Math Olympiad (IMO) problems. The new model acquires 67 percent of the miniF2F validation set accuracy and is 5x more than the previous AI system.
In December 2019, Facebook built its first AI system for solving advanced mathematical equations with the help of symbolic reasoning. The first AI system solves integration problems, first-order, and second-order integration problems. The AI model demonstrated 99.7 percent accuracy for integration problems and 94 and 81.2 percent for first and second-order integration problems, respectively.
Since solving complex equations requires precision rather than an approximation, the launch of Meta’s new AI in 2022 is a milestone. Meta has used the HyperTree Proof Search (HTPS) method in its new AI system, which is trained on a dataset of successful mathematical proofs and is generalized to new or different problems. This method can collect correct proofs for the IMO problem, consisting of some arithmetic reduction to a finite number of cases.
Meta has mentioned the detailed work of the new AI system in its new research paper on HTPS that will be presented in NeurIPS 2022. The new AI system is made available with the Lean Visual Studio Code (LVSC) plugin, which allows other researchers to explore the system. Lean is a functional programming language to write correct and maintainable codes.
