Researchers from the team of Dr. J. Urban achieved a great success at the Championship in Automated Reasoning

In the global competition of universities and research teams, the researchers from the group Automatic reasoning and formal methods at CIIRC CTU, who participated in the development of Vampire, MaLARea, Enigma or Satallax systems, placed perfectly. The Championship in Automated Reasoning Competition (The CADE ATP System Competition) took place online in July this year.

The Vampire system was the best, winning in 3 categories (Typed First Order Theorems, First Order Theorems and First Order Non-theorems), developed by developer Martin Suda from CIIRC CTU together with colleagues from the universities of Manchester and Vienna.

The second place in the First Order Theorems category went to Jan Jakubův’s Enigma system. What more, Enigma is unique in the way it has extended the existing E system with machine learning and was able to solve 50 out of 500 more problems in the competiotion, a significant improvement over the system from which it was derived.

Very interesting from the point of view of both automated verification and CIIRC CTU is a category Large Theory Batch Problems, which was defined directly by Dr Josef Urban. In the past two years, Josef Urban, together with Chad Brown and Thibault Gauthier, had been preparing this division for the championship (the so-called GRUNGE data set). The MaLARea system developed by Urban (which also builds on Jan Jakubův’s Enigma) was able to solve more than 7,000 out of 10,000 problems in a given time frame, and it would gain first place with a lead of more than three and a half thousand solved problems. However, for ethical reasons, the MaLARea system remained out of competition, but it demonstrates the power of machine learning in the field of automated reasoning and also the fact that truly global scientific leaders in the field are conducting their research at CIIRC CTU.

How does it work at such a championship? Within each category, random mathematical problems are selected for the competition, each competition system has a fixed time frame to solve (3 or 5 minutes, with the exception of the Large Theory Batch Problems category, see below). The system that manages to solve the largest number of problems from the specified maximum in a given time frame then becomes the winner.

The already mentioned category Large Theory Batch problems is intended primarily for machine learning. There is rather lengthy time limit of 24 hours to solve the problem, the system can return and progress from the easiest to more complex tasks and at the same time allows the system to learn from its success or failure. This category contains problems arising in large mathematics and software verification projects.

The Typed First Order Theorems category contains a selection of problems formulated in higher order logic. This is one of the most common formalisms used to verify large mathematical proofs and complicated software.

Examples of problems from the standard HOL4 library (GRUNGE: A Grand Unified ATP Challenge) are used at the championship. To put it very simply, competition systems learn advanced mathematics and gradually move closer to an „automatic mathematician“, which can lead to fundamental results in various applications.

More information about the championship can be found here: http://www.tptp.org/CASC/J10/

System teams with CIIRC participation:

MaLARea:

Urban, J. (CIIRC, CTU, Prague, Czech Republic)
(Incl. systems ENIGMA, E-prover, SPASS, Vampire, Paradox, Mace – Jan Jakubuv, Cezary Kaliszyk, Bartosz Piotrowski, Stephan Schulz, Mirek Olšák)

Enigma:

Jakubuv, J. (CIIRC, CTU, Prague, Czech Republic)
Urban, J. (CIIRC, CTU, Prague, Czech Republic)
Chvalovský, K. (CIIRC, CTU, Prague, Czech Republic)
Piotrowski, B. (CIIRC, CTU, Prague, Czech Republic)
Olšák, M. (University of Innsbruck, Innsbruck, Austria)
Suda, M. (CIIRC, CTU, Prague, Czech Republic)
(Incl. system E-prover (http://www.eprover.org/)
Schulz, S. (DHBW Stuttgart, Germany))

Vampire:

R. Giles Reger (University of Manchester, Manchester, UK)
Suda, M. (CIIRC, CTU, Prague, Czech Republic)
Voronkov, A. (University of Manchester, Manchester, UK)
Kovacs, L. (TU Wien, Vienna, Austria)
Evgeny Kotelnikov, Martin Riener, Michael Rawson, Bernhard Gleiss,
Jakob Rath, Ahmed Bhayat, Petra Hozzova, Johannes Schoisswohl

Satallax:

Brown, C. (CIIRC, CTU, Prague, Czech Republic)
Färber, M. (University of Innsbruck, Innsbruck, Austria)

ATPBoost:

Piotrowski, B. (CIIRC, CTU, Prague, Czech Republic)
Josef Urban, Stephan Schulz