Naším cílem je vyvinout systémy silné umělé inteligence a automatického uvažování (AR) schopné asistovat matematice, vědě a vývoji formálně ověřeného softwaru a návrhu systémů. Naše zaměření je na kombinaci AR se strojovým učením (ML) a vzájemným obohacováním induktivních a deduktivních metod AI, zejména za pomoci velkých korpusů pocházejících z formální matematiky a verifikace systémů.
Výzkumná témata:
- učením řízené automatické dokazování vět,
- řešení SAT, QBF a SMT, jejich kombinace s ML,
- metasystémy AI prokládající učení a uvažování,
- formalizace a interaktivní dokazování vět, jeho automatizace, asistence a autoformalizace
Projekty: AI4Reason, PowerATP, MLTPA
Více informací naleznete i na stránkách skupiny http://arg.ciirc.cvut.cz/