🤖 AI

Formally Solving Answer-Construction Problems in Lean

Dieses Paper stellt ECP vor, ein neuro-symbolisches Framework in Lean, das werkzeuggestützte allgemeine LLMs zur Enumeration von Kandidatenantworten mit Prover-LLMs zur Generierung maschinell geprüfter Beweise kombiniert und damit effektiv die Lücke bei der formalen Lösung mathematischer Antwortkonstruktionsprobleme schließt.

Ursprüngliche Autoren: Jialiang Sun, Yuzhi Tang, Ao Li, Chris J. Maddison, Kuldeep S. Meel

Veröffentlicht 2026-06-02

📖 5 Min. Lesezeit🧠 Tiefgang

CC BY 4.0

Ursprüngliche Autoren: Jialiang Sun, Yuzhi Tang, Ao Li, Chris J. Maddison, Kuldeep S. Meel

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 nehmen an einem sehr schwierigen Mathematikwettbewerb teil. Es gibt zwei Arten von Aufgaben, denen Sie gegenüberstehen könnten:

Die „Beweise es“-Aufgabe: Der Richter gibt Ihnen eine Aussage wie „Der Himmel ist blau“ und fragt: „Können Sie beweisen, dass dies wahr ist?“ Sie müssen lediglich ein logisches Argument formulieren.
Die „Baue es“-Aufgabe: Der Richter fragt: „Finde die kleinste Zahl, die diese seltsamen Regeln erfüllt.“ Sie müssen zuerst die Zahl erfinden und dann beweisen, dass sie funktioniert.

Dieses Papier beschäftigt sich ausschließlich mit der zweiten Art: Antwort-Konstruktion (Answer-Construction). Es ist der Unterschied zwischen einem Anwalt, der einen bekannten Fall argumentiert, und einem Architekten, der erst ein Gebäude entwerfen muss, bevor er beweist, dass es nicht einstürzt.

Das Problem: Ein Werkzeug-Mismatch

Die Autoren stellten eine Lücke fest, wie Künstliche Intelligenz (KI) diese Aufgaben bewältigt.

Allgemeine KI (Das „Große Gehirn“): Denken Sie an einen brillanten, gesprächigen Professor. Er ist großartig im Brainstorming, beim Raten von Zahlen und beim groben Rechnen. Aber wenn man ihn bittet, einen formalen, maschinenperfekten Beweis zu schreiben, wird er oft faul, erfindet Fakten oder schreibt Code, der nicht kompiliert. Zudem ist er sehr teuer in der Beschäftigung.
Prover-KI (Der „Strenge Editor“): Denken Sie an einen winzigen, hyperfokussierten Roboter, der nur darauf trainiert ist, formale Beweise zu schreiben. Er ist günstig und hervorragend darin, Logik zu prüfen, aber er ist schrecklich darin, zu erraten, was die Antwort sein könnte. Wenn man ihn fragt: „Finde die Zahl“, starrt er vielleicht nur die Wand an oder rät eine wahllos gewählte Zahl, die nicht funktioniert.

Die Falle:
Wenn man den „Strengen Editor“ einfach bittet, eine „Baue es“-Aufgabe zu lösen, könnte er schummeln. Er könnte sagen: „Die Antwort ist die kleinste Zahl, die die Regeln erfüllt.“ Technisch gesehen ist das eine gültige Antwort in den Augen eines Computers, aber in einem echten Mathematikwettbewerb ist das ein zirkulärer Betrug. Man muss den Computer dazu zwingen, aufzuhören zu schummeln und tatsächlich die echte Zahl zu finden.

Die Lösung: ECP (Enumerate-Conjecture-Prove)

Die Autoren entwickelten ein neues System namens ECP (Enumerate-Conjecture-Prove). Es fungiert als ein Drei-Personen-Team, das bei diesen „Baue es“-Problemen in einer Sprache namens Lean (einem Computer-Beweisassistenten) zusammenarbeitet.

So arbeitet das Team unter Verwendung einer Detektiv-Analogie:

1. Der Detektiv (Die Allgemeine KI + Python-Tools)

Rolle: Dies ist der „Große Gehirn“-Professor, aber dieses Mal hat er einen Taschenrechner und einen Computer, um Code auszuführen.
Aktion: Anstatt nur zu raten, schreibt der Detektiv ein Python-Programm, um durch Brute-Force nach Hinweisen zu suchen. Er lässt Schleifen laufen, um tausende kleine Zahlen zu testen, um zu sehen, welche die Regeln erfüllen.
Die „Vermutung“ (Conjecture): Basierend auf den Daten stellt der Detektiv eine fundierte Vermutung an: „Ich wette, die Antwort ist 245.“ Er schreibt seine Argumentation in einfachem Englisch auf.

