proběhne 26. ledna 2017
v posluchárně S5, MFF UK
Malostranské nám. 25, Praha 1
Na programu je Josef Urban: Umělá inteligence a dokazování matematických vět
Probereme některé metody umělé inteligence, jimiž se lze učit dokazovat hypotézy nad velkými formálními matematickými korpusy. Tyto metody zahrnují (i) techniky strojového učení, jež se z předchozích důkazů učí navrhovat lemmata co nejrelevantnější pro dokazování dalších hypotéz, (ii) metody, které na základě popisů dřívějších důkazů řídí nízkoúrovňové algoritmy vyhledávání důkazů, a (iii) metody, jež samostatně vymýšlejí vhodné dokazovací strategie pro dané třídy problémů.
Ukážu příklady systémů umělé inteligence zahrnujících kladnou zpětnou vazbu mezi indukcí a dedukcí, a předvedu výkonnost současných metod nad velkými knihovnami existujících dokazovacích asistentů, jako jsou Isabelle, Mizar a HOL. Nakonec se zmíním o nově vznikajících systémech umělé inteligence kombinujících techniky statistického větného rozboru neformálních matematických vět se silnými metodami dokazování vět.
Bližší informace najdete na webové stránce PIS.
Žádné komentáře:
Okomentovat