Technische Samenvatting: Formalize Once, Edit the Rest (BASE)

1. Probleemstelling

Naarmate Large Language Models (LLMs) steeds vaker worden toegepast op wiskundige redenering, genereren ze vaak meerdere verschillende redeneerpaden en kandidaat-antwoorden voor één enkel probleem. Een kritieke uitdaging ontstaat bij de antwoordselectie: hoe te verifiëren welk kandidaat-antwoord correct is zonder toegang tot grondwaarheid-labels tijdens test-time scaling.

Hoewel bestaande benaderingen zoals meerderheidsstemmen (majority voting) of geleerde beloningsmodellen statistische signalen bieden, missen zij formele garanties. Recent werk heeft gebruikgemaakt van formele bewijsassistenten (specifiek Lean 4) om kandidaten te verifiëren. In dit paradigma vertaalt een "autoformalizer" een probleem en een kandidaat-antwoord naar een Lean-stelling die de correctheid van het antwoord beweert. Een prover probeert vervolgens deze stelling te verifiëren.

Er bestaat echter een significante bottleneck: om $K$ kandidaat-antwoorden te verifiëren, moet de autoformalizer $K$ keer onafhankelijk worden aangeroepen. Dit brengt een computationele kostenpost met zich mee van $\Theta(K)$, wat lineair schaalt met het aantal samples. De auteurs observeren dat voor een enkel probleem de $K$ formele stellingen bijna identiek zijn, waarbij ze dezelfde probleemstructuur delen en alleen verschillen in de expressie van het antwoord. Het kernproblek is hoe de gedeelde structuur kan worden benut om de formaliseringskosten te reduceren van $\Theta(K)$ naar $\Theta(1)$ zonder de selectienauwkeurigheid op te offeren.

2. Methodologie: De BASE-pipeline

De auteurs stellen BASE (Base-and-Substitute-Edit) voor, een pipeline die is ontworpen om een enkele "base" kandidaat te formaliseren en de resterende $K-1$ stellingen af te leiden door middel van gelokaliseerde bewerkingen.

2.1 Base Discovery (Ontdekking van de basis)

De pipeline begint met een upstream solver die een gerangschikte lijst genereert van $K$ kandidaat-antwoorden, $S(x) = (a_1, \dots, a_K)$, geordend op basis van de betrouwbaarheid van de solver.

• Het systeem iterereert door de kandidaten in rangorde.
• Voor elke kandidaat $a_i$ probeert het het probleem-antwoord paar $(x, a_i)$ te formaliseren naar een Lean-stelling $F_i$.
• Het proces stopt bij de eerste kandidaat $a_b$ waarvan de formele stelling $F_b$ succesvol type-checkt in Lean.
• $F_b$ wordt de base formalization (basis-formalisering), en $a_b$ is het base answer (basis-antwoord).
• Als geen enkele kandidaat type-checkt, valt het systeem terug op de bovstaan in rang geplaatste kandidaat $a_1$.

2.2 Substitution Cascade (Substitutie-cascade)

Zodra een geldige base $F_b$ is vastgesteld, genereert het systeem de overige $K-1$ stellingen door $F_b$ ter plaatse te bewerken om de andere kandidaten te reflecteren. Dit wordt afgehandeld via een twee-lagen cascade:

1. Tier 1 (R1): Regelgebaseerde directe lokalisatie

   • Het systeem probeert de antwoord-expressie te lokaliseren in $F_b$ via exacte string matching binnen een "gated region" (de body van de stelling, exclusief comments/headers).
   • Indien een unieke match wordt gevonden, voert het systeem een directe substitutie uit van de antwoord-string.
   • Indien meerdere matches optreden, selecteert een klein disambiguatie-model de juiste slot.
   • Deze tier is efficiënt maar faalt wanneer de autoformalizer het antwoord in een syntactisch diverse vorm codeert (bijv. een tuple (3, 5) gecodeerd als aparte bindings of een Prod waarde) in plaats van een letterlijke string.

2. Tier 2 (R2): LEANSCRIBE (Geleerde herschrijver)

   • Voor gevallen waar R1 faalt, roept het systeem LEANSCRIBE aan, een gespecialiseerd fine-tuned LLM.
   • Input: Het probleem $x$, de base formalization $F_b$, en het base answer $a_b$.
   • Output:
     • Een lokale blok $s$: Een aaneengesloten segment van $F_b$ dat de antwoord-afhankelijke expressie bevat.
     • Een fill functie $f$: Een lichtgewicht Python-functie die elk informeel antwoord $a_i$ mapt naar de corresponderende Lean-expressie die $s$ vervangt.
   • Executie: LEANSCRIBE draait één keer per probleem. De gegenereerde functie $f$ wordt vervolgens toegepast op alle overige kandidaten $a_i$ om hun formele stellingen $F_i = f(a_i)$ te produceren. Dit amortiseert de kosten van de model call over alle $K-1$ kandidaten.

2.3 Verificatie en Selectie

