Our goal is to develop strong AI and automated reasoning (AR) systems capable of assisting mathematics, science, and the development of formally verified software and designs. Our focus is on combining AR with machine learning (ML) and cross-fertilization of inductive and deductive AI methods, in particular over large formal mathematical and verification corpora.
Research topics include:
- learning-guided automated theorem proving,
- SAT, QBF, and SMT solving, their combinations with ML,
- AI metasystems interleaving learning and reasoning,
- formalization and interactive theorem proving, its automation, assistance, and autoformalization
Projects: AI4Reason, PowerATP, MLTPA
Find more info on the web of our group http://arg.ciirc.cvut.cz/