Machine learning for theorem proving in Lean : master's thesis

Petrovčič, Job (avtor), Todorovski, Ljupčo (mentor), Narvaez Denis, David Eliecer (komentor)

This thesis develops machine learning methods to address bottlenecks in automated theorem proving within the Lean 4 proof assistant, investigating two levels of abstraction: foundational kernel expressions and high-level proof states and tactics. These approaches are first contextualized by an exposition of the proof assistant's internal architecture. Then, at the kernel level, we introduce a curiosity-driven reinforcement learning agent that generates well-typed expressions without training data consisting of well-typed expressions. By using a reward surprisal mechanism to overcome the limitations of premature exploitation, the agent explores the constrained state space of well-typed expressions, discovering a more diverse set of valid mathematical constructs than the baselines. For the high-level task of premise selection, we propose a novel GNN-augmented retriever that exploits the structural dependency graph of mathematical libraries. Our results demonstrate that the purely structural model achieves premise-retrieval metrics comparable to those of the language-model-based retriever, and that combining the two can improve retrieval. This work establishes that curiosity-driven exploration and structural learning are promising directions for overcoming data scarcity and advancing automated mathematical reasoning.

• Jezik: Angleški jezik
• Ključne besede: formal theorem proving, Lean 4, reinforcement learning, graph neural networks, premise selection, formal mathematical libraries
• Vrsta gradiva: Magistrsko delo/naloga
• Tipologija: 2.09 - Magistrsko delo
• Organizacija: FMF - Fakulteta za matematiko in fiziko
• Leto izida: 2026
• PID: 20.500.12556/RUL-190593
• UDK: 004.8
• COBISS.SI-ID: 302863107
• Datum objave v RUL: 30.10.2026

Sekundarni jezik

• Jezik: Slovenski jezik
• Naslov: Strojno učenje za dokazovanje izrekov v Leanu

Izvleček

Magistrsko delo razvije metodi strojnega učenja za odpravljanje pomanjkljivosti avtomatskega dokazovanja izrekov v dokazovalniku Lean 4, pri čemer obravnava dva nivoja abstrakcije: temeljne jedrne izraze ter višjenivojska dokazna stanja in taktike. Najprej je predstavljena notranja arhitektura dokazovalnika, ki je ozadje obeh pristopov. Nato na nivoju jedra predstavimo agenta spodbujevalnega učenja, ki ga vodi radovednost in ki generira izraze s tipom brez učnih podatkov, sestavljenih iz izrazov, za katere že vemo, da imajo tip. Z uporabo mehanizma presenečenja pri nagrajevanju za premagovanje problema prezgodnjega izkoriščanja agent raziskuje omejen prostor stanj izrazov s tipom in odkriva bolj raznolik nabor veljavnih matematičnih konstruktov kot naivni pristopi. Pri višjenivojski nalogi izbire premis predlagamo nov iskalnik, razširjen z grafovskimi nevronskimi mrežami, ki izkorišča grafovsko strukturo odvisnosti matematičnih knjižnic. Rezultati kažejo, da povsem strukturni model dosega metrike iskanja premis, primerljive z metrikami iskalnika na osnovi jezikovnega modela, in da lahko kombinacija obeh izboljša iskanje. Zaključek dela je, da sta raziskovanje, vodeno z radovednostjo, in strukturno učenje obetavni smeri za premagovanje problema pomanjkanja podatkov in za napredek pri avtomatskem matematičnem sklepanju.

• Ključne besede: formalno dokazovanje izrekov, Lean 4, spodbujevalno učenje, grafovske nevronske mreže, izbira premis, formalne matematične knjižnice