The Vampire project, on which Martin Suda of the CIIRC is also working, is constantly evolving and innovating to stay on the cutting edge of the rapidly evolving field of automated reasoning, a subfield of classical artificial intelligence. Last year, Vampire Prover succeeded at the CASC 12th International Joint Conference on Automated Reasoning with its Vampire 4.8 version, and at this year’s prestigious IJCAR 2024 conference, to be held in Nancy, France, in early July 2024, Martin Suda even has three oportunities in the form of three accepted research papers, each of which is related in some way to the improvement of Vampire Prover. Congratulations!
Martin Suda’s research team has recently been focusing mainly on improving automatic provers through the integration of statistical artificial intelligence techniques, i.e. mainly machine learning. However, the three accepted papers this time are more traditional in their focus.
What’s new in the team of automated reasoning?
Martin Suda and his colleagues aren’t slacking off and are taking automatic reasoning research further. Together with colleague Ahmed Bhayat (formerly at the University of Manchester, now heading into the commercial sphere to capitalise on his experience), they recently completed a seven-page research paper that was accepted for presentation at IJCAR 2024 – International Joint Conference on Automated Reasoning, and introduced a new version of the Vampire automated prover, which has implemented a key innovation: extending its capabilities to support proving in higher-order logic. In the CASC’s main division of the competition, which focuses on proving first-order logic, Vampire is one of the regular and long-standing dominant participants. Martin Suda hopes that innovations in this domain will ensure a repeat of this success this year.
Another accepted paper at IJCAR 2024 is a joint paper by Martin Suda and his colleagues Sólrún Einarsdóttir, Nicholas Smallbone and Moy Johansson from Chalmers University in Gothenburg, Sweden, and Marton Hajda from TU Wien, Austria. Together they are working on improving the support for mathematical induction in the Vampire prover so that mathematical induction can be automated completely.
The third accepted paper for presentation at the IJCAR 2024 conference is a joint work with students Filip Bártek (CIIRC and FEL CTU) and Karel Chvalovský (CIIRC), who undertook an extensive analysis on the topic of proving strategies and how strategies can be composed into complete schedules to achieve the best performance on unknown problems, and to make these schedules as compact as possible in time. Part of the research involved investigating an algorithm that can compose strategies into schedules with specific characteristics. One of these characteristics is that the system is supposed to remember the solutions that were discovered during training. Furthermore, the system must perform well in the presence of noise, errors, outliers, or other imperfections in the data it is working with so that it is well transferable to problems not seen during training. The submitted paper also addressed the likelihood of expecting good performance even in such a scenario.
The Vampire prover, co-developed by Martin Suda (head of the automated reasoning team at CIIRC), is at the cutting edge of automated theorem proving. Vampire is known for its efficiency in solving complex problems in first-order logic, and its importance in the fields of computer science, mathematics and artificial intelligence is undeniable. This tool stands out for its advanced implementation of algorithms and techniques, which enables efficient solution of even very challenging problems. Its flexibility and wide application in various fields such as computer science, mathematics and artificial intelligence show its importance as a tool for automated theorem proving. Last year, Vampire 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 presents an interesting challenge for researchers. Higher-order logic is much richer in expression than the standard first-order logic studied, but at the same time, reasoning in it is so much more complex that it was considered unsuitable for automation until recently.
About the IJCAR Conference:
IJCAR 2024, the International Conference on Automated Reasoning, is a prestigious event in the research community that focuses on the latest research and developments in automated reasoning and related challenges. This conference provides a platform for presenting advanced research work, discussing innovations and sharing knowledge among expert communities. It is a key meeting for researchers, academics and professionals in the fields of computer science, mathematics and artificial intelligence. For more information, visit the conference website. The conference will take place in early July in Nancy, France at the INRIA research center under the University of Lorraine.
About the CASC competition:
The CASC (CADE ATP System Competition) is an annual evaluation of fully automatic theorem proving (ATP) systems in classical logic, essentially a world championship for such systems. CASC is part of every CADE and IJCAR conference, which are the main forums for presenting new research in all aspects of automated deduction. This competition is an important platform for evaluating the capabilities of ATP systems and motivating research and development of robust ATP systems that are easy and useful to use in applications.
