💻 computer science

Construction-Verification: A Benchmark for Applied Mathematics in Lean 4

Dieses Paper führt AMBER ein, einen neuen Lean-4-Benchmark für angewandte Mathematik, der die Konstruktion expliziter Lösungen vor der Verifizierung betont und aufzeigt, dass allgemeine Reasoning-Modelle spezialisierte Theorembeweiser übertreffen, da letztere dazu neigen, unter „taktischem Overfitting“ zu leiden, was das Befolgen komplexer Instruktionen behindert.

Ursprüngliche Autoren: Bowen Yang, Yi Yuan, Chenyi Li, Ziyu Wang, Liangqi Li, Bo Zhang, Zhe Li, Zaiwen Wen

Veröffentlicht 2026-02-03

📖 4 Min. Lesezeit☕ Kaffeepausen-Lektüre

CC BY 4.0

Ursprüngliche Autoren: Bowen Yang, Yi Yuan, Chenyi Li, Ziyu Wang, Liangqi Li, Bo Zhang, Zhe Li, Zaiwen Wen

Originalarbeit lizenziert unter CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Dies ist eine KI-generierte Erklärung des untenstehenden Papers. Sie wurde nicht von den Autoren verfasst oder gebilligt. Für technische Genauigkeit konsultieren Sie das Originalpaper. Vollständigen Haftungsausschluss lesen

Stellen Sie sich vor, Sie bringen einem Roboter bei, Mathematik zu betreiben. Lange Zeit waren die Tests, die wir diesem Roboter gaben, so etwas wie die Frage: „Existiert eine Lösung für dieses Rätsel?“ Der Roboter konnte mit „Ja“ antworten, indem er sagte: „Ich weiß, dass sie irgendwo da ist“, ohne jemals das Teil selbst gefunden oder Ihnen gezeigt zu haben, wie man es zusammenfügt.

Dieses neue Paper mit dem Titel „Construction–Verification“ argumentiert, dass für die angewandte Mathematik (die Art von Mathematik, die verwendet wird, um Brücken zu bauen, Lieferrouten zu optimieren oder Daten zu analysieren) ein bloßes „Es existiert“ nicht ausreicht. Man muss den Roboter dazu bringen, die Lösung zuerst tatsächlich zu konstruieren und dann zu beweisen, dass sie funktioniert.

Hier ist eine einfache Aufschlüsselung dessen, was die Forscher getan und herausgefunden haben:

1. Das Problem: Der „Zauberstab“ vs. der „Bauplan“

In traditionellen Mathematiktests könnte ein Roboter einen „Zauberstab“ (einen nicht-konstruktiven Beweis) benutzen, um ein Problem einfach wegzuschwingen und zu erklären: „Eine Lösung existiert!“ und dann weiterzumachen.

Der alte Weg: „Ich habe bewiesen, dass eine Brücke gebaut werden kann.“ (Aber Sie wissen nicht, wie man sie baut).
Der neue Weg (AMBER Benchmark): „Hier sind die Baupläne und die Materialien. Baue die Brücke und zeige mir danach, dass sie nicht einstürzt.“

Die Forscher haben einen neuen Test namens AMBER (Applied Mathematics BEnchmark for Reasoning) entwickelt. Er zwingt die KI, einem strikten Zwei-Schritte-Workflow zu folgen:

Konstruktion: Sie müssen den Code oder die Formel schreiben, die das Ergebnis tatsächlich berechnet.
Verifikation: Sie müssen beweisen, dass Ihr Ergebnis korrekt ist.

Sie haben die KI in vier schwierigen Bereichen getestet:

Konvexe Analyse: Den tiefsten Punkt in einem gekrümmten Tal finden.
Optimierung: Einen möglichst effizienten Plan erstellen.
Numerische Algebra: Zahlen in riesigen Gittern verarbeiten.
Hochdimensionale Wahrscheinlichkeit: Ergebnisse mit vielen Variablen vorhersagen.

2. Die Überraschung: Generalisten schlagen Spezialisten

Die Forscher erwarteten, dass Roboter, die speziell als „Mathematik-Beweiser“ trainiert wurden, diesen Test haushoch gewinnen würden. Sie irrten sich.

