🤖 machine learning

Nazrin: An Atomic Neural Proof Automation Tactic in Lean 4

Dit artikel introduceert Nazrin, een op graph neural networks gebaseerde stellingbewijzersagent voor Lean 4 die gebruikmaakt van een nieuwe set atomaire tactieken, een transponerend atomiseringsalgoritme en de ExprGraph-datastructuur om robuuste, voor consumentenhardware compatibele bewijsautomatisering mogelijk te maken.

Oorspronkelijke auteurs: Leni Aniva, Iori Oikawa, David Dill, Clark Barrett

Gepubliceerd 2026-07-01

📖 5 min leestijd🧠 Diepgaand

CC BY 4.0

Oorspronkelijke auteurs: Leni Aniva, Iori Oikawa, David Dill, Clark Barrett

Oorspronkelijk artikel gelicentieerd onder CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Dit is een AI-gegenereerde uitleg van het onderstaande artikel. Het is niet geschreven of goedgekeurd door de auteurs. Raadpleeg het oorspronkelijke artikel voor technische nauwkeurigheid. Lees de volledige disclaimer

Stel je voor dat je een robot probeert te leren complexe wiskundige puzzels op te lossen. Het doel van de robot is om te bewijzen dat een wiskundige bewering waar is. In de wereld van de informatica wordt dit "Machine-Assisted Theorem Proving" genoemd.

De paper introduceert een nieuwe robot genaamd Nazrin (wat staat voor Neural Atomizer for Inhabitation Problems). Nazrin is ontworpen om slimmer, sneller en efficiënter te zijn dan eerdere robots bij het oplossen van deze puzzels. Hier is hoe het werkt, onderverdeeld in eenvoudige concepten en analogieën.

1. Het Probleem: Te Veel Keuzes

Stel je voor dat je een videogame speelt waarin je een schat moet bereiken. In de oude manier van robots trainen, kreeg de robot een enorme, oneindige menukaart met zetten. De robot kon zeggen: "Spring," "Ren," "Vlieg," "Gebruik een magische spreuk," of "Combineer 50 verschillende spreuken in een specifieke volgorde."

Omdat de menukaart zo groot en rommelig was, raakte de robot in de war. De robot wist niet of de menselijke speler een zet koos omdat het de beste zet was, of gewoon omdat de speler daar zin in had. Ook slaan door mensen geschreven bewijzen vaak stappen over of gebruiken ze slimme afkortingen die er op papier goed uitzien, maar die voor een robot moeilijk zijn om vanaf nul op te bouwen.

2. De Oplossing: Atomische Tactieken (De Lego-stenen)

Nazrin lost dit op door de robot een kleine, eindige doos met Atomische Tactieken te geven. Denk aan deze als standaard Lego-stenen.

In plaats van "Bouw een kasteel," heeft de robot alleen instructies zoals "Plaats een rode steen," "Plaats een blauwe steen," of "Verbind twee stenen."
Deze "stenen" zijn simpel, eindig en strikt gedefinieerd.
De paper beweert dat als je de juiste set van deze eenvoudige stenen hebt, je elk geldig wiskundig bewijs kunt bouwen.

Dit maakt de taak van de robot veel gemakkelijker. In plaats van te kiezen uit een oneindige menukaart, hoeft hij alleen maar te kiezen uit een kleine, beheersbare lijst met opties bij elke stap.

3. De Vertaler: Transposing Atomization

Je zou kunnen vragen: "Maar hoe leren we de robot als alle bestaande wiskundige bewijzen geschreven zijn in 'geavanceerde menselijke taal' met enorme afkortingen?"

De auteurs creëerden een speciale vertaler genaamd Transposing Atomization.

De Analogie: Stel je een menselijke chef voor die een recept schrijft met de tekst: "Maak een perfecte soufflé." Dit is de "Presentation View"—het ziet er geweldig uit, maar het slaat de details over.
De vertaler neemt dat recept en breekt het af in een stapsgewijze lijst van atomische acties: "Klop 3 eieren," "Klutsen gedurende 2 minuten," "Voeg suiker toe," "Bak op 350 graden."
Dit proces zet de "geavanceerde" menselijke bewijzen om in een lange, gedetailleerde sequentie van eenvoudige "atomische" stappen. Dit geeft de robot een enorme bibliotheek aan trainingsgegevens om van te leren.