2. Der Gatekeeper (Der Admissibility-Checker)

Rolle: Dies ist der Türsteher im Club.
Aktion: Bevor die Vermutung des Detektivs weitergeleitet werden darf, prüft der Gatekeeper sie.
- Ist es eine echte Zahl? (Ja, 245 ist eine Zahl).
- Ist es Betrug? (Hat der Detektiv nur gesagt „die Antwort ist die Antwort“? Nein.)
- Werden verbotene Wörter verwendet? (Hat er komplexe mathematische Symbole verwendet, die im Wettbewerb nicht erlaubt sind? Nein.)
Wenn die Vermutung diese Prüfung nicht besteht, schickt der Gatekeeper sie an den Detektiv zurück, damit dieser es erneut versucht.

3. Der Richter (Die Prover-KI + Lean-Automatisierung)

Rolle: Dies ist der „Strenge Editor“-Roboter.
Aktion: Sobald der Gatekeeper die Vermutung (245) genehmigt hat, übernimmt der Richter. Der Richter ignoriert den Teil „wie wir es gefunden haben“ und konzentriert sich ausschließlich auf den Teil „warum es wahr ist“. Er nutzt formale Logik, um zweifelsfrei zu beweisen, dass 245 tatsächlich die korrekte Antwort ist.
Wenn der Beweis fehlschlägt, schickt der Richter den Detektiv zurück, damit dieser eine andere Zahl ausprobiert.

Die Ergebnisse: Hat es funktioniert?

Die Autoren testeten dieses Team auf zwei berühmten Mathematik-Datensätzen: PutnamBench (Mathematik auf Universitätsniveau) und MathArena (Mathematik-Wettbewerbe auf Highschool-Niveau wie AIME).

Der alte Weg: Wenn man den „Strengen Editor“ einfach gebeten hätte, diese Probleme zu lösen, ist er meist gescheitert oder hat durch zirkuläre Antworten geschummelt. Wenn man das „Große Gehirn“ alles machen lassen hätte, wäre es beim formalen Beweis steckengeblieben.
Der ECP-Weg: Durch die Aufteilung der Arbeit löste das System 17 von 346 schwierigen Universitätsproblemen und 18 von 75 Highschool-Problemen.
Warum es wichtig ist: Es geht nicht nur darum, die richtige Zahl zu bekommen; es geht darum, einen maschinenverifizierten Beweis zu erhalten, dass die Zahl korrekt ist und dass die Antwort kein Betrug war.

Zusammenfassung

Betrachten Sie ECP als eine Fließbandfertigung für mathematische Probleme:

Arbeiter A (Allgemeine KI) nutzt Werkzeuge, um nach der Antwort zu graben.
Inspektor B (Gatekeeper) stellt sicher, dass es sich um eine echte, nicht-betrügerische Zahl handelt.
Arbeiter C (Prover-KI) baut die unzerbrechliche Brücke der Logik, um zu beweisen, dass diese Zahl richtig ist.

Dieser Ansatz überbrückt die Lücke zwischen dem „Raten der Antwort“ und dem „Beweisen der Antwort“ und ermöglicht es der KI, Mathematikprobleme zu lösen, die sowohl Kreativität als auch rigorose Logik erfordern.

Technisches Resümee: Formale Lösung von Antwortkonstruktionsproblemen in Lean

Problemdefinition
Mathematische Wettbewerbsaufgaben lassen sich im Allgemeinen in zwei Kategorien unterteilen: Theorembeweis (Verifizierung einer gegebenen Aussage) und Antwortkonstruktion (Konstruktion eines spezifischen Objekts, das eine bestimmte Eigenschaft erfüllt). Während jüngste Fortschritte bei Large Language Models (LLMs) das formale Theorembeweisen signifikant verbessert haben, bleibt die formale Antwortkonstruktion untererforscht. Es besteht eine kritische Lücke zwischen informellen Reasoning-Systemen, die stark im Konjektieren, aber schwach in der formalen Verifizierung sind, und formalen Beweis-LLMs, die für Beweise optimiert sind, aber Schwierigkeiten haben, die notwendigen Zeugen (Witnesses) zu entdecken, um Existenzquantoren zu eliminieren.