Die Spezialisten (Die Falle des „Tactical Overfitting“): Die Roboter, die ausschließlich auf mathematische Beweise trainiert wurden, blieben stecken. Sie waren so sehr darauf konditioniert, Dinge nur zu beweisen, dass sie vergaßen, wie man Dinge baut. Es ist wie ein Schachgroßmeister, der so gut darin ist, Spiele zu gewinnen, dass er vergisst, wie man das Brett aufstellt. Sie versuchten, zu „beweisen“, dass die Antwort existiert, ohne sie tatsächlich zu berechnen, was zum Scheitern führte.
Die Generalisten (Die „Schweizer Taschenmesser“): Die Roboter, die auf allgemeines Denken trainiert wurden (wie DeepSeek oder GPT), schnitten viel besser ab. Da sie daran gewöhnt sind, komplexe, mehrstufige Anweisungen in vielen verschiedenen Kontexten zu befolgen, waren sie besser darin, zu sagen: „Okay, zuerst muss ich diese Funktion definieren, dann muss ich beweisen, dass sie funktioniert.“ Sie verfielen nicht in die Gewohnheit des bloßen Beweisens.

3. Wie der Test tatsächlich aussieht

Das Paper beschreibt drei Arten von Herausforderungen, denen sich die KI stellen musste, die sich von Standard-Mathematiktests unterscheiden:

Evaluationsprobleme: Anstatt zu fragen: „Gibt es eine Zahl $x$ , die dies löst?“, fragt der Test: „Hier ist die Formel für $x$ . Schreibe den Code, um sie zu berechnen.“
Algorithmusdesign: Anstatt zu beweisen, dass eine Schleife funktioniert, muss die KI die Schleife selbst schreiben. Es ist, als würde man einen Koch nicht nur fragen, ob man einen Kuchen backen kann, sondern ihn bitten, das exakte Rezept und die Mischanweisungen zu schreiben.
Repräsentations-Transformation: Dies ist wie die Übersetzung eines unordentlichen, realen Problems (wie „Wie planen wir diese Busse?“) in ein sauberes, standardisiertes mathematisches Format (wie „Dies ist ein lineares Programmierproblem“), das ein Computer lösen kann. Die KI muss als Übersetzer fungieren, nicht nur als Löser.

4. Wo die Roboter scheiterten

Als die Forscher untersuchten, warum die Roboter scheiterten, fanden sie vier Hauptgründe:

Halluzinationen (47 %): Die Roboter erfanden mathematische Theoreme oder Bibliotheksnamen, die gar nicht existierten. Sie klangen zwar selbstbewusst, erfanden aber Fakten.
Formalisierungsfehler (33 %): Sie kannten die richtigen mathematischen Konzepte, konnten sie aber nicht korrekt in die strikte Computersprache (Lean 4) übersetzen.
Aufgeben (15 %): Sie begannen mit dem Code, ließen aber Teile unvollendet und schrieben stattdessen „sorry“ (einen Platzhalter), anstatt den schwierigen Teil zu Ende zu führen.
Tippfehler (5 %): Einfache Formatierungsfehler.

Das Fazit

Das Paper kommt zu dem Schluss, dass wir, um KI für angewandte Mathematik wirklich nützlich zu machen, sie nicht nur als „Beweis-Maschine“ trainieren dürfen. Wir brauchen Systeme, die zuerst Lösungen bauen und diese dann verifizieren können. Derzeit sind allgemeine KI-Modelle besser in dieser „Bau“-Aufgabe als spezialisierte Mathematikmodelle, weil die Spezialisten in ihrem Denken zu starr geworden sind.

Die Forscher schlagen vor, dass zukünftige KI eine Hybridform sein muss: klug genug, um komplexen Anweisungen zum Bauen von Dingen zu folgen, aber rigoros genug, um zu beweisen, dass diese korrekt sind.

Technisches Resümee: Konstruktion–Verifikation: Ein Benchmark für die Formalisierung angewandter Mathematik in Lean 4

1. Problemstellung

Aktuelle Benchmarks für das automatisierte Theorembeweisen, wie MiniF2F und ProofNet, konzentrieren sich vorwiegend auf die logische Verifikation deklarativer Propositionen (d. h. den Beweis der Existenz einer Lösung). Dieses Paradigma ist für die angewandte Mathematik unzureichend, in der das primäre Ziel oft die Ableitung konkreter Werte, ausführbarer Algorithmen oder struktureller Transformationen ist und nicht bloßer Existenzbeweise.

Bestehende Datensätze leiden unter zwei kritischen Einschränkungen in diesem Bereich:

