Zlepšování automatických dokazovačů vět pomocí strojového učení

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

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.

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 <br>(dle <a href="http://www.vyzkum.cz/storage/att/E6EF7938F0E854BAE520AC119FB22E8D/Prevodnik_oboru_Frascati.pdf">převodníku</a>)

AF - Dokumentace, knihovnictví, práce s informacemi<br>BC - Teorie a systémy řízení<br>BD - Teorie informace<br>IN - Informatika

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

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

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č