Eine spezifische Herausforderung bei der Formalisierung der Antwortkonstruktion ist die Admissibilität (Zulässigkeit). Standardmäßige Lean-Proof-Checker verifizieren zwar, dass ein Beweisterm den korrekten Typ besitzt, erzwingen jedoch nicht inhärent, dass der konstruierte Zeuge eine kanonische, geschlossene Antwort ist. Beispielsweise könnte ein Beweis eine existenzielle Aussage $\exists x, P(x)$ dadurch erfüllen, dass er einen nicht-kanonischen Term wie sInf PropertySet (das Infimum der definierten Menge) zurückgibt, anstatt einer expliziten natürlichen Zahl (z. B. 245). Solche „zirkulären“ oder nicht-geschlossenen Zeugen sind innerhalb der Logik mathematisch gültig, aber als Wettbewerbsantwort unzulässig.

Methodik: Enumerate-Conjecture-Prove (ECP)
Um diese Herausforderungen anzugehen, führen die Autoren Enumerate-Conjecture-Prove (ECP) ein, ein neuro-symbolisches Framework, das für die End-to-End-Antwortkonstruktion mit formalen Beweisen in Lean 4 konzipiert ist. ECP trennt den Prozess in distinkte Phasen, während es gleichzeitig eine formale Verifizierungsschleife beibehält:

Problemformalisierung & Admissibilitätsprüfung:
- Probleme werden als funktionale Syntheseaufgaben formalisiert: Das Finden einer Funktion $\Psi$ , sodass $\forall X, P(X) \to Q(X, \Psi(X))$ .
- Ein Admissibilitäts-Checker wird implementiert, um sicherzustellen, dass die synthetisierte Antwort nur ein vordefiniertes „admissibles Vokabular“ (z. B. spezifische Konstanten, arithmetische Operatoren und Standard-Konstruktoren) verwendet. Er extrahiert strukturell semantische Konstanten aus dem Lean-Term und filtert administrative Konstanten (wie Typeclass-Instanzen oder compiler-generierte Artefakte) sowie nicht-kanonische Definitionen (wie sInf) heraus.
Enumerate-Phase (Werkzeuggestützte Exploration):
- Ein Allzweck-LLM (z. B. GPT-5.4) wird mit Python-Tool-Ausführungskapazitäten ausgestattet.
- Das LLM schreibt und führt Python-Code aus, um eine beschränkte Enumeration über kleine Domänen durchzuführen, um Tupel zu finden, die die Problembeschränkungen erfüllen.
- Diese Ausführungstraces dienen als empirische Evidenz zur Identifizierung von Mustern, Invarianten und funktionalen Formen.
Conjecture-Phase (Antwortsynthese):
- Unter Verwendung der Evidenz aus der Enumerate-Phase synthetisiert dasselbe allgemeine LLM eine Kandidaten-Antwortfunktion $\Psi'$ .
- Der Kandidat durchläuft zwei Filter, bevor er fortfährt:
  - Syntaktische Verifizierung: Der Term muss in Lean mit dem korrekten Typ kompilieren.
  - Admissibilitäts-Verifizierung: Der Term darf nur Konstanten aus dem erlaubten Vokabular verwenden.
- Falls ein Kandidat fehlschlägt, iteriert das System mit der Fehlermeldung im Prompt fort.
Prove-Phase (Formale Verifizierung):
- Sobald ein gültiger Kandidat $\Psi'$ konstruiert wurde, versucht das System, das instanziierte Theorem $Stmt(T)|_{\Psi=\Psi'}$ zu beweisen.
- Refutationsschleife: Bevor ein Beweis versucht wird, versucht das System, den Kandidaten durch den Beweis der Negation zu widerlegen. Wenn die Widerlegung erfolgreich ist, wird der Kandidat verworfen und das System kehrt zur Conjecture-Phase zurück.
- Beweisgenerierung: Wenn die Widerlegung fehlschlägt, versucht das System, die positive Aussage mittels einer Kombination aus Leans eingebauter Automatisierung (Taktiken wie simp, aesop, ring, norm_num) und einem spezialisierten Prover-LLM (z. B. Goedel-Prover-V2) zu beweisen. Falls die Automatisierung fehlschlägt, wird das Prover-LLM mit einer Repair-Schleife aufgerufen, um den Beweis zu generieren oder zu korrigieren.

Wesentliche Beiträge