Inhaltliche Lücke (Scope Gap): Ihnen fehlt die Abdeckung von Undergraduate-Niveau und höherer angewandter Mathematik, einschließlich konvexer Analysis, Optimierung, numerischer Algebra und hochdimensionaler Wahrscheinlichkeitstheorie.
Konstruktives Defizit: Sie versäumen es, einen „Konstruktions–Verifikations“-Workflow zu erzwingen. In der angewandten Mathematik muss ein Modell eine Lösung (z. B. einen Algorithmus oder einen spezifischen Wert) explizit synthetisieren, bevor es deren Korrektheit beweist. Aktuelle Benchmarks erlauben es Modellen, dies durch nicht-konstruktive Taktiken zu umgehen (z. B. den Beweis der Existenz über den extremen Wertsatz zu führen, ohne den spezifischen Optimum zu berechnen), was die Fähigkeit des Modells zur computationalen Argumentation falsch darstellt.

2. Methodik

Das Konstruktions–Verifikations-Framework

Die Autoren schlagen ein Formalisierungsparadigma in Lean 4 vor, das strukturell einen zweistufigen Workflow erzwingt: Konstruktion gefolgt von Verifikation. Dieses Framework verhindert, dass Agenten nicht-konstruktive Abkürzungen ausnutzen, indem es explizite Definitionen vor den Beweisen verlangt. Das Framework adressiert drei spezifische Kategorien angewandter mathematischer Aufgaben:

Evaluationsprobleme: Anstatt $\exists x, Q(x)$ zu beweisen, muss der Agent eine Funktion def x (V) := ... definieren, die die Lösung $x(V)$ bassierend auf Parametern $V$ berechnet, gefolgt von einem Theorem, das $Q(x(V), V)$ beweist. Die Funktionssignatur beschränkt die Eingaben strikt auf Rohparameter, um zu verhindern, dass das Modell die Ziel-Eigenschaft nutzt, um die Konstruktion zu „schummeln“.
Algorithmusdesign-Probleme: Der Agent muss eine rekursive Funktion definieren, die einen iterativen Prozess repräsentiert (z. B. Gradientenabstieg). Die Aufgabe erfordert das Ausfüllen der Übergangsregel (des Schleifenkörpers) für den $(n+1)$ -ten Schritt, gefolgt von einem Beweis von Eigenschaften wie Konvergenz oder Monotonie.
Repräsentationstransformation: Der Agent muss eine rohe Probleminstanz als Ziel-Kanonsische Form modellieren (z. B. die Transformation eines Graph-Cut-Problems in eine spektrale Clustering-Formulierung). Dies beinhaltet die Definition des neuen Bereichs, der Constraints und der Zielfunktion sowie den Beweis einer Relaxation oder einer Äquivalenzrelation zwischen dem Quell- und Zielproblem.
Theorembeweis: Eine Basis-Teilmenge traditioneller deduktiver Aufgaben ist enthalten, um die reine logische Argumentationsfähigkeit unabhängig von der konstruktiven Synthese zu messen.

Benchmark-Kuratierung (AMBER)

Die Autoren führen AMBER ein (Applied Mathematics BEnchmark for Reasoning), einen Datensatz, der vier Kernbereiche abdeckt:

Konvexe Analysis
Optimierung
Numerische Algebra
Hochdimensionale Wahrscheinlichkeitstheorie

Datenquellen & Schwierigkeitsgrad: Die Probleme stammen aus klassischen Lehrbüchern (z. B. Boyd & Vandenberghe, Vershynin) und sind nach Schwierigkeit kategorisiert (Easy: Standardübungen; Hard: PhD-Qualifikationsprüfungsniveau).
Formalisierung & Validierung: 50 Probleme pro Teilgebiet wurden von erfahrenen Lean-Anwendern formalisiert. Die Validierung erfolgte in einem zweistufigen Prozess: einer LLM-basierten semantischen Prüfung, gefolgt von einer rigorosen manuellen Kreuzvalidierung durch Mathlib-Mitwirkende, um die strikte Übereinstimmung mit den ursprünglichen mathematischen Aussagen zu gewährleisten.
Komplexitätsmetriken: Der Benchmark zeichnet sich durch eine hohe semantische Abhängigkeitsdichte aus. Durch eine Abhängigkeitsgraph-Analyse ( $k=3$ ) weist AMBER eine durchschnittliche Abhängigkeitsdichte von 164,21 auf, was signifikant höher ist als bei MiniF2F (29,72), ProofNet (33,95) und FATE (53,14), was auf eine tiefere Anforderung an das Abrufen und Argumentieren über komplexe mathematische Konzepte hindeutet.

3. Zentrale Beiträge

