Malleable (ML-able) Theorem Proving Architectures

Project Summary

Encouraged by the promising results of the recent years with the improvement of Automatic Theorem Provers (ATP) by the integration of (deep) Machine Learning (ML) components, this project aims to bring the technology to a new level by proposing and implementing new theorem proving architectures directly designed to benefit the most from the marriage of the deductive and inductive technologies. The ultimate aim of the project is to improve the performance of a state-of-the-art prover in terms of general-purpose proving skills (as measured on problems from the representative TPTP library) by at least 15%. A corresponding improvement in application areas such as automation in interactive theorem proving or program verification is expected to follow.

The project is funded by the Czech Science Foundation, under the code GA24-12759S.

PhD Position Open

The MLTPA project is looking for a highly motivated PhD candidate with a Master's degree in Computer Science, mathematics, or a related field (background in logic and/or machine learning an advantage) to help us enhance the award winning automatic theorem prover Vampire with a new generation of neural guidance, combining elements of reinforcement learning and efficient vectorial representations of formulas and states, targeting the main applications in program verification and proof assistants.

The candidate is expected to contribute to international scientific research with excellent outcomes. This will require independent and innovative thinking and the ability to learn about new topics. The candidate is required to have excellent communication and writing skills in English and have substantial experience with code development.

We offer the opportunity to conduct scientifically challenging research on a fully funded position (1-year contract with the possibility of an extension of up to 4 years), including full social and health insurance. Work with an experienced international team within the CIIRC, CTU in Prague. Benefits include a competitive salary, 30 days paid leave, and a family-friendly environment (children’s corner, kindergarten, and elementary school operated by the Czech Technical University in Prague).

In case of interest or any questions, feel free to contact Martin Suda, the project's principal investigator.