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

Anotace Přednášející Poster

2024
2023
2022
2020
2019
2018
2017
2016
2015
2014

Přehrát záznam

26. ledna 2017

16:00

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

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.

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.

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.