Lean-GAP: A Dataset of Formalized Graduate Algebra Problems

Technische Samenvatting van LEAN-GAP: Een Dataset van Geformaliseerde Graduate Algebra Problemen

Probleemstelling
Ondanks aanzienlijke vooruitgang in geautomatiseerd redeneren en grote taalmodellen (LLM's), blijft er een substantiële kloof bestaan tussen informele wiskundige kennis en de formele tegenhangers in bewijsassistenten zoals Lean 4. Hoewel recente inspanningen succesvol zijn geweest in het formaliseren van competitie-stijl problemen of hooggespecialiseerde stellingen, is er een tekort aan representatieve, gestructureerde datasets die standaard materiaal op graduate-niveau dekken. Dit gebrek aan fundamentele curriculumdata belemmert de ontwikkeling van systemen voor geautomatiseerd redeneren, aangezien deze vaak worden getraind op "uitdagende problemen" zonder de systematische conceptuele ontwikkeling die in standaard tekstboeken aanwezig is. Bovendien, hoewel autoformalisatie vooruitgang heeft geboekt, blijft het verifiëren of een gegenereerde formele bewering daadwerkelijk de beoogde betekenis van een informele bewering vangt, een kritieke, onopgeloste bottleneck.

Methodologie
De auteurs presenteren LEAN-GAP (Lean-Graduate Algebra Problems), een dataset afgeleid van 430 geformaliseerde oefeningen uit het tekstboek Abstract Algebra door Dummit en Foote. Het project maakt gebruik van een schaalbare, drie-fasen pijplijn:

1. PDF-naar-LATEX Preprocessing: Gescande PDF-pagina's van het tekstboek worden gerenderd als afbeeldingen, bijgesneden om overbodige elementen te verwijderen, en verwerkt via de Mathpix Convert API om initiële LATEX-transcripties van de oefenstellingen te genereren.
2. LATEX-naar-Lean Autoformalizatie: Een prompt-gebaseerde aanpak met diverse LLM's vertaalt de LATEX-stellingen naar Lean 4-code. De prompts dwingen consistente naamgevingsconventies af (bijv. DF_{sec}_{subsec}_{exercise_num}), compatibiliteit met Mathlib, en de inclusie van sorry-placeholders voor bewijzen. De auteurs evalueerden zes systemen: vijf single-shot modellen (GPT-5, Gemma4-31B, Goedel-Formalizer-V2-32B, Qwen3.6-35B-A3B, DeepSeek-R1-Distill-Qwen-32B) en een iteratieve agent-loop (Codex).
3. Verificatie van de Informeel–Formeel Correspondentie: In het besef dat succesvolle compilatie geen garantie biedt voor semantische correctheid, hebben de auteurs een rigoureuze human-in-the-loop verificatieworkflow geïmplementeerd.
   • Contributor Fase: Een contributor herschrijft de oefening als een zelfstandige stelling en formaliseert deze in Lean, en dient vervolgens een Pull Request (PR) in.
   • Geautomatiseerde Check: GitHub CI verifieert dat de Lean-code elaboreert tegen een gepinde Mathlib-revisie.
   • Maintainer Review: Een onafhankelijke maintainer voert een semantische review uit, waarbij wordt gecontroleerd of de Lean-declaratie de wiskundige inhoud van de informele stelling werkelijk vangt.
   • AI-Geassisteerde Correctie: Tools zoals Claude Opus 4.7 en Aristotle worden ingezet als "second readers" om subtiele semantische fouten te detecteren, zoals omgedraaide kwantoren of ontbrekende restricties (bijv. $n \ge 2$) die menselijke reviewers aanvankelijk over het hoofd zouden kunnen zien.

Belangrijkste Bijdragen

1. De LEAN-GAP Dataset: Een gestructureerde corpus van 430 geformaliseerde graduate algebra oefeningen, georganiseerd per onderwerp en moeilijkheidsgraad, dekkend groepentheorie, ringtheorie, veldentheorie en Galois-theorie.
2. Systematische Formalisatiepijplijn: Een reproduceerbare methodologie voor het converteren van tekstboekoefeningen naar formele stellingen, waarbij de noodzaak van menselijk toezicht in de verificatiefase wordt benadrukt.
3. Analyse van Formalisatie-uitdagingen: Een gedetailleerde examinatie van terugkerende bottlenecks, waaronder:
   • Geometrische argumenten: Oefeningen die constructies met liniaal en passer betreffen, zijn moeilijk te formaliseren vanwege het gebrek aan robuuste geometrische infrastructuur in Mathlib.
   • Antwoord-ingebedde formalisatie: Problemen die het enumereren van oplossingen vereisen, vormen een uitdaging bij het onderscheiden tussen het verifiëren van een gegeven antwoord en het ontdekken ervan.
   • Ontbrekende definities: Oefeningen die concepten vereisen die nog niet in Mathlib aanwezig zijn (bijv. specifieke Frobenius-groepen), vereisen aangepaste definities die zorgvuldig moeten worden geconstrueerd om overeen te komen met de intentie van het tekstboek.
   • Subtiele ambiguïteiten: Informele stellingen bevatten vaak impliciete restricties (bijv. $n \ge 2$) die, indien weggelaten, de formele stelling onwaar maken in de logica van Lean (bijv. door het gedrag van aftrekken bij natuurlijke getallen).

Resultaten
De auteurs evalueerden de prestaties van verschillende autoformalisatie-modellen op de volledige set van 1.966 oefeningen:

• Elaboratie Succes: Codex (een iteratieve agent-loop) behaalde het hoogste succespercentage van 95,5%, waarmee het single-shot modellen aanzienlijk overtrof. GPT-5 leidde de single-shot modellen met 44,1% van de oefeningen die volledig elaboreerden.
• Semantische Getrouwheid: Hoewel syntactisch succes (elaboratie) noodzakelijk is, is het niet voldoende. Een LLM-gebaseerde semantische rechter (Claude Opus 4.7) evalueerde de getrouwheid van de stellingen. GPT-5 behaalde een gemiddelde score van 3,45/5, waarbij 45,1% van de outputs als "getrouw" werd beschouwd. In contrast hiermee scoorde DeepSeek-R1 aanzienlijk lager (1,15/5), waarbij het vaak faalde om declaraties te genereren of vacuüm stellingen produceerde.
• Complementariteit van Modellen: De modellen vertoonden een hoge mate van onenigheid; slechts 7 oefeningen werden door alle systemen opgelost, terwijl 654 door exact één systeem werden opgelost. Dit onderstreept de waarde van het draaien van modellen in parallel.
• Noodzaak van Menselijke Verificatie: De verificatiefase bleek het meest arbeidsintensief. Zelfs met hoge elaboratiepercentages bevatten veel stellingen semantische fouten (bijv. verkeerde groepsnamen, omgedraaide kwantoren) die deskundige menselijke interventie vereisten om op te lossen.

Betekenis
Het artikel stelt dat LEAN-GAP een kritieke kloof adresseert in de trainingsdata voor AI-systemen, door verder te gaan dan competitie-benchmarks naar standaard graduate-curricula. Het werk demonstreert dat, hoewel LLM's de initiële vertaling van wiskundige tekst kunnen automatiseren, ze nog niet in staat zijn om end-to-end autoformaliseerders te zijn voor standaardmateriaal vanwege hardnekkige semantische hiaten. De auteurs betogen dat de toekomst van formalisatie ligt in productieve mens-AI-samenwerking, waarbij AI fungeert als een "second reader" om subtiele fouten en niet-geëxpliciteerde hypothesen te identificeren, terwijl menselijke wiskundigen het noodzakelijke toezicht bieden op de semantische getrouwheid. Deze aanpak biedt een sjabloon voor het opschalen van de formalisatie van standaard wiskundige trainingsmaterialen, wat potentieel kan dienen als een fundament voor de ontwikkeling van "AI-wiskundestudenten" die in staat zijn om standaard curricula te beheersen.