🤖 AI

From LLM-Generated Conjectures to Lean Formalizations: Automated Polynomial Inequality Proving via Sum-of-Squares Certificates

Dieser Beitrag stellt NSPI vor, ein neuro-symbolisches Framework, das große Sprachmodelle nutzt, um angenäherte Sum-of-Squares-Vermutungen vorzuschlagen, und symbolische Berechnung einsetzt, um diese zu exakten, maschinell verifizierten Lean-Beweisen zu verfeinern, wodurch eine skalierbare automatisierte Beweisführung für Polynomungleichungen mit bis zu 10 Variablen erreicht wird.

Ursprüngliche Autoren: Ruobing Zuo, Hanrui Zhao, Gaolei He, Zhengfeng Yang, Jianlin Wang

Veröffentlicht 2026-05-18

📖 4 Min. Lesezeit☕ Kaffeepausen-Lektüre

CC BY 4.0

Ursprüngliche Autoren: Ruobing Zuo, Hanrui Zhao, Gaolei He, Zhengfeng Yang, Jianlin Wang

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 versuchen zu beweisen, dass ein komplexer, mehrschichtiger Kuchen immer „genügend süß" (mathematisch: nicht-negativ) ist, egal wie Sie ihn schneiden oder die Zutaten ändern. In der Welt der Mathematik nennt man dies den Beweis einer Polynomungleichung.

Lange Zeit hatten Mathematiker zwei Hauptmethoden, dies zu tun, doch beide hatten gravierende Mängel:

Die „Reine Logik"-Methode (Symbolisch): Dies ist vergleichbar damit, das Kuchenproblem zu lösen, indem man jede einzelne chemische Reaktion der Zutaten auf eine Tafel schreibt. Es ist absolut präzise, doch wenn der Kuchen zu viele Zutaten (Variablen) hat, füllt sich die Tafel augenblicklich, und die Methode bricht zusammen. Sie ist für große Probleme zu langsam und zu unübersichtlich.
Die „KI-Raten"-Methode (LLMs): Dies ist vergleichbar damit, einen sehr klugen, kreativen Koch zu bitten, das Rezept zu erraten. Der Koch ist schnell und bei kleinen Kuchen gut, doch wenn der Kuchen riesig und kompliziert wird, beginnt der Koch, Zutaten zu halluzinieren, die es nicht gibt, oder mathematische Fehler zu machen. Er kann nicht beweisen, dass seine Antwort zu 100 % wahr ist.

Diese Arbeit stellt ein neues Team vor, das NSPI (Neuro-Symbolic Polynomial Inequality proving) heißt. Betrachten Sie NSPI als eine perfekte Partnerschaft zwischen einem kreativen Koch und einem strengen Qualitätsinspektor.

So funktioniert ihre „Fließband"-Produktion, Schritt für Schritt:

Schritt 1: Der kreative Koch (Das LLM)

