DRIFT: Decompose, Retrieve, Illustrate, then Formalize Theorems

Probleemstelling

Het automatiseren van de formalisatie van wiskundige stellingen (autoformalization) voor theorem-provers zoals Lean blijft een grote uitdaging voor Large Language Models (LLMs). Bestaande methoden, die vaak gebruikmaken van Retrieval-Augmented Generation (RAG), hebben twee fundamentele beperkingen:

1. Complexiteit van informele statements: Informele wiskundige zinnen zijn vaak dicht en multifaceted. Het direct gebruiken van een volledige informele zin als zoekopdracht voor een externe bibliotheek (zoals Mathlib) leidt tot suboptimale resultaten omdat de zoekopdracht te vaag is om de specifieke, atomaire definitie te vinden die nodig is.
2. Gebrek aan contextueel gebruik: Zelfs als de juiste formele definities worden opgehaald, missen modellen vaak de kennis over hoe deze definities correct in syntaxis en structuur moeten worden toegepast binnen een stelling. Bestaande methoden leveren vaak alleen definities zonder voorbeelden van gebruik, wat leidt tot syntactische en semantische fouten.

Methodologie: Het DRIFT Framework

DRIFT (Decompose, Retrieve, Illustrate, then Formalize Theorems) is een nieuw raamwerk dat deze problemen aanpakt door een vierstapsproces te implementeren dat is ontworpen om de afhankelijkheidsstructuur van formele wiskunde te volgen.

1. Decompose (Ontleden):

   • In plaats van de volledige informele zin als één query te gebruiken, deelt een LLM de zin op in kleinere, atomaire sub-vragen (sub-queries).
   • Elke sub-vraag richt zich op één specifiek wiskundig concept (bijv. "wat is een priemgetal van de vorm 4t+3?").
   • De LLM genereert ook een voorspelde formele representatie voor elk concept, wat dient als een syntactisch anker voor de retriever.

2. Retrieve (Ophalen):

   • Voor elke gegenereerde sub-vraag wordt een dichte passage-retriever (DPR) gebruikt om de exacte afhankelijke premissen (definities, lemmata) uit de formele bibliotheek (bijv. Mathlib) op te halen.
   • Door de zoekopdrachten te verfijnen tot atomaire concepten, wordt de precisie en recall van het ophalen van de juiste definities aanzienlijk verbeterd ten opzichte van monolithische zoekopdrachten.

3. Illustrate (Illustreren):

   • Dit is een cruciale stap om de kloof tussen definitie en gebruik te overbruggen. Het systeem selecteert een klein aantal illustrerende stellingen uit de bibliotheek die de opgehaalde premissen daadwerkelijk gebruiken.
   • Een gulzig algoritme kiest stellingen die de grootste dekking bieden van de opgehaalde premissen.
   • Deze voorbeelden fungeren als "scaffolding" (steigers) voor het model, waardoor het de correcte syntaxis en patronen voor het gebruik van de definities kan zien.

4. Formalize Theorems (Formaliseren):

   • Een finalizer (LLM) genereert de uiteindelijke formele stelling in Lean 4.
   • De prompt bevat de originele informele zin, de verzameling opgehaalde premissen, de illustrerende stellingen en instructies.
   • Het model synthetiseert de formele code door te leren van de contextuele voorbeelden en de specifieke definities.

Belangrijkste Bijdragen

1. Innovatief Framework: DRIFT introduceert een decompositie-gedreven aanpak die informele statements omzet in gerichte zoekopdrachten, gevolgd door contextuele verrijking via illustrerende voorbeelden. Dit sluit de kloof tussen formele definities en hun syntactisch correcte gebruik.
2. State-of-the-art Resultaten: Het framework bereikt nieuwe state-of-the-art resultaten in afhankelijkheidsretrieval en autoformalisatie op diverse benchmarks, inclusief ProofNet en het uit-distributie ConNF-benchmark.
3. Inzicht in Modelgrenzen: De analyse toont aan dat de effectiviteit van opgehaalde kennis sterk afhankelijk is van de parametrische kennis van het model. DRIFT is vooral effectief bij modellen die moeite hebben met specifieke formele syntax of bij uit-distributie taken.

Resultaten

Het paper evalueert DRIFT op drie benchmarks: ProofNet (in-distributie), MiniF2F-test (zelfstandige problemen met weinig afhankelijkheden) en ConNF (uit-distributie, gebaseerd op Quine's New Foundations).

• Retrieval Performance: Op ProofNet verdubbelde DRIFT de F1-score voor het ophalen van premissen bijna ten opzichte van de DPR-baseline (van ~13,77% naar ~27,68% met Claude-Opus-4).
• Autoformalisatie Performance:
  • ConNF (OOD): DRIFT toont een opmerkelijke prestatieverbetering op dit moeilijke, uit-distributie benchmark. Met GPT-4.1 steeg de BEq+@10 score met 55,57% ten opzichte van de zero-shot baseline, en zelfs 3,43% boven de "Oracle*" baseline (die de grondwaarheid premissen bevat maar geen gebruikskaders).
  • ProofNet: DRIFT verbeterde consistent de prestaties ten opzichte van zowel zero-shot als de sterke RAuto-baseline.
  • MiniF2F-test: Op dit benchmark met zeer weinig externe afhankelijkheden is het effect gematigd; hier kan extra context soms als afleiding werken, wat aantoont dat adaptieve strategieën nodig zijn.
• Ablatie Study: Het verwijderen van de "Illustrate"-module leidt tot een significante daling in prestaties, wat bevestigt dat voorbeelden van gebruik essentieel zijn voor het correct integreren van premissen.

Betekenis en Conclusie

DRIFT demonstreert dat het simpelweg ophalen van definities onvoldoende is voor succesvolle autoformalisatie. De kerninzicht is dat modellen niet alleen wat ze nodig hebben (definities) moeten weten, maar ook hoe ze deze moeten gebruiken (syntactische patronen).

De studie benadrukt de noodzaak van adaptieve retrieval-strategieën. Voor complexe, afhankelijkheidsrijke problemen (zoals ConNF) is DRIFT superieur, terwijl voor eenvoudige, zelfstandige problemen (zoals MiniF2F) een dynamische keuze tussen retrieval en zero-shot nodig is. DRIFT biedt een robuust, model-onafhankelijk raamwerk dat de betrouwbaarheid van geautomatiseerde wiskundige formalisatie aanzienlijk verbetert en een pad effent voor toekomstige agentische systemen die iteratief kunnen leren van compiler-feedback.