We all still keep in mind Mathematical Olympiad. Pupils try to correctly solve as many mathematical problems as possible in the given time. The world championship in automatic reasoning works like that.
More specifically, it is The CADE ATP System Competition, which has been organized by Dr. Geoff Sutcliffe from the University of Miami, and which is part of the international conference on automated reasoning (The 29th International Conference on Automated Deduction took place on July, 1 – 4, 2023 in Rome, Italy). Only the tasks at the championship are not formulated in a natural but machine-intelligible language of mathematical logic, and instead of students, they are solved by programmed systems with elements of artificial intelligence, which, with a little imagination, could be compared to an automatic mathematician. The systems try to solve a maximum number of randomly selected math problems within a time limit of 3 or 5 minutes.
However, the championship in automatic reasoning is not just a competition of algorithms or a battle for who can push the limits of this scientific field by the biggest chunk. Automatic reasoning methods can lead to important results in their applications – provers could facilitate or ease the work of mathematicians, logicians, programmers, system designers (software, hardware, communication protocols), etc. The latter is especially important for systems whose correct and reliable functioning fundamentally affects the human lives, such as in medicine or transport.
From the long term perspective, one of the very successful systems at the championship has been Vampire system, in which Martin Suda, Head of the automatic reasoning group at CIIRC CTU, also participates. Vampire and its latest version 4.8 won the categories First-order Non-theorems, Typed First-Order Non-Theorems, Typed First-order Theorems and also the category Higher-order Theorems. The last-mentioned category currently represents an interesting challenge for scientists in the field of higher-order logic, which is far richer in expression than the standardly studied first-order logic, but at the same time, thinking in it is so much more complex that it was considered unsuitable for automation until recently.
In addition to Martin Suda, who created a portfolio of strategies, Ahmed Bhayat of the University of Manchester was particularly active in developing the Vampire system for higher-order logic.
Results can be found HERE.
Source: the Vampire team
