Technische Samenvatting: Constructie–Verificatie: Een Benchmark voor het Formaliseren van Toegepaste Wiskunde in Lean 4

1. Probleemstelling

Huidige benchmarks voor geautomatiseerd bewijsgenereren, zoals MiniF2F en ProofNet, richten zich voornamelijk op de logische verificatie van declaratieve proposities (d.w.z. het bewijzen van het bestaan van een oplossing). Dit paradigma is onvoldoend voor toegepaste wiskunde, waarbij het primaire doel vaak de afleiding van concrete waarden, uitvoerbare algoritmen of structurele transformaties is, in plaats van louter existentiebewijzen.

Bestaande datasets lijden onder twee kritieke beperkingen in dit domein:

1. Scope-kloof: Ze missen dekking van de bacheloropleiding en hoger niveau in de toegepaste wiskunde, inclusief convexe analyse, optimalisatie, numerieke algebra en hoogdimensionale waarschijnlijkheid.
2. Constructief Tekort: Ze slagen er niet in een "constructie–verificatie"-workflow af te dwingen. In de toegepaste wiskunde moet een model expliciet een oplossing synthetiseren (bijv. een algoritme of een specifieke waarde) voordat de correctheid ervan bewezen kan worden. Huidige benchmarks laten modellen toe dit te omzeilen door niet-constructieve tactieken te gebruiken (bijv. het bestaan bewijzen via de extremalewaardestelling zonder de specifieke optimum te berekenen), waardoor het vermogen van het model tot computationeel redeneren verkeerd wordt weergegeven.

2. Methodologie

Het Constructie–Verificatie Framework

De auteurs stellen een formaliseringsparadigma voor in Lean 4 dat structureel een tweestaps-workflow afdwingt: Constructie gevolgd door Verificatie. Dit framework voorkomt dat agenten gebruikmaken van niet-constructieve shortcuts door expliciete definities te vereisen vóór de bewijzen. Het framework adresseert drie specifieke categorieën van taken in de toegepaste wiskunde:

• Evaluatieproblemen: In plaats van te bewijzen $\exists x, Q(x)$, moet de agent een functie def x (V) := ... definiëren die de oplossing $x(V)$ berekent op basis van parameters $V$, gevolgd door een stelling die $Q(x(V), V)$ bewijst. De functiesignatuur beperkt de inputs strikt tot ruwe parameters, wat voorkomt dat het model de doeleigenschap gebruikt om de constructie te "valsspelen".
• Algoritmeontwerpproblemen: De agent moet een recursieve functie definiëren die een iteratief proces representeert (bijv. Gradient Descent). De taak vereist het invullen van de transitieregel (de loop body) voor de $(n+1)$-de stap, gevolgd door een bewijs van eigenschappen zoals convergentie of monotoniciteit.
• Representatie Transformatie: De agent moet een rauwe probleeminstantie modelleren als een doel-canonieke vorm (bijv. het transformeren van een graph cut-probleem naar een spectrale clusteringformulering). Dit omvat het definiëren van het nieuwe domein, de restricties en de objectieffunctie, en het bewijzen van een relaxatie of equivalentierelatie tussen het bron- en doelprobleem.
• Stellingbewijzen: Een baseline subset van traditionele deductieve taken is opgenomen om het pure logische redeneervermogen te meten, los van constructieve synthese.

Benchmark Curatie (AMBER)

De auteurs introduceren AMBER (Applied Mathematics BEnchmark for Reasoning), een dataset die vier kerngebieden beslaat:

1. Convexe Analyse
2. Optimalisatie
3. Numerieke Algebra
4. Hoogdimensionale Waarschijnlijkheid

Databronnen & Moeilijkheidsgraad: Problemen zijn afkomstig van klassieke tekstboeken (bijv. Boyd & Vandenberghe, Vershynin) en zijn gecategoriseerd naar moeilijkheid (Easy: standaard oefeningen; Hard: PhD-kwalificeringsexamen niveau).
Formalisering & Validatie: 50 problemen per subveld werden geformaliseerd door ervaren Lean-gebruikers. Validatie omvatte een tweestaps-proces bestaande uit een LLM-gebaseerde semantische controle gevolgd door een rigoureuze handmatige cross-validatie door Mathlib-bijdragers om strikte afstemming met de oorspronkelijke wiskundige beweringen te waarborgen.
Complexiteitsmetrieken: De benchmark wordt gekenmerkt door een hoge semantische afhankelijkheidsdichtheid. Gebruikmakend van een afhankelijkheidsgraafanalyse ($k=3$), vertoont AMBER een gemiddelde afhankelijkheidsdichtheid van 164,21, wat aanzienlijk hoger is dan MiniF2F (29,72), ProofNet (33,95) en FATE (53,14), wat wijst op een diepere vereiste voor het ophalen en redeneren over complexe wiskundige concepten.

