Speaker
Description
Predstavljamo MLFMF, zbirko podatkovnih množic za primerjalno analizo sistemov za priporočanje, ki se uporabljajo pri podpori formalizacije matematike s pomočniki za dokazovanje (angl. proof assistants). Ti sistemi pomagajo ljudem ugotoviti, kateri prejšnji vnosi (izreki, leme, aksiomi in podatkovni tipi) so uporabni pri dokazovanju novega izreka ali implementaciji novega vnosa.
Vsaka podatkovna množica v zbirki je zgrajena iz pripadajoče knjižnice formalizirane matematike, zapisane v pomočnikih za dokazovanje Agda ali Lean. Zbirka podatkovnih množic vključuje Mathlib (največjo knjižnico za Lean 4) in nekaj največjih Agdinih knjižnic: standardno knjižnico, knjižnico univalentne matematike Agda-unimath in knjižnico TypeTopology. Vsaka podatkovna množica predstavlja ustrezno knjižnico na dva načina: kot heterogeno omrežje in kot seznam s-izrazov, ki predstavljajo sintaksna drevesa posameznih vnosov v knjižnici. Omrežje vsebuje (modularno) strukturo knjižnice in reference med vnosi, medtem ko s-izrazi dajejo popolne in računalniku dostopne informacije o vsakem vnosu.
Poročamo o osnovnih rezultatih z uporabo standardnih vpetij grafov in besed, drevesnih ansamblov in algoritmov strojnega učenja, ki temeljijo na najbližjih sosedih. Podatkovne množice MLFMF zagotavljajo dobro podlago za nadaljnje raziskovanje in primerjalno analizo poljubnih pristopov strojnega učenja k formalizirani matematiki. Metodologija, uporabljena za pretvorbo knjižnic v omrežja in s-izraze, se zlahka uporablja tudi za druge knjižnice in druge pomočnike za dokazovanje. S skupno več kot $250\,000$ vnosi je to trenutno največja zbirka formaliziranega matematičnega znanja v obliki, primerni za uporabo algoritmov strojnega učenja.
