2014
2015
2016
2017
2018
2019
2020
2022
2023
2024

Dvacátépáté setkání Pražského informatického semináře

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ů.

26. ledna 2017

16:00

Posluchárna S5, MFF UK
Malostranské nám. 25, Praha 1
Zobrazit na mapě

Anotace přednášky

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.

Přednášející

Josef Urban

Josef Urban je vedoucím výzkumníkem v Českém institutu informatiky, robotiky a kybernetiky (CIIRC) při Českém vysokém učení technickém v Praze, kde vede projekt AI4REASON financovaný ERC. Jeho hlavním zájmem je vývoj inteligentních metod kombinujících indukci a dedukci nad velkými formálními (plně sémanticky popsanými) znalostními bázemi, jako jsou korpusy formálně zadaných matematických definic, vět a důkazů. Jeho systémy zvítězily v několika soutěžích na tomto poli. Magisterský a doktorský titul z informatiky získal na Karlově univerzitě v Praze, kde dále pracoval jako odborný asistent, a jako výzkumník pracoval na univerzitě v Miami a na Radboud University Nijmegen.

O PRAŽSKÉM INFORMATICKÉM SEMINÁŘI

Seminář se obvykle schází jednou za měsíc ve čtvrtek v 16:15 a to buď v budově FEL ČVUT nebo v budově MFF UK.

Jeho program je tvořen hodinovou přednáškou, po níž následuje časově neomezená diskuse. Základem přednášky je něco (v mezinárodním měřítku) mimořádného nebo aspoň pozoruhodného, na co přednášející přišel a co vysvětlí způsobem srozumitelným a zajímavým i pro širší informatickou obec. Přednášky jsou standardně v angličtině.

Seminář připravuje organizační výbor ve složení Roman Barták (MFF UK), Jaroslav Hlinka (ÚI AV ČR), Michal Chytil, Pavel Kordík (FIT ČVUT), Michal Koucký (MFF UK), Jan Kybic (FEL ČVUT), Michal Pěchouček (FEL ČVUT), Jiří Sgall (MFF UK), Vojtěch Svátek (FIS VŠE), Michal Šorel (ÚTIA AV ČR), Tomáš Werner (FEL ČVUT), Filip Železný (FEL ČVUT)

Idea Pražského informatického semináře vznikla z rozhovorů představitelů několika vědeckých institucí na téma, jak odstranit zbytečnou fragmentaci informatické komunity v ČR.

Podporovatelé

Kontakt

Pražský informatický seminář je z důvodů prevence šíření nákazy novým koronavirem do odvolání pozastaven.