Sylabus
- Přednáška uvede moderní metody a architektury, které kombinují strojové uvažování a učení. Stručně představíme dnešní hlavní systémy pro automatické a interaktivní dokazování vět, SMT solvery a velké formální knihovny. Dále probereme typické úlohy strojového učení, které odpovídají automatickému uvažování, od výběru znalostí z velkých znalostních bází, reprezentace znalostí a prohledávání, po detailní vedení dokazování. Podrobněji plánujeme pokrýt následující témata: -
1. Dokazování a učení v rozsáhlých znalostních bázích (výběr předpokladů, “hammer” systémy pro interaktivní dokazovače HOL, Mizar a Isabelle). -
2. Vedení saturačních a tableau dokazovačů (ENIGMA, metoda hintů, ProofWatch, MaLeCoP, Deep guidance). -
3. Vedení interaktivních dokazovačů (TacTicToe). -
4. Zpětné vazby mezi dokazováním a učením, reinforcement learning, pozitivní / negativní boosting (MaLARea, rlCoP, DeepMath, ATPBoost) -
5. Učení pro SAT, QBF, SMT a hledání modelů. -
6. Strojové učení a dokazování pro překlad a propojení mezi různými matematickými korpusy.
7. Reprezentace a tvorba domněnek - standardní symbolické reprezentace, neuronové a sémantické reprezentace, EnigmaWatch.
Anotace
Přednáška uvede moderní metody a architektury pro strojové uvažování a jeho kombinace s učením.