AR: Automatické uvažování

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/

Vedoucí skupiny

Jméno: Martin Suda
Email: martin.suda@cvut.cz

PI: Josef UrbanMartin Suda

Vědečtí pracovníci: Chad Brown, Jan Jakubův, Thibault Gauthier, Karel Chvalovský, Jan Hůla, Robert Veroff

Doktorandi: Filip Bártek, Lasse Blaauwbroek, Zarathustra Goertzel, Yutaka Nagashima, Jelle Piepenbrock, Bartosz Piotrowski