Obohacování SMT řešičů pomocí strojového učení
Cíle projektu
"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í."
Klíčová slova
Artificial intelligenceAutomated reasoningMachine LearningSMTSoftware verification
Veřejná podpora
Poskytovatel
Ministerstvo školství, mládeže a tělovýchovy
Program
ERC CZ
Veřejná soutěž
SMSM2019LL001
Hlavní účastníci
České vysoké učení technické v Praze / Český institut informatiky, robotiky a kybernetiky
Druh soutěže
VS - Veřejná soutěž
Číslo smlouvy
MSMT-35696/2019-1
Alternativní jazyk
Název projektu anglicky
Powering SMT Solvers by Machine Learning
Anotace anglicky
"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."
Vědní obory
Kategorie VaV
ZV - Základní výzkum
OECD FORD - hlavní obor
20202 - Communication engineering and systems
OECD FORD - vedlejší obor
—
OECD FORD - další vedlejší obor
—
CEP - odpovídající obory
(dle převodníku)JW - Navigace, spojení, detekce a protiopatření
Termíny řešení
Zahájení řešení
1. 1. 2020
Ukončení řešení
31. 12. 2025
Poslední stav řešení
K - Končící víceletý projekt
Poslední uvolnění podpory
11. 1. 2024
Dodání dat do CEP
Důvěrnost údajů
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů
Systémové označení dodávky dat
CEP25-MSM-LL-R
Datum dodání záznamu
20. 2. 2025
Finance
Celkové uznané náklady
38 916 tis. Kč
Výše podpory ze státního rozpočtu
38 916 tis. Kč
Ostatní veřejné zdroje financování
0 tis. Kč
Neveřejné tuz. a zahr. zdroje finan.
0 tis. Kč
Základní informace
Uznané náklady
38 916 tis. Kč
Statní podpora
38 916 tis. Kč
100%
Poskytovatel
Ministerstvo školství, mládeže a tělovýchovy
OECD FORD
Communication engineering and systems
Doba řešení
01. 01. 2020 - 31. 12. 2025