Priporočilni sistem za pisanje programske kodeErzetič, Nik (Avtor) Todorovski, Ljupčo (Mentor) formalizacija matematikedokazovalnikiAgdastrojno učenjegrafovske nevronske mreževložitve programske kodenapovedovanje povezavV delu smo razvili priporočilni sistem, ki podpira formalizacijo matematike s pomočjo dokazovalnika Agda. Priporočilni sistem smo zgradili z uporabo strojnega učenja na podatkovnih množicah, pripravljenih iz treh Agdinih knjižnic formalizirane matematike. Vsaka podatkovna množica je sestavljena iz dveh delov; prvi del je množica abstraktnih sintaktičnih dreves posameznih vnosov knjižnice, drugi pa je graf sklicev med vnosi. Priporočilni sistem združuje metodo za vložitev sintaktičnih dreves Agdinih vnosov v realni vektorski prostor, grafovsko nevronsko mrežo za vložitev vozlišč grafa sklicev in ansambel odločitvenih dreves za napovedovanje sklicev med vnosi. Svoj model smo primerjali z že obstoječimi in ugotovili smo, da za vodilnim le malo zaostaja in da je za uporabo priročnejši od njega.20252025-03-01 08:15:06Magistrsko delo/naloga167588sl