De pipeline vertrouwt op statement-level type-checking als het primaire selectiesignaal.

• Een kandidaat wordt beschouwd als "geverifieerd" indien de formele stelling $F_i$ type-checkt in Lean (d.w.z. een goed gevormde propositie is).
• Het systeem selecteert de hoogst gerangschikte kandidaat $a_j$ waarvoor $F_j$ type-checkt.
• Als geen enkele kandidaat type-checkt, valt het systeem terug op de bovstaan in rang geplaatste kandidaat $a_1$.
• De auteurs merken op dat hoewel bewijs-niveau verificatie (het draaien van een prover) rigoureuzer is, huidige provers een lage pass@1 rate hebben, waardoor statement-level type-checking een praktischer signaal is voor selectie in deze budgetbeperkte setting.

3. Belangrijkste Bijdragen

1. BASE Pipeline: Het eerste werk dat de formaliseringskosten amortiseert door een enkele geverifieerde base stelling te delen over meerdere kandidaten, waardoor de autoformalizer oproepen worden gereduceerd van $\Theta(K)$ naar $\Theta(1)$.
2. LEANSCRIBE Model: Een geleerde herschrijver getraind om antwoord-afhankelijke blokken te lokaliseren en herbruikbare edit-functies te genereren, wat de syntactische variaties afhandelt die regelgebaseerde substitutie niet kan behandelen.
3. Pareto-verbetering: De methode bereikt een hogere selectienauwkeurigheid terwijl de computationele kosten over alle geteste configuraties aanzienlijk worden verminderd.

4. Experimentele Resultaten

De auteurs evalueerden BASE op vier benchmarks (MATH-500, OlympiadBench, AMC-AIMO, AIME 2024) met drie verschillende upstream solvers (Gemini 3 Pro, Qwen3-8B, DeepSeek-R1-Qwen3-8B) met $K=8$ kandidaten.

• Nauwkeurigheid: BASE verbeterde de selectienauwkeurigheid (Acc) in alle 12 (dataset, solver) configuraties vergeleken met onafhankelijke formalisering, met winsten variërend van +0,7 tot +23,3 procentpunten.
• Robuustheid: De "Gold-Answer Pass" rate (GT-pass)—het deel van de problemen waarbij de stelling van het juiste antwoord type-checkt—nam significant toe (tot +33,3 punten), en bereikte in veel gevallen 96–100%. Dit geeft aan dat het delen van een geverifieerde base de formalisering van het correcte antwoord robuuster maakt.
• Kostenefficiëntie: Bij $K=8$ verminderde BASE het aantal autoformalizer oproepen met ongeveer 5,4× (gemiddelde reductie van 4,7–6,5×). De kosten schalen als $\Theta(1)$ in plaats van $\Theta(K)$.
• Ablatie: Het verwijderen van de geleerde herschrijver (LEANSCRIBE) en het uitsluitend vertrouwen op regelgebaseerde substitutie (R1) resulteerde in een significante daling in de dekking van kandidaten (8–22 procentpunten), wat de noodzaak van het geleerde component aantoont voor het afhandelen van diverse syntactische coderingen.
• Bewijs-niveau Analyse: Zelfs wanneer een prover (DeepSeek-Prover-V2) wordt gebruikt met een enkele poging per kandidaat, verbeterde BASE de bewijs-niveau nauwkeurigheid in 11 van de 12 configuraties, wat suggereert dat beter gestructureerde formele stellingen downstream provers helpen.

5. Betekenis en Claims

Het artikel claimt dat BASE een Pareto-verbetering vormt voor Lean-gebaseerde antwoordselectie. Door één keer te formaliseren en de rest te bewerken, doet de methode tegelijkertijd het volgende:

• Verlaagt de Kosten: Vermindert de inference kosten van formele verificatie drastisch, wat test-time scaling met een grote $K$ levensvatbaarder maakt.
• Verbetert de Nauwkeurigheid: Verhoogt de betrouwbaarheid van het selecteren van het juiste antwoord, waarschijnlijk omdat de gedeelde base structuur de variantie en de foutratio van de autoformalizer voor de correcte kandidaat vermindert.

De auteurs benadrukken dat deze aanpak een "drop-in replacement" is voor de formaliseringsfase in bestaande pipelines (gedemonstreerd door integratie in de FANS pipeline), en dat de winsten worden gedreven door het vermogen van de verifier om correcte antwoorden effectiever te behouden wanneer een gedeelde, geverifieerde scaffold wordt gebruikt, in plaats van door veranderingen in de upstream solver-generatie.

Het werk erkent beperkingen en merkt op dat het zich richt op statement-level type-checking vanwege de huidige beperkingen van provers, en ervan uitgaat dat kandidaat-antwoorden een probleem-zijde structuur delen. Het claimt niet de getrouwheid (faithfulness) van autoformalisering op te lossen (waarbij een incorrect antwoord nog steeds kan type-checken), maar suggereert dat het combineren van formele signalen met solver-rangschikkingen dit risico mitigeert.