- Статьи
- Internet and technology
- Quick to figure it out: the new AI agent will prove theorems many times faster than mathematicians
Quick to figure it out: the new AI agent will prove theorems many times faster than mathematicians
Russian scientists have created a system that independently formulates mathematical optimization problems, selects methods for solving them, and formally proves the results. With her help, it was possible to formulate about 100 theorems, 35 of which received proofs. It takes an average of three to seven hours to prove a single AI theorem, which is many times faster than that of professional mathematicians. However, using the platform also carries certain risks. In particular, the system may give correct answers to incorrectly formulated tasks, experts warned. Whether the algorithm will be able to replace scientists in individual operations is discussed in the Izvestia article.
From iterating over methods to proof
AI Institute scientists, together with Vietnamese student Quoc Viet, have developed the LongTails software platform, capable of automating a significant part of mathematical research. The system formulates new mathematical optimization problems, selects methods for solving them, and then proves the results. It takes an agent an average of three to seven hours to prove a single theorem, which makes it possible to solve such problems many times faster than mathematicians.
In total, the researchers have already worked out about 100 theorems using the system. In 50 cases, AI proved that algorithms can work faster and more accurately than previously thought by scientists. Another 35 results turned out to be so unique that the authors will prepare separate articles on them for major international journals.
— The framework has proven more results in a couple of days than I have in my entire career. It's hard to determine how I feel about this, but it's very interesting. We will continue to prove new theorems, increase the complexity of tasks, structure them, and ensure that the algorithms found are effective in practice," said Alexander Tyurin, head of the Optimization Methods in Machine Learning research group at the AIRI Institute.
The system specializes in mathematical optimization, an area that searches for the best solution among a variety of possible options. Such methods are used in the training of neural networks, as well as in logistics, energy, engineering, chemistry and physics. The key feature of the platform is the formal verification of results using the Lean 4 language. The usual language model can produce a proof that looks convincing, but contains an error or relates to the wrong problem statement. LongTails checks whether the proof formally meets the specified conditions and the set goal.
Risks of using the platform
Experts see the main risk of such systems not so much in the errors of the proof itself, as in the possibility of getting a correct answer to an incorrectly set task.
— If the task statement was formulated by the agent, the error can be laid already at this stage. Then the perfect proof confirms the wrong result. Therefore, the responsibility for what exactly has been proven and where it is applied remains with the researcher," said Olga Yashina, Advisor to the Intellectual Property Practice at EBR Law Firm.
Another expert draws attention to the difference between formal correctness and scientific understanding. According to Denis Astafyev, founder of the SharesPro fintech platform, the proof may be perfect from the point of view of mathematics, but it is practically inaccessible to human understanding. This is not enough for the development of science: the researcher must understand why the found method works and how it can be applied in other tasks.
"The machine's ability to independently obtain mathematically correct results raises the question of how much such research depends on human understanding," he explained.
Systems that can not only provide evidence, but also explain the course of reasoning can become promising. Otherwise, the machine solves a specific mathematical problem, but does not necessarily give a person a new understanding, explained Egor Starovoitov, lead developer of MWS AI Cowork.
The main transformation will be related to the redistribution of functions. AI will take on more and more computing and technical search, while the specialist will be left with setting research tasks, building models and evaluating the scientific significance of the results, believes Mikhail Novoselov, head of the Department of Theory and Methodology of Computer Sports, Chess and Digital Technologies at RUS "GTSOLIFK".
— There is also an educational risk here. If you constantly transfer complex stages of reasoning to AI, young researchers may get less practice building evidence on their own. Therefore, training should combine working with AI and solving mathematical problems independently," explained Artur Vafin, associate professor at the Financial University under the Government of the Russian Federation.
There is no reason to talk about mass rejection of such technologies among mathematicians. As Evgeny Grigoriev, Deputy head of the Artificial Intelligence department at T1 IT Holding, noted, AI is able to take on a significant part of routine work — searching and verifying evidence, iterating over approaches and technical calculations. This allows scientists to focus on more complex tasks.
Mathematicians will be needed further
Such frameworks will change the profession of mathematics, but they will not lead to its disappearance. Even if the agent formulates tasks independently, it will be up to the person to determine which ones are important and why they should be solved, Egor Starovoitov noted. According to him, the situation resembles the appearance of calculators and computer algebra systems: some of the manual work has disappeared, but the profession itself has been preserved. Now the specialist will need not only to master the mathematical apparatus, but also to be able to correctly set tasks for AI and verify the results obtained.
— Technological progress in this case increases the requirements for a person, rather than canceling his role. The researcher will have to determine which of the many possible tasks are really of scientific value, and monitor the application of the results obtained," said political scientist Elena Shtulman.
With the development of AI, the profession of mathematics will change — both the content of the work and the areas of application of the acquired knowledge, says Ashot Margaryan, head of the Alice AI model AI training team in higher mathematics.
— In this case, AI does not replace mathematics, but acts as a good assistant to whom you can delegate the verification of certain hypotheses and routine calculations. However, creating a conceptual approach, searching for hidden logic and obtaining genuine scientific novelty is impossible without a scientist," he noted.
The experts interviewed note that the machine is able to find solutions and prove theorems faster than a human. But it is still up to the researcher to determine which problems are worth solving, why the result is important, and what new directions can follow from it.
Переведено сервисом «Яндекс Переводчик»
