Powering SMT Solvers by Machine Learning
The project POSTMAN aims at a breakthrough in the field of Satisfiability Modulo Theories (SMT) by developing Machine Learning (ML) methods targeted at critical parts of SMT procedures.
To solve real-world problems, many tools rely on SMT by translating the problems into a logic formulation and delegating their solution to a solver. SMT is thus at the heart of today's large verification toolchains, run continuously on thousands of CPUs by major software and hardware companies around the world.
The project will advance SMT solving by developing ML methods that prune the search space of the solvers. Unlike the current search methods, ML allows taking into account a large number of observations made during the search.
Guiding methods will be developed at various levels of abstraction, focusing on two critical problems in SMT: solving of quantified formulas and solving of sets of related formulas. The great challenges for ML are to learn and represent abstract objects under semantic constraints and to employ interpretable learning in combination with reasoning.
The expected outcome of the project is a range of new powerful methods combining ML techniques with current logic-based SMT approaches, providing a significant improvement over the state-of-the-art. The methods will be integrated in a number of systems and deployed in major SMT applications, benefiting large parts of today's formal methods.
The project is funded by ERC-CZ.
|