Technische Samenvatting: Monotone Referentievrije Verfijning voor Autoformalisatie

1. Probleemstelling

Hoewel Large Language Models (LLM's) de wiskundige redenering hebben verbeterd, blijft volledige-stelling autoformalisatie—de omzetting van stellingen in natuurlijke taal en hun bijbehorende bewijzen naar complete, mechanisch verifieerbare formele stellingen en bewijzen—onderbelicht. Bestaande benaderingen richten zich vaak uitsluitend op de formalisatie van de stelling, waarbij ze vertrouwen op "sorry"-placeholders voor bewijzen, of behandelen stellinggeneratie en stellingbewijs als geïsoleerde taken.

De kernuitdaging ligt in de multidimensionale aard van hoogwaardige autoformalisatie. Een succesvolle formalisatie moet gelijktijdig voldoen aan:

1. Formele Validiteit (FV): Syntactische correctheid en mechanische verificatie door een stellingbewijzer (bijv. Lean4).
2. Logische Behoud (LP): Semantische uitlijning met de logische structuur van de oorspronkelijke stelling in natuurlijke taal.
3. Wiskundige Consistentie (MC): Accurate weergave van wiskundige objecten en operaties.
4. Formele Kwaliteit (FQ): Structurele helderheid, beknoptheid en herbruikbaarheid.

Huidige iteratieve verfijningsmethoden worstelen om deze dimensies gezamenlijk te optimaliseren, waarbij ze vaak één aspect (bijv. syntaxis) verbeteren ten koste van andere (bijv. semantische uitlijning). Bovendien vertrouwen bestaande methoden vaak op grondwaarheidsformalisaties of menselijke interventie voor selectie, wat hun toepasbaarheid in referentievrije settings beperkt.

2. Methodologie

De auteurs stellen een referentievrij, iteratief, monotoon optimalisatieproces voor dat werkt tijdens de testfase zonder toegang tot grondwaarheidsformalisaties of menselijke selectie. Het raamwerk integreert feedback van stellingbewijzers en door LLM's aangedreven rechters om een ensemble van gespecialiseerde LLM's te sturen.

2.1 Doelfunctie

De auteurs definiëren een gemaskerde samengestelde doelstelling $J_{OA}(x)$ om de vier dimensies in evenwicht te brengen. Formele Validiteit ($\pi_{FV}$) fungeert als een harde beperking (een masker), terwijl Logische Behoud ($\pi_{LP}$), Wiskundige Consistentie ($\pi_{MC}$) en Formele Kwaliteit ($\pi_{FQ}$) worden behandeld als zachte dimensies:
$$J_{OA}(x) = \frac{1}{3}\pi_{FV}(x) \left( \pi_{LP}(x) + \pi_{MC}(x) + \pi_{FQ}(x) \right)$$
Deze formulering zorgt ervoor dat ongeldige formalisaties (waarbij $\pi_{FV}=0$) niet worden geselecteerd, ongeacht hun zachte scores.

2.2 LLM-rechters en Onzekerheid

Aangezien zachte dimensies niet exact berekenbaar zijn, maakt het raamwerk gebruik van LLM-rechters om scores te schatten. Om de inherente ruis en bias van LLM's te hanteren, gaan de auteurs uit van:

• Asymptotische Stabiliteit: Oordelen stabiliseren na kalibratie.
• Meetbare Onzekerheid: Een eenzijdige Lower Confidence Bound (LCB) kan worden vastgesteld voor de ware scores.
  De doelstelling wordt geoptimaliseerd met een op LCB gebaseerde schatter, zodat selectiebeslissingen conservatief zijn en bestand tegen evaluatieruis.

2.3 Generatorrollen en Responsiviteit

Het raamwerk deconstrueert LLM-rollen in drie categorieën, geleid door een responsiviteitskaart die verwachte verbeteringen per dimensie modelleert:

1. Eenmalige Generatoren (OOG's): Genereren initiële formalisaties vanaf nul (bijv. gespecialiseerde wiskundemodellen zoals DeepSeek-Prover).
2. FV-Reparateurs (FVR's): Richt zich specifiek op en corrigeert formeel ongeldige kandidaten (bijv. modellen die in staat zijn tot iteratieve bewijsrevisie).
3. Recurrente Generatoren (REG's): Verfijnen de huidige beste kandidaat op basis van feedback van LLM-rechters over specifieke zachte dimensies (LP, MC of FQ).

2.4 Monotone Acceptatiebeleid

Het proces doorloopt iteraties van kandidaatgeneratie en selectie. Een Conservatief Acceptatiebeleid wordt toegepast: een nieuwe kandidaat wordt alleen geaccepteerd als zijn geschatte doelscore (gebaseerd op de LCB) strikt hoger is dan de huidige beste. Dit garandeert gecertificeerde monotoon verbetering, wat betekent dat de kwaliteit van de geselecteerde formalisatie nooit afneemt over de iteraties heen. Het proces is bewezen te convergeren en te termineren onder specifieke voorwaarden.

3. Belangrijkste Bijdragen

1. Formele Definitie en Raamwerk: Het artikel is de eerste die volledige-stelling autoformalisatie formeel definieert als een geünificeerde taak en een referentievrij, iteratief monotoon proces voorstelt om dit op te lossen.
2. Gemaskerde Samengestelde Doelstelling: Introductie van een doelfunctie die Formele Validiteit afdwingt als een harde beperking terwijl meerdere zachte dimensies (LP, MC, FQ) gelijktijdig worden geoptimaliseerd.
3. Rol-gespecialiseerd Ensemble: Decompositie van de autoformalisatietaken in OOG-, FVR- en REG-rollen, waarbij gebruik wordt gemaakt van een responsiviteitskaart om generators te selecteren die het meest effectief zijn voor specifieke kwaliteitsdimensies.
4. Theoretische Waarborgen: Levering van theoretische bewijzen voor gecertificeerde monotonie, convergentie en procesterminabiliteit, waardoor niet-afnemende vooruitgang wordt gegarandeerd, zelfs onder realistische rechterruis.
5. Empirische Validatie: Aantonen dat het raamwerk effectief de sterktes van gespecialiseerde en algemeen doelgerichte LLM's combineert om hoogwaardige resultaten te behalen op standaard benchmarks.

4. Experimentele Resultaten

De methode werd geëvalueerd op miniF2F-Test en ProofNet-Test met behulp van Lean4. Het raamwerk gebruikte een ensemble van modellen, waaronder DeepSeek-Prover-V2-7B, Goedel-Prover-V2-8B, Seed-Coder-8B, Qwen2.5-7B en GPT-4.1-mini (als rechters).

Belangrijkste Prestatiemetrics:

• miniF2F: Bereikte 100,00% Formele Validiteit en een totaalscore van 90,27%. Het percentage "perfecte" formalisaties (alle dimensies scoren 1) bereikte 49,18%.
• ProofNet: Bereikte 77,96% Formele Validiteit en een totaalscore van 52,45%, met 17,74% perfecte formalisaties.

Vergelijkende Bevindingen:

• Monotoon versus Baselines: Het monotoon proces presteerde aanzienlijk beter dan zowel Best-of-k (het bemonsteren van $k$ outputs) als Iteratieve Zelf-Verfijning (ISR) zonder acceptatiebeleid.
• Ensemble versus Eén Model: Hoewel één sterk model (GPT-5.4) verbetering liet zien, bereikte het ensemble van kleinere, gespecialiseerde modellen die aan specifieke rollen waren toegewezen superieure prestaties, met name in Formele Validiteit.
• Robuustheid: De monotone trend bleef behouden, zelfs wanneer geëvalueerd door verschillende families van LLM-rechters (bijv. Qwen versus GPT) en menselijke experts, wat aangeeft dat de verbeteringen geen artefacten zijn van rechterbias.

5. Betekenis en Claims

Het artikel beweert dat dit werk een praktische en theoretisch onderbouwde stap biedt naar betrouwbare autoformalisatie. Door te werken in een referentievrije manier, is de aanpak toepasbaar zelfs in domeinen die ontbreken aan uitgebreide formele bibliotheken, wat potentieel kan bijdragen aan de formalisatie van onderbelichte gebieden van wiskunde en wetenschap.

De auteurs benadrukken dat het raamwerk een geprincipeerde methodologie biedt voor door AI ondersteunde autoformalisatie die:

• De behoefte aan menselijk toezicht in grootschalige formele verificatiepijplijnen vermindert.
• Onzekerheid in oordelen expliciet kwantificeert en controleert via LCB-aannames.
• Aantoont dat het combineren van complementaire LLM's met feedback van formele verifiers formalisaties kan produceren met bewezen niet-afnemende kwaliteit.

Het werk concludeert dat, hoewel de rekenkosten hoger zijn dan inferentie in één doorgang, de afweging gerechtvaardigd is door de aanzienlijke winst in prestaties en stabiliteit, wat de weg effent voor toekomstig onderzoek in veilig, betrouwbaar door AI ondersteund formeel redeneren.