Powering SMT Solvers by Machine Learning
Project goals
"The POSTMAN project aims at a breakthrough in the field of Satisfiability Modulo Theories (SMT) by developing Machine Learning methods targeted at the critical parts of today's SMT procedures. SMT solvers are efficient tools that reason about fragments of first order logic with focus on practical applications. These tools play a crucial role in verification and testing of software, hardware and related areas. To solve real-world problems, many tools rely on SMT by translating the problems into a logic formulation and delegating their solution to the SMT solvers. 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. SMT systems strive to provide push-button technology, however, they need to handle inherently hard problems. Failing to solve a problem in reasonable time means that the users are forced to reformulate the problem or to provide the solver with hints. Both scenarios are undesirable, requiring extra effort and considerable SMT expertise. POSTMAN will very significantly advance SMT solving by developing Machine Learning methods that prune the search space of the solvers. Unlike the current search methods, Machine Learning allows to take into account a large number of observations made during the proof searches, and recommend the most relevant course of action. The project will develop learning-based guiding methods at various levels of abstraction, focusing on two critical problems in SMT and its applications: solving of quantified formulas and solving of classes of formulas. The expected outcome of the project is a range of new powerful methods combining Machine Learning techniques with current logic-based SMT approaches, providing significant improvement over current 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 verification."
Keywords
Artificial intelligenceAutomated reasoningMachine LearningSMTSoftware verification
Public support
Provider
Ministry of Education, Youth and Sports
Programme
ERC CZ
Call for proposals
SMSM2019LL001
Main participants
České vysoké učení technické v Praze / Český institut informatiky, robotiky a kybernetiky
Contest type
VS - Public tender
Contract ID
MSMT-35696/2019-1
Alternative language
Project name in Czech
Obohacování SMT řešičů pomocí strojového učení
Annotation in Czech
"Cílem projektu POSTMAN je dosáhnout průlomu v oblasti Splnitelnost Modulo Teorie (SMT) pomocí vývoje metod strojového učení cílených na kritické části dnešních procedur pro řešení SMT. Řešiče SMT jsou účinné nástroje, které uvažují nad fragmenty logiky prvního řádu se zaměřením na praktické aplikace. Tyto nástroje hrají stěžejní roli v ověřování a testování softwaru, hardwaru a příbuzných oblastech. K řešení problémů z reálného světa, mnoho nástrojů závisí na SMT tím, že překládají daný problém do formulace matematické logiky a delegují jeho řešení SMT řešiči. SMT se tímto ocitá v jádru dnešních verifikačních nástrojů, které se systematicky spouští na tisících procesorech ve velkých softwarových a hardwarových firmách. SMT systémy usilují o poskytnutí plné automatizace, ale oproti tomu musí řešit ze své podstaty těžké problémy. Pokud nástroj nevyřeší daný problém v požadovaném čase, uživatelé jsou nuceni reformulovat tento problém nebo poskytnout řešiči nápovědu. Oba scénáře jsou nežádoucí tím že vyžadují další úsilí a značnou znalost používaného nástroje. POSTMAN velmi výrazně pokročí v řešení SMT rozvíjením metod strojového učení, které prořezávají prohledávací prostor problému. Na rozdíl od současných metod prohledávání, strojové učení umožňuje brát v úvahu velký počet pozorování provedených během hledání důkazů a doporučit nejrelevantnější postup. Projekt bude rozvíjet učící metody na různých úrovních abstrakce se zaměřením na dva kritické problémy v SMT a jeho aplikacích: řešení kvantifikovaných formulí a řešení tříd formulí. Očekávaným výstupem projektu je řada nových výkonných metod kombinujících techniky strojového učení se současnými přístupy SMT založenými na logice, které poskytnou výrazné zlepšení oproti současnému stavu. Tyto metody budou integrovány do řady systémů a nasazeny ve významných SMT aplikacích, používaných ve velké části moderního formálního ověřování."
Scientific branches
Solution timeline
Realization period - beginning
Jan 1, 2020
Realization period - end
Dec 31, 2025
Project status
K - Ending multi-year project
Latest support payment
Jan 11, 2024
Data delivery to CEP
Confidentiality
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů
Data delivery code
CEP25-MSM-LL-R
Data delivery date
Feb 20, 2025
Finance
Total approved costs
38,916 thou. CZK
Public financial support
38,916 thou. CZK
Other public sources
0 thou. CZK
Non public and foreign sources
0 thou. CZK
Basic information
Recognised costs
38 916 CZK thou.
Public support
38 916 CZK thou.
100%
Provider
Ministry of Education, Youth and Sports
OECD FORD
Communication engineering and systems
Solution period
01. 01. 2020 - 31. 12. 2025