Automatic formalization of mathematics: a path to automatic reasoning

Therefore it is natural to ask: Will we ever arrive at the point where an AI agent can learn to do reasoning as well as the best humans in the world in most established domains of mathematics. —- Christian Szegedy

This paper refers to A Promising Path Towards Autoformalization and General Artificial Intelligence

It is well known that deep learning is not very good at reasoning, and it is natural for us to think that we can test reasoning AI mathematically. But before entering into the problem, there are two obvious difficulties: (1) humans express mathematical knowledge in natural language, and the fuzziness of natural language makes it difficult for computers to understand and verify it in a mechanized way; (2) Human mathematical knowledge is scattered in a vast number of papers, and it is difficult to generate effective data sets for system training.

At the same time, the development of human basic mathematics has also encountered an obvious bottleneck, the complexity of human mathematical papers is getting higher and higher, resulting in the difficulty of verifying their correctness, often a paper review time is extremely long or even unable to review the situation.

In response to these problems, some mathematicians have developed formal mathematical languages to represent mathematical knowledge, and these formal languages represent propositions and proof processes that can be verified by fixed procedures. These mathematicians hope to verify the correctness of human mathematical knowledge and promote the development of human mathematics through computers, but the workload of translating human mathematics into formal language is very huge, and the content of the mathematical theorem library of the main formal language is very limited, and even cannot completely include the content of undergraduate mathematics.

Therefore, the need to develop a mathematical automatic formalization algorithm is particularly urgent, on the one hand, it can provide a large number of clear mathematical knowledge base for mathematical reasoning artificial intelligence, on the other hand, it can verify the correctness of human mathematical knowledge on a large scale.

简史

The idea of automatic formalization was first proposed by John McCarthy in 1961. Another early attempt was Donald Simons’ doctoral thesis in 1990. The first thorough study was carried out in Claus Zinn’s PhD thesis in 2004. None of this work has produced even a partially practical solution.

Josef Urban began working on the subject in the early 2000s. He designed the first large-scale benchmark for large-scale theoretical reasoning, motivated by the belief that reasoning in a large knowledge base of mathematical facts is a key component of any automated formalization system. In 2007, he published the groundbreaking MaLARea system for large-scale theoretical reasoning. Since then, he and Cezary Kaliszyk have been spearheading research into inference and automatic formatting of large theories.

Ref. [1]First experiments with neural translation of informal to formal mathematics [2]Exploration of neural machine translation in autoformalization of mathematics in Mizar

Partial application of AI technology to mathematics

  1. Progress of GPT-f series models in automatic reasoning: some IMO difficulty problems can be done.

    Ref. [1]Generative Language Modeling for Automated Theorem Proving [2]Mathematical Reasoning via Self-supervised Skip-tree Training [3]Proof Artifact Co-training for Theorem Proving with Language Models [4]Formal Mathematics Statement Curriculum Learning

  2. Machine learning guides human intuition and uses clustering algorithms to capture patterns in examples of knot theory and symmetric group theory, resulting in the discovery of two new theorems.

    Ref. [1]Advancing mathematics by guiding human intuition with AI

  3. A neural network solver that can solve undergraduate mathematical problems by using Python’s symbolic computation package sumpy.

    Ref. [1]A Neural Network Solves and Generates Mathematics Problems by Program Synthesis: Calculus, Differential Equations, Linear Algebra, and More

Possible technical paths

I am currently working on a data set corresponding to Lean in natural language. After obtaining the data set, I will design the methods of automatic translation theorem and proof respectively. Translation of the theorem can generally be done using the transformer class model; The translation of proof should be a reinforcement learning task, which is not very clear for the time being.

Or you can try an unsupervised approach. SeeUnsupervised Translation of Programming Languages