Meta AI Has Built A Neural Theorem Prover That Has Solved 10 International Math Olympiad (IMO) Problems — 5x More Than Any Previous Artificial Intelligence AI System

The scientific world has long acknowledged that proving mathematical theorems is an essential first step in developing artificial intelligence. To prove the truth or falsity of a conjecture, one must use symbolic thinking and sort through an unlimited number of alternatives. These tasks are beyond the capabilities of even the most sophisticated AI systems.

The state of the art in artificial intelligence today is to create machines that can “solve at once” or come up with a whole answer to a problem in a single go. However, this is not how most individuals approach difficult situations. Mathematical reasoning is significantly more challenging to formalize and measure. 

Meta AI has made an important development at the intersection of artificial intelligence and mathematics. The neural theorem prover developed by the team has completed five times as many IMO problems as any other AI system before it, totaling ten. Concerning miniF2F, a popular mathematics test, the AI model outperforms the state of art by 20% and outperforms Metamath by 10%.

The HyperTree Proof Search (HTPS) approach developed by the team is taught to generalize from a dataset of correct mathematical proofs to completely novel challenges. Using some arithmetic reduction to a finite number of examples, it could deduce a proper proof for an IMO problem.

The neural theorem proved required to link a “state” with an existing (incomplete) understanding of the problem so that it might behave more like a human. Initially, the researchers used a reinforcement learning strategy integrated with pre-existing proving tools like Lean.

The “present state” of the (unfinished) proof is considered a node in a graph, and each subsequent step is an edge. This allows visualization of the proof as a whole. Proving assistants use a deductive reasoning process to make this method feasible. 

A chess-playing AI requires a similar mechanism: the ability to assess the strength of a given chess position, in this case, a proof state. To achieve this, the team adopted a strategy reminiscent of a Monte Carlo tree search (MCTS), in which the model iteratively estimates the following:

1. A set of plausible counterarguments to use in a given proof state
2. The result of the proof after a fixed number of counterarguments have been presented.

This enables an online-training procedure that significantly improves the performance of the initial pretrained model on specific problems.

As a result, the proposed method outperforms the currently published state-of-the-art by 20% on the Minif2f validation set accuracy and solves ten previously unsolved IMO problems. The team hopes their work will help the community build upon their work so that we can all make even more rapid strides forward in this fascinating field.

Check out the paper, tool, and reference article. All Credit For This Research Goes To Researchers on This Project. Also, don’t forget to join our Reddit page and discord channel, where we share the latest AI research news, cool AI projects, and more.