20.500.12556/RUL-167588 Priporočilni sistem za pisanje programske kode Recommender system for writing program code V 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. In this work we develop a recommender system that supports formalisation of mathematics with the proof assistant Agda. We use machine learning to build the recommender system; we train the model on datasets mined from three Agda libraries for formalisation of mathematics. Each dataset consists of two parts: a set of abstract synatx trees for each library entry, and a graph of references between entries. The final recommender system combines a method for embedding abstract syntax trees of Agda entries into a real vector space, a graph neural network for vertex embeddings in the references graph, and an ansamble of decision trees for predicting references between entries. We compare our model to previous work and argue, that although it fails to surpass the best model so far it offers more practical use. formalizacija matematike dokazovalniki Agda strojno učenje grafovske nevronske mreže vložitve programske kode napovedovanje povezav formalization of mathematics proof assistants Agda machine lear- ning graph neural networks embedding program code edge prediction true false false Slovenski jezik Angleški jezik Magistrsko delo/naloga 2025-03-01 08:15:06 2025-03-01 08:15:13 2025-03-03 16:57:37 0000-00-00 00:00:00 2025 0 0 0000-00-00 NiDoloceno NiDoloceno NiDoloceno 0000-00-00 0000-00-00 0000-00-00 004.42 150028 227592451 16607.pdf 16607.pdf 1 59899E758AE5010AABCAB5625EC1A7D4 c1f1255ea205fc818de752c3002b5a9cf21473249049167d9e71ffac84683d54 002af3f9-f66c-11ef-b232-0050569b8976 https://repozitorij.uni-lj.si/Dokument.php?lang=slv&id=200247 Fakulteta za matematiko in fiziko 0 0 0