Paradigmenwechsel: Das Paper schlägt einen Wechsel von der Verifikation existentieller Propositionen hin zur Synthese konstruktiver Lösungen vor, wodurch formale Aufgaben mit der computationalen Intuition der angewandten Mathematik in Einklang gebracht werden.
AMBER-Benchmark: Ein umfassender Datensatz, der Kernbereiche der angewandten Mathematik mit variierenden Schwierigkeitsgraden abdeckt und komplexe Aufgaben wie Algorithmusdesign und Repräsentationstransformation umfasst, nicht nur Theorembeweise.
Formalisierungsmuster: Spezialisierte Lean 4-Templates für Evaluation, Algorithmusdesign und Repräsentationstransformation, die strikte syntaktische Barrieren gegen nicht-konstruktives Argumentieren setzen.
Empirische Analyse: Eine systematische Evaluierung, die einen fundamentalen Trade-off in aktuellen neuro-symbolischen Systemen aufzeigt: das Spannungsverhältnis zwischen lokaler taktischer Kompetenz (spezialisierte Prover) und hochgradiger algorithmischer Synthese (allgemeine Modelle).

4. Experimentelle Ergebnisse

Modellleistung

Die Autoren evaluierten eine diverse Menge an Modellen, darunter allgemeine Reasoning-Agenten (DeepSeek-V3.2-Thinking, GPT-5.1, Gemini-3.0 Pro) und spezialisierte Theorembeweiser (Goedel Prover-32B, Kimina Prover-72B).

Gesamtschwierigkeit: Die Leistung über alle Modelle hinweg ist bemerkenswert niedrig. Bei der „Hard“-Teilmenge liegen die Erfolgsraten für fast alle Modelle nahe Null.
Allgemein vs. Spezialisiert: Entgegen dem Trend bei reinen Mathematik-Benchmarks übertreffen allgemeine Reasoning-Modelle konsistent spezialisierte Theorembeweiser.
- Pass@16 (Full AMBER): Allgemeine Modelle erreichten 4,50 %–6,00 %, während spezialisierte Prover 4,00 % erreichten.
- Pass@16 (Hard Subset): Allgemeine Modelle erreichten 0 %–0 % (mit gewisser Variation in den Easy-Teilmengen), während spezialisierte Prover ebenfalls signifikant kämpften.
Ablationsstudie: Die Construction-Verification-Prompt-Strategie lieferte eine Erfolgsrate von 8 % auf eine 100-Problem-Teilmenge und übertraf damit die Standard-Code-Completion (6 %) und traditionelle Proof-only-Prompts (5 %). Proof-only-Prompts führten häufig dazu, dass Modelle nicht-konstruktive Abkürzungen (z. B. Classical.choice) verwendeten.

Fehleranalyse

Eine Analyse von 3.189 Fehlermeldungen des DeepSeek-R1 Modells ergab:

Halluzination (47,3 %): Der häufigste Fehlermodus, bei dem Modelle nicht existierende Theoreme oder Definitionen aufrufen (z. B. convexHull eq sInter).
Formalisierungskompetenz (32,7 %): Fehlanwendung gültiger Taktiken oder das Versagen beim Erfüllen von Nebenbedingungen.
Unvollständige Ausgaben (15,2 %): Unfähigkeit, vollständig ausführbaren Code bereitzustellen, oft mit sorry-Platzhaltern in komplexen induktiven Schritten.
Formatierung/Syntax (4,8 %): Basale Markdown- oder Syntaxfehler.

5. Bedeutung und Behauptungen

Das Paper behauptet, dass die aktuelle Landschaft der automatisierten Formalisierung einem Phänomen des „Taktik-Overfittings“ gegenübersteht. Spezialisierte Modelle, die intensiv auf Proof-Korpora feinjustiert wurden, scheinen ihre allgemeine Instruktionsfolgebefähigkeit zu verlieren. Sie behandeln jede strukturelle Herausforderung als reine Theorembeweis-Aufgabe und ignorieren dabei oft die mehrstufigen Anforderungen der angewandten Mathematik (z. B. die Definition einer Funktion vor deren Beweis).

Im Gegensatz dazu behalten allgemeine Modelle die notwendige Vielseitigkeit, um die Brücke zwischen informeller Intention und formaler Syntax zu schlagen, indem sie mathematische Objekte erfolgreich synthetisieren, bevor sie in die Verifikationsphase eintreten. Die Autoren schließen, dass die Weiterentwicklung der formalisierten angewandten Mathematik über die reine Beweissuche hinausgehen muss hin zu neuro-symbolischen Systemen, die hochgradiges algorithmisches Argumentieren mit rigoroser formaler Verifikation integrieren. Der AMBER-Benchmark dient als Fundament für zukünftige Forschung zur Erweiterung der Grenzen der formalisierten angewandten Mathematik, indem er einen Standard setzt, der konstruktive Synthese statt bloßer logischer Gültigkeit fordert.