Zlepšování automatických dokazovačů vět pomocí strojového učení
Cíle projektu
Tento projekt bude systematicky studovat téma kombinování metod strojového učení se “state-of-the-art” automatickými dokazovači vět zaločnými na saturaci. Naším konečným cílem je zvýšit výkon těchto dokazovačů na široké škále úloh, měřených na standardních benchmarcích z oblasti automatického uvažování a v oblastech jako matematika a verifikace software. Ze zvýšení výkonu dokazovačů budou okamžitě benefitovat odborníci v oblasti formálního uvažování s řadou aplikací. Navrhované téma je taktéž velmi zajímavé jako otázka výzkumu obecné umělé inteligence. Úspěšné kombinace statistických metod a symbolické umělé inteligence jsou stále poměrně vzácné a je dobře známo, že dokazování vět v logice prvního řádu je nerozhodnutelné. To vyvolává řadu otázek jak o praktických tak teoretických limitech existujících učících metod pro úlohy spojené s uvažováním.
Klíčová slova
Veřejná podpora
Poskytovatel
Grantová agentura České republiky
Program
Juniorské granty
Veřejná soutěž
SGA0202000002
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
20-06390Y
Alternativní jazyk
Název projektu anglicky
Powering Automatic Theorem Provers by Machine Learning
Anotace anglicky
In this project, we will systematically investigate the topic of combining machine learning methods with state-of-the-art saturation-style Automated Theorem Provers (ATPs). Our ultimate objective is increasing the performance of these ATPs on a wide range of tasks, measured on standard automated reasoning benchmarks and in areas such as mathematics and software verification. Increased performance of the ATP systems will in turn immediately benefit practitioners of formal reasoning in a number of applications. The proposed topic is very interesting also from the perspective of general AI research. Successful combinations of statistical and symbolic AI are still relatively rare, and it is well known that first-order theorem proving is undecidable. This leads to a number of questions about both the theoretical and practical power of existing learning approaches in reasoning tasks.
Vědní obory
Kategorie VaV
ZV - Základní výzkum
OECD FORD - hlavní obor
10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)
OECD FORD - vedlejší obor
—
OECD FORD - další vedlejší obor
—
CEP - odpovídající obory
(dle převodníku)AF - Dokumentace, knihovnictví, práce s informacemi
BC - Teorie a systémy řízení
BD - Teorie informace
IN - Informatika
Termíny řešení
Zahájení řešení
1. 1. 2020
Ukončení řešení
31. 12. 2022
Poslední stav řešení
—
Poslední uvolnění podpory
8. 4. 2022
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
CEP23-GA0-GJ-R
Datum dodání záznamu
26. 6. 2023
Finance
Celkové uznané náklady
6 467 tis. Kč
Výše podpory ze státního rozpočtu
6 467 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
6 467 tis. Kč
Statní podpora
6 467 tis. Kč
100%
Poskytovatel
Grantová agentura České republiky
OECD FORD
Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)
Doba řešení
01. 01. 2020 - 31. 12. 2022