Priporočilni sistem za pisanje programske kode

magistrsko delo

Nik Erzetič (Avtor), Ljupčo Todorovski (Mentor)

Povzetek

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.

Ključne besede

formalizacija matematike;dokazovalniki;Agda;strojno učenje;grafovske nevronske mreže;vložitve programske kode;napovedovanje povezav;

Podatki

Jezik:	Slovenski jezik
Leto izida:	2025
Tipologija:	2.09 - Magistrsko delo
Organizacija:	UL FMF - Fakulteta za matematiko in fiziko
Založnik:	[N. Erzetič]
UDK:	004.42
COBISS:	227592451
Št. ogledov:	39
Št. prenosov:	7
Ocena:	0 (0 glasov)
Metapodatki:

Ostali podatki

Sekundarni jezik:	Angleški jezik
Sekundarni naslov:	Recommender system for writing program code
Sekundarni povzetek:	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.
Sekundarne ključne besede:	formalization of mathematics;proof assistants;Agda;machine learning;graph neural networks;embedding program code;edge prediction;
Vrsta dela (COBISS):	Magistrsko delo/naloga
Študijski program:	0
Konec prepovedi (OpenAIRE):	1970-01-01
Komentar na gradivo:	Univ. v Ljubljani, Fak. za matematiko in fiziko, Oddelek za matematiko, Matematika - 2. stopnja
Strani:	VIII, 42 str.
ID:	25992503