Matej Petković: Strojno učenje iz Agdinih grafov

Povzetek: Agda je programski jezik, ki se večinoma uporablja kot pomoč pri dokazovanju matematičnih trditev. V tipični Agdini knjižnici je formalno tako zapisan del matematičnega znanja. Na tokratnem srečanju bomo najprej osvežili spomin, kako Agdino knjižnico pretvorimo v graf, v katerem so vozlišča definicije iz knjižnice, usmerjene povezave pa sklici med njimi.

Nato si bomo ogledali, kako iz grafa s pomočjo strojnega učenja dobimo napovedni model, ki za dani par trditev $(t, u)$ pove, ali bi v dokazu trditve $t$ lahko uporabili trditev $u$. Pozornost bomo namenili samemu postopku ocenjevanja kvalitete algoritma, na koncu pa si bomo ogledali še rezultate za nekaj izbranih knjižnic.