3. Belangrijkste Bijdragen

1. Paradigmaverschuiving: Het artikel stelt een verschuiving voor van het verifiëren van existentiële proposities naar het synthetiseren van constructieve oplossingen, waardoor formele taken worden afgestemd op de computationele intuïtie van toegepaste wiskunde.
2. AMBER Benchmark: Een uitgebreide dataset die kerngebieden van de toegepaste wiskunde beslaat met variërende moeilijkheidsgraden, voorzien van complexe taken zoals algoritmeontwerp en representatietransformatie, en niet enkel stellingbewijzen.
3. Formaliseringspatronen: Gespecialiseerde Lean 4-templates voor evaluatie, algoritmeontwerp en representatietransformatie die strikte syntactische barrières opwerpen tegen niet-constructief redeneren.
4. Empirische Analyse: Een systematische evaluatie die een fundamentele trade-off onthult in huidige neuro-symbolische systemen: de spanning tussen lokale tactische bekwaamheid (gespecialiseerde provers) en hoogwaardige algoritmische synthese (algemene modellen).

4. Experimentele Resultaten

Modelprestaties

De auteurs evalueerden een diverse set modellen, waaronder algemene redeneeragenten (DeepSeek-V3.2-Thinking, GPT-5.1, Gemini-3.0 Pro) en gespecialiseerde stellingbewijzers (Goedel Prover-32B, Kimina Prover-72B).

• Algemene Moeilijkheidsgraad: De prestaties over alle modellen heen zijn opmerkelijk laag. Op de "Hard" subset liggen de succespercentages voor bijna alle modellen nabij nul.
• Algemeen vs. Gespecialiseerd: In tegenstelling tot de trend bij pure wiskunde-benchmarks, presteren algemene redeneermodellen consistent beter dan gespecialiseerde stellingbewijzers.
  • Pass@16 (Volledige AMBER): Algemene modellen behaalden 4,50%–6,00%, terwijl gespecialiseerde provers 4,00% behaalden.
  • Pass@16 (Hard Subset): Algemene modellen behaalden 0%–0% (met enige variatie in de Easy subsets), terwijl gespecialiseerde provers ook aanzienlijk moeite hadden.
• Ablatiestudie: De constructie-verificatie prompt-strategie leverde een succespercentage van 8% op een subset van 100 problemen, wat beter is dan standaard code-aanvulling (6%) en traditionele proof-only prompts (5%). Proof-only prompts leidden modellen vaak naar niet-constructieve shortcuts (bijv. Classical.choice).

Foutanalyse

Een analyse van 3.189 foutmeldingen van het DeepSeek-R1 model onthulde:

1. Hallucinatie (47,3%): De meest voorkomende foutmodus, waarbij modellen niet-bestaande stellingen of definities aanroepen (bijv. convexHull eq sInter).
2. Formaliseringsbekwaamheid (32,7%): Verkeerde toepassing van geldige tactieken of het niet kunnen voldoen aan zijvoorwaarden.
3. Incomplete Outputs (15,2%): Het niet volledig leveren van uitvoerbare code, vaak met sorry placeholders in complexe inductieve stappen.
4. Formattering/Syntaxis (4,8%): Basale markdown- of syntaxisfouten.

5. Betekenis en Claims

Het artikel claimt dat het huidige landschap van geautomatiseerde formalisering te maken heeft met een "tactische overfitting"-fenomeen. Gespecialiseerde modellen, die uitgebreid zijn gefinetuned op bewijs-corpora, lijken hun algemene instructie-volgende vermogens te verliezen. Ze behandelen elke structurele uitdaging als een pure stellingbewijstaak, waarbij ze vaak de meerstapsvereisten van toegepaste wiskunde (bijv. het definiëren van een functie voordat deze bewezen wordt) negeren.

In contrast hiermee behouden algemene modellen de veelzijdigheid die nodig is om de brug te slaan tussen informele intentie en formele syntaxis, waarbij ze succesvol wiskundige objecten synthetiseren voordat ze de verificatiefase ingaan. De auteurs concluderen dat het bevorderen van geformaliseerde toegepaste wiskunde vereist dat men verder kijkt dan pure bewijszoektochten naar neuro-symbolische systemen die hoogwaardig algoritmisch redeneren integreren met rigoureuze formele verificatie. De AMBER-benchmark dient als fundament voor toekomstig onderzoek naar de uitbreiding van de grenzen van geformaliseerde toegepaste wiskunde door een standaard te bieden die constructieve synthese eist in plaats van louter logische geldigheid.