Akce ČVUT

 Dnes
«  leden  2017  »
Po Út St Čt So Ne
            1
2 3 4 5 6 7 8
9 10 11 12 13 14 15
16 17 18 19 20 21 22
23 24 25 26 27 28 29
30 31          

Zpět na kalendář

25. přednáška PIS ? dr. Josef Urban: Umělá inteligence a dokazování matematických vět

26.01.2017   16:00

ANOTACE:

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 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 schází vždy 4. čtvrtek v měsíci v 16 hod. (s výjimkou letních měsíců a prosince), a to buď v budově FEL ČVUT na Karlově náměstí, nebo v budově MFF UK na Malostranském náměstí.
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ě.
Formát semináře připravil přípravný výbor ve složení Michal Chytil (ÚI AVČR), Pavel Kordík (FIT ČVUT), 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), 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.

Místo konání
MFF UK, Posluchárna S5, MFF UK, Malostranské nám. 25, Praha 1
Pořadatel
Přípravný výbor PIS
Kontaktní osoba
Veronika Šínová, info@praguecomputerscience.cz, 224 35 7667
Podrobnější informace
http://www.praguecomputerscience.cz/index.php?l=cz&p=25
Příloha
Stáhnout