Framework für Antwortkonstruktion: ECP ist das erste Framework, das die Antwortkonstruktion explizit von der Beweiserzeugung trennt und gleichzeitig Admissibilitätsbeschränkungen innerhalb einer formalen Verifizierungsschleife erzwingt.
Admissibilitätserzwingung: Die Arbeit führt eine strukturelle Methode ein, um nicht-kanonische Zeugen (z. B. zirkuläre Definitionen) zu filtern, die Standard-Lean-Checker ansonsten akzeptieren würden, wodurch sichergestellt wird, dass die Ausgabe den Wettbewerbsanforderungen entspricht.
Neuro-symbolische Integration: Das Framework kombiniert effektiv das explorative Reasoning allgemeiner LLMs mit Python-Tools und die rigorose Beweiskapazität spezialisierter Prover-LLMs.
Benchmarks und Autoformalisierung: Die Autoren haben 75 Probleme aus den 2026 MathArena Final Answer Comps (AIME, HMMT, APEX) und 346 Antwortkonstruktionsprobleme aus PutnamBench autoformalisiert und damit einen neuen Evaluierungsstandard für diesen Problemtyp geschaffen.

Experimentelle Ergebnisse
Das System wurde auf MathArena 2026 (75 Probleme) und PutnamBench (346 Probleme) gegen Baselines evaluiert, darunter direkte Beweisgenerierungs-LLMs (GPT-5.4, Goedel-Prover-V2).

End-to-End-Performance: ECP übertraf die direkten Beweisgenerierungs-Baselines.
- MathArena: ECP löste 18/75 Probleme (Pass@32), verglichen mit 13/75 für die beste LLM-only Baseline (GPT-5.4).
- PutnamBench: ECP löste 17/346 Probleme (Pass@32), verglichen mit 8/346 für GPT-5.4 und 7/346 für Goedel-Prover-V2-32B.
Antwortgenauigkeit (nur Antwort): Werkzeuggestützte Antwortkonstruktion verbesserte die Genauigkeit der korrekten Kandidatengenerierung der allgemeinen LLMs signifikant. Für GPT-5.4 steigerte die Tool-Nutzung die korrekte Antwortkonstruktion auf PutnamBench von 290/346 auf 303/346.
Auswirkung der Admissibilität: Die Analyse ergab, dass viele von Baselines generierte Beweise zwar Lean-kompilierbar waren, aber unzulässige Antworten (z. B. zirkuläre Zeugen) enthielten. Die explizite Admissibilitätsprüfung von ECP war entscheidend, um diese herauszufiltern.
Ablationsstudien:
- Das Entfernen des Prover-LLM-Korrektur-Schritts reduzierte die Performance auf MathArena (18 $\to$ 16) und PutnamBench (17 $\to$ 16).
- Das Entfernen der Lean-Automatisierung hatte einen schweren Einfluss auf MathArena (18 $\to$ 11), aber weniger auf PutnamBench in diesem spezifischen Durchlauf, was darauf hindeutet, dass MathArena-Probleme stärker auf Automatisierungstaktiken angewiesen sind, während PutnamBench eher auf die Prover-Kapazität setzt.
- Die Verwendung eines kleineren Provers (8B) behielt die MathArena-Performance bei, senkte aber die PutnamBench-Ergebnisse signifikant (17 $\to$ 7), was zeigt, dass Putnam-Probleme stärker durch die Beweissuche limitiert sind.

Bedeutung und Behauptungen
Die Arbeit behauptet, dass ECP erfolgreich die Lücke zwischen informeller Antwortgenerierung und formalem Theorembeweis schließt. Durch die explizite Handhabung der „Antwortkonstruktionsphase“ und die Erzwingung der Admissibilität löst ECP Instanzen, die für direkte Beweisgenerierungs-Ansätze derzeit unlösbar sind. Die Autoren betonen, dass ihr Ansatz besonders effektiv für Probleme ist, die die Konstruktion eines spezifischen Zeugen (Existenzquantifizierung) erfordern, anstatt nur die Verifizierung einer festen Schlussfolgerung.

Die Arbeit hebt hervor, dass aktuelle formale Benchmarks oft die Schwierigkeit der Antwortkonstruktion aussparen und stattdessen auf „With-Answer“-Versionen von Problemen fokussieren. ECP demonstriert, dass die Kombination von allgemeinen LLMs mit Tool-Execution zur Enumeration, gefolgt von spezialisierten Prover-LLMs zur Verifizierung, ein gangbarer Weg zur Lösung komplexer, offener mathematischer Probleme in formalen Systemen ist. Die Autoren weisen auf Limitationen hinsichtlich der heuristischen Natur der Labeling-Verfahren für das admissible Vokabular und das Potenzial für kombinatorische Explosionen in der Enumerationsphase bei hochkomplexen Kombinatorik-Problemen hin.