Powering Automatic Theorem Provers by Machine Learning
Project goals
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.
Keywords
Public support
Provider
Czech Science Foundation
Programme
Junior Grants
Call for proposals
SGA0202000002
Main participants
České vysoké učení technické v Praze / Český institut informatiky, robotiky a kybernetiky
Contest type
VS - Public tender
Contract ID
20-06390Y
Alternative language
Project name in Czech
Zlepšování automatických dokazovačů vět pomocí strojového učení
Annotation in Czech
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.
Scientific branches
R&D category
ZV - Basic research
OECD FORD - main branch
10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)
OECD FORD - secondary branch
—
OECD FORD - another secondary branch
—
AF - Documentation, librarianship, work with information
BC - Theory and management systems
BD - Information theory
IN - Informatics
Solution timeline
Realization period - beginning
Jan 1, 2020
Realization period - end
Dec 31, 2022
Project status
—
Latest support payment
Apr 8, 2022
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
CEP23-GA0-GJ-R
Data delivery date
Jun 26, 2023
Finance
Total approved costs
6,467 thou. CZK
Public financial support
6,467 thou. CZK
Other public sources
0 thou. CZK
Non public and foreign sources
0 thou. CZK
Recognised costs
6 467 CZK thou.
Public support
6 467 CZK thou.
0%
Provider
Czech Science Foundation
OECD FORD
Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)
Solution period
01. 01. 2020 - 31. 12. 2022