4. De Kaart: ExprGraph

Wiskundige expressies kunnen rommelig zijn. Ze bevatten vaak dezelfde getallen of variabelen die vele malen worden herhaald, of ze gebruiken verschillende namen voor hetzelfde ding.

De Analogie: Stel je een kaart van een stad voor. Op een normale kaart wordt elke straat apart getekend. Maar in de kaart van Nazrin (genaamd ExprGraph), als twee straten eigenlijk dezelfde weg zijn, worden ze als één enkele lijn getekend. Als twee gebouwen hetzelfde type zijn, delen ze één enkel icoon.
Deze "Essentialization" stript de verwarrende details weg en focust alleen op de structuur van de wiskunde. Het helpt de robot om de "vorm" van het probleem te zien zonder afgeleid te worden door irrelevante informatie.

5. Het Brein: Nazrin Prover

Nazrin is het brein van de robot. Het is een type kunstmatige intelligentie genaamd een Graph Neural Network (GNN).

Omdat de wiskundige problemen zijn omgezet in deze schone "kaarten" (ExprGraphs), kan Nazrin naar de kaart kijken en de volgende beste "Lego-steen" (atomische tactiek) voorspellen om te plaatsen.
De Superkracht: Nazrin is ongelooflijk snel. Terwijl andere robots (zoals die met grote taalmodellen) misschien seconden nodig hebben om één zet te bedenken, kan Nazrin duizenden zetten per minuut genereren.
Hardware: Het is zo efficiënt dat het kan draaien op een standaard thuiscomputer ("consumer-grade" machine), en niet alleen op een enorme supercomputer.

6. De Resultaten: Hoe goed werkt het?

De auteurs testten Nazrin op twee grote bibliotheken met wiskundige problemen (de "Standard Library" en "Mathlib").

Ze trainden Nazrin op één set problemen en vroegen hem vervolgens om nieuwe, ongeziene problemen uit een vergelijkbare set op te lossen.
De Uitkomst: Nazrin slaagde erin om ongeveer 57% van de problemen in de standaardbibliotheek te bewijzen en 34% in de grotere Mathlib-bibliotheek.
Cruciaal is dat Nazrin in staat was om sommige problemen op te lossen die andere beroemde geautomatiseerde tools (zoals Aesop en Grind) niet konden oplossen. Het fungeert als een ander soort hulpmiddel dat de bestaande tools aanvult.

Samenvatting

Kortom, de paper introduceert Nazrin, een theorem-proving robot die:

Complexe wiskunde afbreekt in eenvoudige, atomische stappen (zoals Lego-stenen).
Menselijke bewijzen vertaalt naar deze eenvoudige stappen om van te leren.
Een speciale "kaart" gebruikt om de structuur van de wiskunde te begrijpen zonder in de war te raken door details.
Snel draait op gewone computers en wiskundige problemen kan oplossen die andere tools missen.

De auteurs benadrukken dat dit een nieuwe manier is om wiskundige bewijzen aan te pakken, waarbij de focus ligt op het proces van het vinden van de oplossing (de zoektocht) in plaats van alleen op het uiteindelijke geschreven resultaat.

Technische Samenvatting: Nazrin: Een Atomaire Neurale Bewijsautomatiseringstactiek in Lean 4

Probleemstelling

Machine-ondersteunde stellingbewijsvorming in systemen zoals Lean 4 staat voor aanzienlijke uitdagingen bij het trainen van geautomatiseerde agenten op door mensen geschreven bewijzen. De primaire obstakels zijn:

