Technische Samenvatting: Beyond the Library: An Agentic Framework for Autoformalizing Research Mathematics

Probleemstelling

Hoewel Large Language Models (LLM's) aanzienlijke capaciteiten hebben getoond in wiskundige redeneringen, produceren ze regelmatig subtiele logische fouten die moeilijk door mensen te detecteren zijn. Dit maakt automatische verificatie noodzakelijk. Formele talen zoals Lean 4 bieden mechanische bewijscontrole, maar de vertaling van informele natuurlijke taal wiskunde naar verifieerbare code (autoformalizatie) blijft een knelpunt.

Twee primaire uitdagingen belemmeren de huidige autoformalisatie-inspanningen:

1. Formalisering van Stellingen: In tegenstelling tot bewijsformalisering, die profiteert van compiler-feedback, mist de vertaling van een stelling zonder "mechanische grondwaarheid". Het is onmogelijk om automatisch te verifiëren dat een vertaalde stelling perfect overeenkomt met de natuurlijke taalbron zonder menselijke tussenkomst.
2. Beperkingen van Bibliotheken: Onderzoekswiskunde leunt vaak op concepten die buiten de reikwijdte van bestaande formele bibliotheken zoals Mathlib vallen. Directe vertaling van complexe stellingen in niet-ondersteunde domeinen faalt routinematig omdat de benodigde type-definities niet bestaan.
3. Rigiditeit van de Pipeline: Bestaande benaderingen vertrouwen vaak op enkelvoudige agenten of vaste, lineaire pipelines. Deze worstelen met langetermijnredeneringen (verzadiging van het contextvenster) en kunnen niet terugkeren naar eerdere stappen wanneer vroege stappen falen, wat leidt tot harde fouten in complexe onderzoeksscenario's.

Methodologie

De auteurs stellen een multi-agent agentic framework voor, aangedreven door algemene programmeer-LLM's (specifiek Claude Opus). Het systeem wordt beheerd door een centrale Orchestrator die twee onderscheidende, niet-lineaire pipelines aanstuurt: Statement Formalization (Stellingformalisering) en Proof Formalization (Bewijsformalisering).

1. Orchestrator en Agentic Design

De Orchestrator beheert een dynamische pipeline waarbij sub-agenten specifieke taken afhandelen. In tegenstelling tot vaste pipelines kan de Orchestrator fasen herordenen, terugkeren naar vorige staten en feedbackloops openen. Dit ontwerp voorkomt contextverzadiging door sub-taken te delegeren en maakt dynamisch herstel van fouten mogelijk.

2. Statement Formalization Pipeline

Deze pipeline volgt een "type-first" paradigma om bibliotheekbeperkingen aan te pakken:

• Type Planning: Voordat de hoofdstelling wordt geformaliseerd, identificeert een Type Planner ontbrekende domeinspecifieke concepten die vereist zijn vanuit Mathlib.
• Auxiliary Lemma Verification (Unit Testing): Voor elk ontbrekend type genereert het systeem "auxiliary lemmas" (algemene eigenschappen van het type). Vervolgens probeert het deze lemmas te bewijzen. Als de bewijzer faalt, geeft dit aan dat de type-definitie incorrect of slecht gevormd is. Dit functioneert als een unit test voor wiskundige definities.
• Iteratieve Verfijning: Meerdere Type Formalizer agents genereren kandidaten. Een Auctioneer selecteert de beste kandidaat op basis van succespercentages van bewijzen, semantische alignment (geverifieerd door een Faithfulness Judge) en codelengte.
• Faithfulness Checking: Een Faithfulness Judge verifieert dat de Lean-code overeenkomt met de bron in natuurlijke taal. Hiervoor wordt een "blind" back-translation methode gebruikt (het vertalen van Lean terug naar natuurlijke taal) en een directe vergelijking, beoordeeld door een apart model om bias te verminderen.
• Theorem Formalization: Zodra de noodzakelijke vocabulaire is vastgesteld, vertaalt een Theorem Formalizer de hoofdstelling, onderworpen aan dezelfde faithfulness checks.

3. Proof Formalization Pipeline

Deze pipeline deelt bewijzen recursief op in een boom van knooppunten:

• Natural Language Prover: Stelt een informeel bewijs op, dat iteratief wordt verfijnd door een Proof Critic (die controleert op logische hiaten, ongedefinieerde termen en niet-gestelde hypothesen) voordat de formalisering plaatsvindt.
• Recursieve Decompositie: De Proof Detailer en Lemma Breakdown agents breken het bewijs af in beheersbare lemmas.
• Top-Down Proving: Het systeem bewijst ouder-nodes door kind-lemmas eerst als onbewezen premissen (sorry) te gebruiken. Pas nadat het ouder-bewijs is vastgesteld, wordt er gerecurseerd om de kinderen te bewijzen. Dit zorgt ervoor dat kind-lemmas daadwerkelijk bruikbaar zijn voor het ouder-doel.
• Axiom Handling: Eerder geciteerde werkzaamheden in het paper worden als axioma's toegelaten in plaats van opnieuw bewezen, waardoor de formalisatie-inspanning wordt geïsoleerd tot de kernbijdragen van het paper. Echter, voor benchmark-evaluatie (PutnamBench) wordt dit pad uitgeschakeld om zelfstandige bewijzen te garanderen.
• Failure Handling: Als een bewijsverslag faalt, biedt het systeem een gestructureerde diagnose (bijv. ontbrekende hypothese, conflicterend lemma) en activeert het specifieke herstelstrategieën (bijv. het lemma opnieuw afbreken, of een blad promoten naar een niet-blad).

Belangrijkste Bijdragen

1. Methodologische Verschuiving: De toepassing van software engineering principes—specifiek objectgeoriënteerde type-decompositie en unit-test-stijl auxiliary lemma verificatie—op wiskundige autoformalizatie.
2. Agentic Framework: Een multi-agent systeem dat gebruikmaakt van de dynamische, niet-lineaire capaciteiten van moderne programmeerkaders om de beperkingen van enkelvoudige agenten en vaste pipelines te overwinnen.
3. Type-First Formalization: Een nieuwe benadering om de kloof in formele bibliotheken te overbruggen door dynamisch nieuwe types te definiëren en te valideren voordat stellingen worden bewezen.
4. Recursive Proof Formalization: Een pipeline die machine-gecontroleerde bewijzen produceert voor onderzoekswiskunde, in staat om hiaten in gepubliceerde bewijzen te identificeren.
5. Kostenefficiëntie: Een demonstratie dat hoogwaardige autoformalizatie haalbaar is met standaard commerciële abonnementen zonder lokale GPU's.

Resultaten

PutnamBench Evaluatie

Het systeem werd geëvalueerd op een willekeurige steekproef van 32 problemen uit PutnamBench (totaal 672 problemen).

• Prestaties: De pipeline loste alle 32 gesamplede problemen op.
• Nauwkeurigheid: Dit vestigt een ondergrens van een nauwkeurigheid van 91,3% over de gehele dataset bij een betrouwbaarheidsniveau van 95%.
• Kosten: De gemiddelde operationele kosten waren ongeveer $5 per probleem, bereikt met een standaard $200/maand software-abonnement. Dit contrasteert scherp met concurrerende methoden die aanzienlijke GPU-bronnen vereisen of kosten boven de $54 per probleem met zich meebrengen.

Onderzoekswiskunde (STOC Papers)

Het systeem werd toegepast op vijf papers van het ACM Symposium on Theory of Computing (STOC), variërend van combinatoriek en communicatiecomplexiteit tot mechanismeontwerp en leertheorie.

• Succes van Formalisering: Het systeem slaagde erin de hoofdstellingen van alle vijf de papers te formaliseren. Menselijke experts verifieerden dat de formalisaties de oorspronkelijke bewijsstrategieën getrouw weergeven.
• Gebruik van Axioma's:
  • Twee papers (Mackenzie & Saffidine; Gravin & Jia) werden bewezen met geen axioma's buiten de standaard Lean kernel. Het systeem heeft zelfs eerder geciteerde resultaten vanaf nul opnieuw bewezen.
  • Andere papers vereisten het toelaten van bekende externe stellingen als expliciete axioma's, wat de zelfstandigheid van de oorspronkelijke papers accuraat weerspiegelt.
• Gap Detectie: Bij het formaliseren van Pham [17] identificeerde het systeem een gat in het gepubliceerde bewijs van een specifieke lemma (Lemma 3.9 bound). Het systeem vond een tegenvoorbeeld dat aantoonde dat een structurele lemma die in het bewijs van het paper werd gebruikt, zoals gesteld onjuist was. Het systeem nam de bound op als een axioma en bewees de rest van het paper, wat de capaciteit van de pipeline demonstreert om fouten in peer-reviewed literatuur aan het licht te brengen.

Betekenis en Claims

Het paper claimt dat dit framework een cruciale stap vormt voor AI-ondersteunde wiskunde door:

1. Barrières te Verlagen: Het drastisch verminderen van de kosten en hardwarevereisten voor automatisch bewijsleveren, waardoor het toegankelijk wordt zonder lokale GPU's.
2. Complexiteit aan te Pakken: Het succesvol formaliseren van onderzoekswiskunde die de scope van bestaande bibliotheken overstijgt via dynamische type-definitie en validatie.
3. Wetenschappelijke Nut: Het bieden van een tool die niet alleen bewijzen verifieert, maar ook subtiele fouten in gepubliceerde wiskundige argumenten kan detecteren, zoals aangetoond door de gevonden gap in het Pham [17] paper.
4. Schaalbaarheid: Het demonstreren dat algemene programmeer-LLM's, wanneer effectief georchestreerd, beter presteren dan kleinere, gespecialiseerde modellen die voor Lean zijn gefinetuned, vooral bij complexe, onderzoeksgraad taken.

De auteurs benadrukken dat het vermogen van het systeem om machine-gecontroleerde bewijzen te produceren voor STOC-papers, inclus\nclusief twee met nul externe axioma's, de haalbaarheid valideert van volledig geautomatiseerde, rigoureuze wiskundige verificatie aan de onderzoeksgrens.