Martin Suda improves automatic theorem provers by machine learning


Martin Suda received a junior grant from the Czech Science Foundation for improving automatic theorem provers (ATP) by methods of machine learning. ATPs are widely used in industry where formal proofs of safety of systems are critically needed, especially in automotive, aerospace or medicine.

Suda’s grant is for three years and it enables him to make and finance his micro team, who will take part in the research. What is interesting about the research is that it links two areas: that is, machine learning and automated verification. “To exaggerate a bit, in my research I will try to fulfil the dream of the famous philosopher Leibnitz, whose vision was that machines would be able to think about mathematics,” describes Suda his mission. “My goal is to achieve a great deal of versatility, that is, the language of the prover to be general enough to be used in a wide range of applications,” adds Suda.

The project will systematically investigate the topic of combining machine learning methods with state-of-the-art saturation-style Automated Theorem Provers. The ultimate objective is increasing the performance of the ATPs on a wide range of tasks, measured on standard automated reasoning benchmarks and in areas such as mathematics and software verification.

In the past Martin Suda worked on improvement of the prover called Vampire, which regularly ranks on top positions during the World Championship in Automated Reasoning.