Onbegrensde Actieruimtes: Menselijke bewijzen maken gebruik van een oneindige variëteit aan tactieken met willekeurige parameters (bijv. simp met lange argumentenlijsten, use met willekeurige getuigen), wat een ruisende en moeilijk te leren zoekruimte creëert.
Presentatie versus Zoekweergave: Door mensen geschreven bewijzen geven vaak de voorkeur aan beknoptheid en leesbaarheid (Presentatieweergave), wat de incrementele, achterwaartse redeneerstappen (Zoekweergave) die feitelijk vereist zijn voor het ontdekken van het bewijs, maskeert. Dit omvat "mysterieuze sprongen" en het weglaten van tussenliggende stappen.
Metavariabele Koppeling: In Lean zijn doelen (goals) vaak aan elkaar gekoppeld via metavariabelen. Een naïeve boomzoektocht houdt geen rekening met het feit dat het oplossen van één doel onmiddellijk een ander doel kan oplossen of een pad onmogelijk kan maken, wat de zoektocht bemoeilijkt op een Directed Acyclic Graph (DAG) in plaats van een eenvoudige boom.
Hardwarebeperkingen: Bestaande neurale stellingbewijzers vereisen vaak aanzienlijke computationele middelen, wat hun toegankelijkheid en de schaal van de te verwerken trainingsdata beperkt.

Methodologie

Het artikel introduceert Nazrin (Neural Atomizer for Inhabitation Problems), een op een Graph Neural Network (GNN) gebaseerde stellingbewijzende agent. De methodologie rust op drie kernzuilen:

1. Atomaire Tactieken

De auteurs definiëren een kleine, eindige verzameling "atomaire tactieken" die in staat zijn om elke bewijsbare stelling in Lean te bewijzen. Deze tactieken zijn ontworpen om een begrensde parameterruimte te hebben, zodat de actieruimte voor de agent eindig is.

Volledigheid: De verzameling dekt alle top-level expressieconstructoren in Lean (bijv. intro voor lambda-abstractie, exact/apply voor constanten, cases voor inductieve typen).
Eigenschappen: De tactieken zijn invariant (veranderen de toegewezen metavariabelen niet zonder terug te draaien), volledig, progressief (maken altijd progressie) en deterministisch.
Minimalisatie van de Doorsnede: De verzameling is gekozen om "doorsneden" (het aantal gekoppelde doelen) te minimaliseren, wat de moeilijkheid van het genereren van begeleiding vermindert.

2. Transponering van Atomisering

Om de agent te trainen, hebben de auteurs een nieuw algoritme ontwikkeld om bestaande door mensen geschreven bewijzen (Presentatieweergave) om te zetten in sequenties van atomaire tactieken (Zoekweergave).

Atomisering: Het algoritme vertaalt willekeurige bewijstermen naar een reeks atomaire stappen. Het gebruikt de grondwaarheid van de bewijsterm om de constructie van een nieuw bewijs te leiden met behulp van enkel atomaire tactieken.
Transponering: Het algoritme herordent de uitvoering van tactieken om overeen te komen met de "Zoekweergave". Het geeft prioriteit aan "opvolger"-doelen (doelen waarvan de oplossingen voorgangers informeren) boven "voorganger"-doelen. Dit bootst de achterwaartse redenering na die wordt gebruikt bij ontdekking (bijv. $\epsilon$ - $\delta$ bewijzen) in plaats van de voorwaartse presentatie.
State-Level en Goal-Level Transponering: Het systeem herordent de tactische dispatch om doodlopende paden te vermijden. Het staat bijvoorbeeld toe dat niet-conflicterende "semigraad"-tactieken (die werken op delen van een doel of vrije variabele) in een willekeurige volgorde worden uitgevoerd, zelfs als de gekoppelde doelen nog niet zijn geïnstantieerd.

3. ExprGraph en Neurale Architectuur

De agent gebruikt een Graph Neural Network (GNN) om Lean-expressies te verwerken, gerepresenteerd als ExprGraphs.

