Technische Samenvatting: MATHLIBPR – Een Benchmark voor de Review-klare Staat van Formele Wiskundige Bibliotheken

1. Probleemdefinitie

Het ecosysteem van Lean en Mathlib is de standaard geworden voor formeel redeneren met ondersteuning van grote taalmodellen (LLM), met recente successen in het oplossen van problemen op Olympiade-niveau (MiniF2F), competitiewiskunde (AlphaProof) en grootschalige formalisatieprojecten (Gauss-agent). Deze systemen consumeren Mathlib echter voornamelijk als afhankelijkheid in plaats van er aan bij te dragen. Hoewel door LLM's gegenereerde code door de Lean-kern kan worden geverifieerd op correctheid, vereist het bepalen of een bijdrage "merge-ready" is – dat wil zeggen, voldoet aan gemeenschapsconventies, de coherentie van de bibliotheek behoudt en geschikt is voor langdurig onderhoud – menselijke review.

Menselijke review is momenteel de belangrijkste knelpunt voor de groei van Mathlib, met een achterstand van ongeveer 300 pull requests (PR's) en een mediane wachttijd van twee weken. De centrale vraag die in dit artikel wordt behandeld is: Kunnen LLM's helpen bij het reviewen van Mathlib PR's? Specifiek: kunnen ze onderscheid maken tussen code die de build haalt en klaar is voor integratie, en code die de build haalt maar herziening vereist of zal worden afgewezen?

2. Methodologie

2.1 Datasetconstructie: MATHLIBPR

De auteurs introduceren MATHLIBPR, een benchmark opgebouwd uit echte PR-historie van Mathlib4.

• Bron: Gesloten PR's uit de repository leanprover-community/mathlib4 (per 5 april 2026).
• Selectiecriteria: De benchmark richt zich uitsluitend op snapshots die de build halen. Dit elimineert triviale strategieën gebaseerd op syntaxisfouten of compilatiefouten en dwingt modellen om te oordelen op basis van codekwaliteit en conventies.
• Labels:
  • Merge Ready: Snapshots die zijn geaccepteerd in de master-branch.
  • Niet Merge Ready: Snapshots die de build-controles haalden, maar ofwel werden herzien voordat ze werden geaccepteerd, ofwel behoorden tot PR's die nooit werden samengevoegd.
• Samenstelling: De definitieve dataset bevat 15.895 gelabelde snapshots van 12.063 PR's (11.409 merge-ready, 4.486 niet-merge-ready). Het bevat 3.687 paren binnen een PR (een eerdere snapshot die de build haalde versus de uiteindelijk geaccepteerde versie) om herkenning van vooruitgang in herziening te testen.

2.2 Evaluatieprotocol

De auteurs stellen een driefasen evaluatieprotocol voor dat modellen geleidelijk aan rijkere context biedt:

• Fase 1: Code-lokale bewijslast (diff, gewijzigde bestanden) en compacte samenvattingen van Mathlib-richtlijnen (namenstijl, stijl, documentatie).
• Fase 2: Voegt gestructureerde diagnostiek toe (linting, imports, plaatsing van declaraties, API-aansluiting) afgeleid van historische GitHub-checkrecords of lokaal aangevuld.
• Fase 3: Voegt PR-titel en -beschrijving toe als bedoeling.

2.3 Geëvalueerde Systemen

De benchmark evalueert twee klassen van systemen:

1. LLM-modellen: DeepSeek-R1-Distill-Qwen, Qwen3-8B, Goedel-Prover-V2-32B (vooraf gefinetuned op Mathlib) en Kimina-Prover-Distill-8B.
2. LLM-agenten: Codex (GPT-5.4) en Claude Code (Claude Sonnet 4.6). Agenten opereren in een read-only lokale repository-checkout, met beperkingen om bestanden te bewerken, toegang tot het web te krijgen of PR-uitkomsten op te halen.

2.4 Outputschema en Metrieken

Systemen moeten een gestructureerde JSON-review outputten in plaats van vrije tekst. Het schema omvat:

• Verdict: merge_ready, not_merge_ready of uncertain.
• Score: Een scalair merge-ready-score ($p_{merge\_ready}$).
• Assen: Beoordelingen over acht rubric-dimensies (namenstijl, documentatie, lokale structuur, bestandsplaatsing, imports, leesbaarheid van bewijzen, API-aansluiting, overlap met repository).

Metrieken:

• MR/NMR Recall: Recall voor de klassen merge-ready en niet-merge-ready (waarbij uncertain en ongeldige outputs als fouten worden beschouwd).
• Gebalanceerde Nauwkeurigheid: Gemiddelde van MR- en NMR-recall.
• Valid-Output Rate: Percentage van outputs die voldoen aan het schema binnen de runtime-begroting.
• AUROC: Oppervlakte onder de ROC-curve gebaseerd op scalair scores.

3. Belangrijkste Resultaten

3.1 Algemene Prestaties

• Lage Nauwkeurigheid: Geen enkel systeem onderscheidt betrouwbaar merge-ready van niet-merge-ready snapshots. Het best presterende model (DeepSeek) behaalde een Gebalanceerde Nauwkeurigheid van 36,0% in Fase 3, significant onder de 50% toevalsbasislijn voor een gebalanceerde taak (hoewel de dataset onevenwichtig is, benadrukken de recall-metrieken het falen).
• Klasseasymmetrie: Systemen vertonen een sterke bias richting het voorspellen van merge_ready.
  • DeepSeek (Fase 3): 69,8% MR Recall, maar slechts 2,3% NMR Recall.
  • Qwen (Fase 3): 48,3% MR Recall, 0,0% NMR Recall.
  • Codex (Agent): 92,0% MR Recall, maar slechts 12,0% NMR Recall.
• Invloed van Context: Het toevoegen van diagnostiek en PR-voornemen (Fase 2 en 3) leverde beperkte en ongelijke winst op. Zo verbeterde de gebalanceerde nauwkeurigheid van DeepSeek van 18,1% naar 36,0%, maar bleef het vermogen om niet-merge-ready code te identificeren dicht bij nul.

3.2 Agent versus Model Prestaties

• Agenten: Hoewel Codex hoge operationele betrouwbaarheid toonde (99,9% geldige outputrate) en hoge MR Recall, slaagde het er niet in niet-merge-ready code te identificeren. Claude Code had een lagere betrouwbaarheid (56,4% geldige rate) en vergelijkbaar slechte NMR recall.
• Gespecialiseerde Modellen: Goedel en Kimina, ondanks training op formele bewijzen, presteerden slecht. Goedel's geldige outputrate stortte in van 68,3% (Fase 1) naar 13,5% (Fase 3), en beide modellen produceerden vaak ongeldige outputs (proza of codeblokken) in plaats van het vereiste JSON-schema.

3.3 Analyse Binnen PR

In een gecontroleerde vergelijking van eerdere snapshots die de build haalden versus de uiteindelijk geaccepteerde snapshots uit dezelfde PR:

• Modellen deden nauwelijks beter dan toeval. De pairwise-nauwkeurigheid van DeepSeek plateauerde op 51,1% (Fase 3), en Qwen bleef rond 49,1%.
• Dit geeft aan dat modellen niet betrouwbaar de specifieke verbeteringen kunnen detecteren die leidden tot de acceptatie van een PR, zelfs niet bij het vergelijken van twee versies van dezelfde bijdrage.

3.4 Foutanalyse

• Afweging: Systemen weigeren vaak (uncertain) bij assen zoals documentatie of leesbaarheid van bewijzen.
• Ongeldige Outputs: Een aanzienlijk deel van de outputs van gespecialiseerde modellen (Goedel, Kimina) en agenten (Claude Code) was ongeldig vanwege schendingen van het schema, time-outs of het niet produceren van JSON. Dit suggereert een mismatch tussen de trainingsdoelen van de modellen (bewijsvoering) en de gestructureerde review-interface.

4. Bijdragen

1. MATHLIBPR Benchmark: De eerste benchmark voor het evalueren van LLM's op de merge-ready staat van build-haalt Mathlib-bijdragen, afgeleid van echte PR-historie.
2. Gestaffeld Evaluatieprotocol: Een protocol dat systematisch test of rijkere context (diagnostiek, PR-voornemen) de beoordeling door een reviewer-achtig oordeel verbetert.
3. Empirische Studie: Een uitgebreide evaluatie die aantoont dat huidige LLM's en agenten moeite hebben om merge-ready code te onderscheiden van build-haalt code die herziening vereist, wat een kloof benadrukt tussen codecorrectheid en de kwaliteit van bibliotheekintegratie.

5. Betekenis en Beweringen

Het artikel beweert dat MATHLIBPR een stap voorwaarts biedt naar reviewer-assistenten en reward-modellen voor formele wiskundige bibliotheken.

• Huidige Staat: De resultaten tonen aan dat het beoordelen van merge-ready staat een aanzienlijk moeilijkere capaciteit is dan het detecteren van syntaxisfouten of compilatiefouten. Huidige systemen slagen er niet in de genuanceerde reviewnormen te vangen die nodig zijn om een geïntegreerde wiskundige bibliotheek te cureren.
• Toekomstig Nut: De benchmark is bedoeld om te worden gebruikt voor:
  • Reviewer-assistentie: Triage en aan het licht brengen van waarschijnlijke blokkades voor menselijke reviewers.
  • Reward Modeling: Het trainen van reward-modellen met behulp van de structuur van binnen-PR-paren (de voorkeur geven aan de uiteindelijk geaccepteerde snapshot boven een eerdere build-haalt versie) om LLM's te sturen naar het genereren van code die niet alleen correct is, maar ook onderhoudbaar en merge-ready.
• Beperkingen: De auteurs erkennen dat de benchmark een selectief stukje PR-historie bestrijkt en dat labels zijn afgeleid van historische beslissingen van maintainers, die niet-technische factoren kunnen bevatten. Ze stellen expliciet dat het doel niet is om menselijke reviewers te vervangen, maar om een adviserend signaal te bieden.

Concluderend: hoewel LLM's succesvol zijn geweest in het genereren van correcte bewijzen, vereist de overgang naar het bijdragen aan Mathlib een niveau van oordeel over codestijl, documentatie en aansluiting bij de bibliotheek dat huidige modellen nog niet hebben onder de knie. MATHLIBPR legt de basislijn vast voor het meten van vooruitgang in deze richting.