Zunächst bittet das Team ein Large Language Model (den „Koch"), sich ein schwieriges mathematisches Problem anzusehen. Der Koch versucht nicht sofort, die harte Mathematik zu lösen. Stattdessen nutzt er seine Kreativität, um eine Struktur zu raten.

Die Analogie: Stellen Sie sich vor, der Koch sagt: „Ich wette, dieser Kuchen besteht aus drei spezifischen Schichten von Zuckerwürfeln, die übereinander gestapelt sind."
In mathematischen Begriffen errät das LLM eine Sum-of-Squares (SOS)-Zerlegung. Es schlägt vor: „Dieser komplizierte Ausdruck ist wahrscheinlich einfach die Summe einiger weniger einfacher Dinge, die quadriert wurden."
Kritischer Punkt: Die Vermutung des Kochs ist meist eine Approximation. Sie ist nah dran, könnte aber winzige Dezimalfehler haben (wie die Angabe, ein Zuckerwürfel wiege 1,0000001 Gramm statt genau 1).

Schritt 2: Der Qualitätsinspektor (Symbolische Korrektur)

Die Vermutung des Kochs wird an den „Qualitätsinspektor" weitergeleitet, ein leistungsfähiges Computeralgebrasystem.

Die Analogie: Der Inspektor nimmt die grobe Skizze des Kochs und nutzt ein Mikroskop, um die winzigen Fehler zu beheben. Er verwendet eine Technik namens Newton-Verfahren (eine mathematische Methode, um auf die exakte Antwort zu zoomen) und Rational Recovery (das Umwandeln von unordentlichen Dezimalzahlen in saubere, exakte Brüche).
Wenn der Koch geraten hat, die Schichten seien „ungefähr" 1,5, 2,3 und 0,7, berechnet der Inspektor die exakten Zahlen: 3/2, 23/10 und 7/10.
Nun wurde die Vermutung in ein perfektes, exaktes mathematisches Zertifikat verwandelt.

Schritt 3: Der Gerichtshof-Richter (Lean-Verifikation)

Schließlich bringt das Team dieses exakte Zertifikat zu einem „Richter" namens Lean.

Die Analogie: Lean ist ein strenger, unblinzelnder Richter, der jeden einzelnen Schritt der Arbeit des Inspektors überprüft. Ihn interessieren keine „Gefühle" oder „Vermutungen". Er akzeptiert nur Beweise, die logisch wasserdicht sind.
Da der Inspektor ein exaktes Zertifikat geliefert hat, kann der Richter leicht verifizieren: „Ja, wenn Sie diese exakten Zahlen quadrieren und addieren, erhalten Sie den ursprünglichen Kuchen. Und da Quadrate immer positiv sind, ist der Kuchen immer süß."
Der Richter stellt dann einen maschinengeprüften Beweis aus, der zu 100 % garantiert korrekt ist.

Warum ist das eine große Sache?

Die Arbeit testete dieses Team an 522 sehr schwierigen mathematischen Problemen, einige davon mit bis zu 10 verschiedenen Variablen (Zutaten).

Die alten Logikmethoden gaben auf, wenn die Probleme zu groß wurden (zu viele Zutaten).
Die alten KI-Methoden gerieten bei den großen Problemen in Verwirrung und machten Fehler.
Das NSPI-Team hatte Erfolg, wo andere scheiterten. Sie konnten Probleme mit 10 Variablen lösen, die keine andere Methode überhaupt angehen konnte.

Das Fazit

Die Arbeit behauptet, dass sie durch die Kombination eines KI-gestützten Ratens der Form der Lösung, gefolgt von der Nutzung mathematischer Werkzeuge zur Korrektur der Details und eines Computers zur Verifizierung der Wahrheit, ein System gebaut haben, das komplexe Ungleichungsprobleme schneller und zuverlässiger lösen kann als je zuvor. Sie haben nicht nur geraten; sie haben eine Brücke von einer „guten Vermutung" zu einer „bewiesenen Tatsache" gebaut.

Was sie NICHT behauptet haben:

Sie haben nicht gesagt, dass dies Krankheiten heilen oder den Aktienmarkt vorhersagen wird.
Sie haben nicht behauptet, dass dies für jeden Typ mathematisches Problem funktioniert, sondern nur für den Beweis, dass bestimmte Polynomausdrücke immer positiv sind.
Sie haben nicht behauptet, dass dies menschliche Mathematiker vollständig ersetzt, sondern vielmehr einen sehr spezifischen, schwierigen Typ von Schlussfolgerungen automatisiert.

Technische Zusammenfassung: Von LLM-generierten Vermutungen zu Lean-Formalisierungen

Problemstellung

Die automatisierte Beweisführung für Polynomungleichungen ist eine fundamentale Herausforderung im mathematischen Schlussfolgern, insbesondere für hochdimensionale und multivariate Fälle. Bestehende Ansätze sehen sich erheblichen Skalierungsbeschränkungen gegenüber:

Rein symbolische Methoden: Obwohl sie starke Garantien bieten, leiden Methoden, die auf Sum-of-Squares (SOS)-Zerlegung und Semidefiniten Programmierung (SDP) basieren, unter kombinatorischer Explosion und einem raschen Wachstum der Zwischenausdrücke, sobald die Anzahl der Variablen oder der Grad steigt. Sie scheitern häufig daran, strukturierte, für Menschen lesbare Beweise zu erzeugen.
Rein LLM-basierte Methoden: Große Sprachmodelle (LLMs), die mit Beweisassistenten (z. B. Lean, Isabelle) integriert sind, haben Potenzial gezeigt, sind jedoch durch den Mangel an hochwertigen formalisierten Trainingsdaten begrenzt. Sie haben Schwierigkeiten mit komplexen algebraischen Ungleichungen, insbesondere solchen mit mehr als 5 Variablen, und verfügen oft nicht über die Fähigkeit, rigorose, maschinenprüfbare Zertifikate zu generieren.

Die Kernherausforderung besteht darin, die Lücke zwischen heuristischer Entdeckung und rigoroser formaler Verifikation zu schließen, um die automatisierte Beweisführung für unbeschränkte Polynomungleichungen in hochdimensionalen Settings (bis zu 10 Variablen) mit maschinengeprüfter Korrektheit zu ermöglichen.

Methodik: NSPI-Rahmenwerk

Die Autoren schlagen NSPI (Neuro-Symbolic SOS-based Polynomial Inequality Proving) vor, ein Rahmenwerk, das die komplementären Stärken von LLMs und symbolischer Berechnung in eine End-to-End-Pipeline integriert. Der Prozess besteht aus drei Hauptphasen:

1. Neuronale Vermutung (LLM-gesteuerte SOS-Generierung)

Anstatt LLMs lediglich zur Suchführung zu verwenden, erhebt NSPI sie zu primären Vermutungsgeneratoren.

Datenerstellung: Die Autoren erstellen einen groß angelegten Datensatz aus nicht-negativen Polynom–SOS-Paaren mittels zweier neuartiger Strategien:
- Rechengetrieben: Erzeugung von Gram-Matrizen durch spektrales Verschieben oder LMI-Optimierung, um positive Semidefinitheit (PSD) mit kontrollierten Koeffizienten sicherzustellen.
- Strukturgetrieben: Ausnutzung algebraischer Strukturen wie diagonal dominanter (dd) und skaliert diagonal dominanter (sdd) Matrizen, die PSD-Eigenschaften per Design garantieren.
Training: Ein zweistufiges Trainingsschema wird angewendet:
- Kalter Start: Supervised Fine-Tuning (SFT) auf über einer Million synthetischer Polynom-SOS-Paare, um grundlegendes strukturelles Schlussfolgern zu etablieren.
- Progressives Bestärkungslernen: Curriculum-basierte Group Relative Policy Optimization (GRPO) wird auf herausfordernde Instanzen angewendet (Erhöhung der Variablenanzahl von 3–5 auf 9–10). Die Belohnungsfunktion kombiniert Genauigkeit (numerische Treue), Formatkonformität und algebraische Strukturstrafen, um sicherzustellen, dass das LLM plausible SOS-Strukturen generiert.
Ausgabe: Das LLM schlägt eine approximative SOS-Zerlegung (eine Summe von quadrierten Termen) für ein gegebenes Polynom vor.

2. Symbolische Korrektur (Exakte rationale Wiederherstellung)

Um die approximative Vermutung des LLM in einen rigorosen Beweis zu verwandeln, verfeinert ein symbolischer Korrekturmodul die Ausgabe:

Gauss–Newton-Verfeinerung: Die approximative SOS-Struktur wird mittels Newton-artiger iterativer Methoden verfeinert, um den Rückwärtsfehler zwischen der vermuteten Summe von Quadraten und dem Zielpolynom zu minimieren. Dies ergibt eine hochpräzise numerische Gram-Matrix.
Rationale Wiederherstellung: Die numerische Matrix wird in eine exakte rationale PSD-Matrix umgewandelt. Je nachdem, ob die Lösung im Inneren oder auf dem Rand des PSD-Kegels liegt, setzt das System orthogonale Projektion oder eine abgeschnittene LDL $^\top$ -Faktorisierung in Kombination mit simultaner diophantischer Approximation ein. Dieser Schritt stellt sicher, dass das resultierende SOS-Zertifikat exakt und frei von Gleitkommafehlern ist.

3. Formale Verifikation (Lean-Beweisgenerierung)

Das exakte rationale SOS-Zertifikat wird automatisch in einen maschinenprüfbaren Lean-Beweis umgewandelt.

Beweisvorlagen: Vordefinierte Lean-Vorlagen werden mit den exakten SOS-Termen gefüllt.
Verifikation: Der Lean-Beweiser überprüft zwei Bedingungen:
1. Gleichheit: Das Zielpolynom entspricht dem expandierten SOS-Ausdruck (verifiziert via linear_combination).
2. Nichtnegativität: Der SOS-Ausdruck ist nicht-negativ (verifiziert via der positivity-Taktik, die rekursiv Regeln wie $x^2 \ge 0$ anwendet).

Hauptbeiträge

Neuro-Symbolische Pipeline: Der Vorschlag von NSPI, einem End-to-End-Rahmenwerk, das die Generierung vollständiger formaler Beweise für Polynomungleichungen automatisiert, indem neuronale Vermutung, symbolische Korrektur und formale Verifikation verkettet werden.
Prinzipielle Zuverlässigkeitsbrücke: Eine neuartige Methode zur Integration von LLM-basierter heuristischer Generierung mit symbolischer exakter Zertifizierung. Dies verwandelt neuronale Vermutungen in maschinenprüfbare Beweise und ermöglicht Skalierbarkeit auf hochdimensionale multivariate Fälle (bis zu 10 Variablen), ohne auf massive Mengen an bereits existierenden formalisierten Trainingsdaten angewiesen zu sein.
Benchmark und Evaluation: Die Erstellung von PolyIneqBench, einem herausfordernden Benchmark mit 522 Ungleichungsproblemen (3 bis 10 Variablen), einschließlich realer Wettbewerbsaufgaben und synthetischer hochdimensionaler Instanzen. Umfassende Experimente zeigen, dass NSPI state-of-the-art symbolische Solver (Maple, Z3), reine LLM-Beweiser (DeepSeek-Prover-V2, Goedel-Prover) und bestehende hybride Systeme (LIPS) übertrifft, insbesondere in hochdimensionalen Szenarien.

Experimentelle Ergebnisse

Leistung: Auf PolyIneqBench erreichte NSPI eine Bestehensquote von 11,7 % für Probleme mit 10 Variablen, wohingegen symbolische Methoden (Maple, Z3) und reine LLM-Beweiser auf nahezu 0 % oder einstellige Werte fielen.
Effizienz: NSPI behielt die niedrigste durchschnittliche Ausführungszeit unter den erfolgreichen Solvern bei und zeigte eine Beschleunigung von über 10-fach im Vergleich zu mehreren LLM-basierten Beweisern.
Skalierbarkeit: Die progressive Bestärkungslernstrategie verlagerte die Fähigkeitsgrenze des Modells erfolgreich zu höheren Dimensionen, wobei Leistungssteigerungen beobachtet wurden, als das Curriculum von 3–5 auf 9–10 Variablen fortschritt.
Ablation: Experimente bestätigten, dass sowohl das synthetische Kaltstart-Training als auch das curriculum-basierte GRPO für den Erfolg des Systems entscheidend sind.

Bedeutung und Behauptungen

Die Arbeit beansprucht, ein neues Paradigma im neuro-symbolischen Theorembeweisen zu etablieren, in dem LLMs als kernsymbolische Vermutungsmaschinen fungieren und nicht nur als Suchführer. Indem LLMs als Generatoren symbolischer Priors (SOS-Strukturen) behandelt werden und sich auf symbolische Berechnung für Präzision sowie formale Verifikation für Korrektheit verlassen, adressiert dieser Ansatz die Engpassproblematik der Datenknappheit rein neuronaler Methoden und die Skalierungsgrenzen rein symbolischer Methoden.

Die Autoren positionieren NSPI als bedeutende Erweiterung der Grenze für die automatisierte Beweisführung von Polynomungleichungen, die erfolgreich hochdimensionale Fälle (bis zu 10 Variablen) handhabt, die für bestehende automatische Systeme zuvor unlösbar waren. Die Arbeit zeigt, dass die Kombination von heuristischer Entdeckung mit rigoroser Zertifizierung den praktischen Anwendungsbereich des automatisierten mathematischen Schlussfolgerns erheblich erweitern kann.