Essentialisering: Expressies worden omgezet in grafen waarbij irrelevante technische verschillen (bijv. specifieke variabelenamen, metadata) worden verwijderd. De graaf behoudt fundamentele symmetrieën (bijv. $\alpha$ -equivalentie) en zorgt ervoor dat subexpressies overeenkomen met subgrafen.
Neural Probabilistic Automaton (NPA): In plaats van een standaard generatief model gebruikt Nazrin een NPA. De GNN moduleert de overgangskansen van een eindige automaat.
- Kind State: Selecteert het type tactiek (bijv. intro, apply).
- Descendant States: Gespecialiseerde GNN-koppen genereren argumenten (bijv. het selecteren van een constante voor apply of een vrije variabele).
Efficiëntie: Het model is klein (1,5M parameters voor de standaardbibliotheek, 11M voor Mathlib) en draait op consumentenhardware van een CPU, waarbij duizenden tactieken per minuut worden gegenereerd.

Belangrijkste Bijdragen

Atomaire Tactieken: Een eindige, volledige verzameling tactieken die de actieruimte van het stellingbewijzen reduceert tot een beheersbare grootte, wat efficiënte reinforcement learning en supervised training mogelijk maakt.
Transponering van Atomisering Algoritme: Een methode om grootschalige trainingsdata te genereren door bestaande geformaliseerde wiskunde om te zetten in atomaire, zoekweergave-bewijzen, waardoor de agent effectief leert hoe men bewijzen vindt in plaats van hoe men ze presenteert.
ExprGraph: Een gereduceerde graafgebaseerde representatie van Lean-expressies die de structurele symmetrieën en variabele-referenties benut, en expliciet de aandachtmechanismen (attention mechanisms) nabootst die in taalmodellen worden gevonden.
Nazrin Prover: Een efficiënte, op GNN gebaseerde agent die succesvol traint op atomiseerde data en generaliseert naar nieuwe stellingen.
Evaluatiekader: Een rigoureuze evaluatie die de ontwikkeling van nieuwe theorieën nabootst, waarbij de agent wordt getraind op één deel van de bibliotheek en wordt getest op het volgende deel om informatielekkage te voorkomen.

Resultaten

De auteurs hebben Nazrin geëvalueerd op de standaardbibliotheek van Lean en Mathlib:

Atomiseringssucces: Ongeveer 58% van de 170.180 stellingen werd succesvol geatomiseerd.
Generalisatie:
- Getraind op Standard Library Slice 1, bereikte Nazrin 57% nauwkeurigheid op Slice 2.
- Getraind op Mathlib Slice 3, bereikte Nazrin 34% voltooiing op Slice 4.
Vergelijking: Nazrin demonstreerde het vermogen om stellingen te bewijzen die bestaande automatiserings-tactieken (Aesop en Grind) niet konden oplossen binnen een tijdlimiet van 15 seconden.
Prestaties: Het systeem werkt efficiënt op consumentenhardware, wat contrasteert met de zware middelen die nodig zijn voor veel LLM-gebaseerde bewijzers.

Betekenis en Claims

Het artikel beweert dat Nazrin de fundamentele mismatch aanpakt tussen de structuur van door mensen geschreven bewijzen en de vereisten van geautomatiseerde zoektochten. Door een eindige actieruimte af te dwingen via atomaire tactieken en trainingsdata te genereren via transponering van atomisering, laten de auteurs zien dat:

Machine learning-agenten getraind kunnen worden om bewijzen incrementeel te ontdekken zonder dat zij complexe, willekeurige parameters vanuit het niets hoeven te genereren.
Graafgebaseerde representaties effectief zijn voor het vastleggen van de structurele symmetrieën van wiskundige bewijzen.
Hoge-prestatie stellingbewijzing haalbaar is op bescheiden hardware, wat de technologie toegankelijker maakt.

De auteurs merken op dat hoewel het systeem veelbelovend is, het momenteel niet alle stellingen dekt (atomisering faalt voor sommige bewijzen met een hoge doorsnede) en de architectuur nog niet volledig is afgesteld. Ze suggereren dat toekomstig werk zich kan richten op het verbeteren van de dekking van de atomisering, het verminderen van de doorsneden en het verfijnen van de neurale architectuur om robuuster om te gaan met multi-parameter conditionering en niet-symbolische data (getallen/strings).