Make up math lessons for AI, AI can prove 82% of the problems in the math database

It has to be said that scientists have been obsessed with supplementing mathematics lessons for AI recently. No, the Facebook team also joined the fun and proposed a new model,Can fully automate the proof of theorems and is significantly better than SOTA.

You know, as the mathematical theorems get more complicated,It will only get harder to prove theorems later on with humans alone. Therefore, the use of computers to demonstrate mathematical theorems has become a research focus.

OpenAI has also proposed a model GPT-f specializing in this direction before.Able to demonstrate 56% of the problems in Metamath. The latest method proposed this time,can raise this figure to 82.6%.

At the same time, the researchers say that the method takes less time, and can reduce the computational cost to one-tenth compared to GPT-f. Could it be that this AI war against mathematics is going to be a success?

or Transformer

The method proposed in this paper is an online training program based on Transformer. It can be roughly divided into three steps:

• First, pre-training in the mathematical proof library;

• Second, fine-tune the policy model on the supervised dataset;

• Third, online training strategy model and judgment model.

Specifically, it uses a search algorithm,Let the model learn from the existing mathematical proof library, and then generalize to prove more problems. Among them, there are three kinds of mathematical proof libraries, namely Metamath, Lean and a self-developed proof environment. These proof libraries are, in a nutshell, transforming ordinary mathematical languages ​​into forms that approximate programming languages.

Metamath’s main library is set.mm, which contains about 38,000 proofs based on ZFC set theory. Lean is better known,It’s Microsoft’s AI algorithm that can participate in IMO competitions. The Lean library is there to teach the algorithm of the same name all undergraduate mathematics and make it learn to prove these theorems.

The main goal of this research is to build a prover that can automatically generate a series of suitable strategies to prove the problem. to this end,Researchers propose a non-equilibrium hypergraph proof search algorithm based on MCTS.

MCTS, translated as Monte Carlo Tree Search, is often used to solve game tree problems and is well known from AlphaGo. Its operation process is to find a promising action by randomly sampling in the search space, and then expand the search tree according to this action.

This study follows a similar line of thinking. The search proof process starts from the goal g, searches down the method, and gradually develops into a hypergraph. When an empty set appears under a branch, it means that an optimal proof has been found. Finally, during backpropagation, note down the node value of the supertree and the total number of operations.

In this section,The researchers hypothesized a policy model and a judgment model. Policy models allow for sampling from judgmental models that assess the ability of the current policy to find a way to prove it. The entire search algorithm takes the above two models as a reference. Both models are Transformer models, and the weights are shared.

Next, it comes to the stage of online training. During this process, the controller sends the statement to asynchronous HTPS verification and collects training and proof data. The validator will then send training samples to the distributed trainer and periodically sync its copy of the model.

Experimental results

In the test session, the researchers compared HTPS with GPT-f. The latter is a mathematical theorem inference model previously proposed by OpenAI, which is also based on Transformer. the result shows,The model after online training can prove 82% of the problems in Metamath, far exceeding the previous record of 56.5% in GPT-f.

In the Lean library, this model can prove 43% of the theorems, which is 38% higher than SOTA. The following are the IMO test questions proved by the model.

But it’s not perfect yet. For example, in the following problem, it does not solve the problem in the easiest way,The researchers say this is because of an error in the annotation.

One More Thing

Use computers to demonstrate mathematical problems,The proof of the four-color theorem is one of the most well-known examples. The four-color theorem is one of the three major problems in modern mathematics. It proposes that “any map can use only four colors to make countries with common borders colored with different colors”.

Since the proof of this theorem is computationally intensive, no one has been able to fully demonstrate it for 100 years after it was proposed. Until 1976, on two computers at the University of Illinois, USA,After 1200 hours and 10 billion judgmentsand finally it can be demonstrated that any map only needs 4 colors to mark, which has also caused a sensation in the entire mathematics community.

In addition, as mathematical problems become more complex, it becomes more difficult to test the correctness of theorems manually. Recently, the AI ​​community has also gradually focused its attention on mathematical problems.

In 2020, OpenAI launched the mathematical theorem reasoning model GPT-f, which can be used for automatic theorem proving. This method can complete 56.5% of the proofs in the test set, surpassing the then SOTA model MetaGen-IL by more than 30%.

In the same year, Microsoft also released Lean, which can make IMO test questions, which means that AI can make unseen questions. Last year, after OpenAI added a validator to GPT-3, the effect of doing math problems was significantly better than the previous fine-tuning method, which could reach 90% of the level of primary school students.

In January of this year, a joint study from MIT + Harvard + Columbia University + University of Waterloo showed that their proposed model can do high numbers. In short,Scientists are working hard to make AI a partial student with both liberal arts and sciences.

Paper address:

https://arxiv.org/abs/2205.11491