💻 computer science

Towards Solving the Gilbert-Pollak Conjecture via Large Language Models

Dieser Beitrag stellt ein KI-System vor, das große Sprachmodelle nutzt, um ausführbare geometrische Lemmata zu generieren und zu verfeinern, wodurch eine neue zertifizierte untere Schranke von 0,8559 für das Steiner-Verhältnis erreicht wird und wesentliche Fortschritte in Richtung der langjährigen Gilbert-Pollak-Vermutung erzielt werden.

Ursprüngliche Autoren: Yisi Ke, Tianyu Huang, Yankai Shu, Di He, Jingchu Gai, Liwei Wang

Veröffentlicht 2026-05-22

📖 5 Min. Lesezeit🧠 Tiefgang

CC BY 4.0

Ursprüngliche Autoren: Yisi Ke, Tianyu Huang, Yankai Shu, Di He, Jingchu Gai, Liwei 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 sind Stadtplaner und versuchen, eine Gruppe von Häusern durch Straßen zu verbinden. Sie haben zwei Möglichkeiten, dies zu tun:

Der „Direkte" Weg (Minimaler Spannbaum): Sie verbinden die Häuser direkt miteinander. Sie dürfen keine neuen Kreuzungen bauen; Sie ziehen lediglich Linien zwischen den bestehenden Häusern.
Der „Intelligente" Weg (Minimaler Steinerbaum): Ihnen ist erlaubt, neue, unsichtbare Kreuzungen (sogenannte Steiner-Punkte) überall in der Stadt zu errichten. Durch das Hinzufügen dieser zusätzlichen Knotenpunkte können Sie oft ein Netzwerk schaffen, das kürzer ist und weniger Asphalt verbraucht als der direkte Weg.

Die große Frage:
Wie viel kürzer kann der „Intelligente" Weg im Vergleich zum „Direkten" Weg sein?

1968 stellten die Mathematiker Gilbert und Pollak eine berühmte Vermutung (eine Konjektur) auf. Sie sagten: „Egal wie Sie die Häuser anordnen, der Intelligente Weg wird niemals weniger als 86,6 % (genauer gesagt $\sqrt{3}/2$ ) der Länge des Direkten Weges betragen."

Jahrzehntelang versuchten Mathematiker, dies zu beweisen. Sie schafften es zu beweisen, dass er mindestens 82,4 % der Länge beträgt, blieben jedoch dort stecken. Das mathematische Problem war wie ein riesiger, verwickelter Knoten, den menschliche Gehirne nicht entwirren konnten, weil es zu viele mögliche Formen und Winkel gab, die zu überprüfen waren.

Der neue Ansatz: Die KI-„Lemma-Fabrik"
Diese Arbeit beschreibt ein neues System, bei dem eine KI (ein Large Language Model) hilft, diesen Knoten zu lösen. Die KI versucht jedoch nicht, das gesamte Problem auf einmal zu lösen – das wäre, als würde man einem Roboter befehlen, in einer Sekunde einen ganzen Roman zu schreiben. Stattdessen bauten die Forscher eine spezialisierte Fabrik für die KI.

So funktioniert das System, veranschaulicht durch eine einfache Analogie:

1. Der „Beweis" ist ein riesiges Puzzle

Um die 86,6 %-Regel zu beweisen, müsste man jede mögliche Form des Straßennetzes überprüfen. Dies ist unmöglich, einzeln durchzugehen.
Stattdessen verwenden Mathematiker eine Strategie namens Induktion. Sie sagen: „Wenn wir beweisen können, dass jedes Mal, wenn wir ein Stück vom Netzwerk abschneiden, der verbleibende Teil immer noch den Regeln folgt, dann folgt das Ganze den Regeln."

Dafür benötigen sie winzige, spezifische Regeln, die Lemmata genannt werden. Denken Sie an ein Lemma als ein einzelnes, perfektes Puzzleteil, das besagt: „Wenn die Straßen so aussehen, dann wissen wir mit Sicherheit, dass die Länge mindestens so viel beträgt."

2. Die Aufgabe der KI: Herstellen der Puzzleteile

Die Forscher baten die KI nicht, das gesamte Puzzle zu lösen. Sie baten sie um etwas viel Kleineres: Code zu schreiben, der diese Puzzleteile generiert.

Die Einschränkung: Der KI wird gesagt: „Sie dürfen nur Code schreiben, der eine spezifische geometrische Form beschreibt (wie einen 'Gefangenen regulären Punkt' oder einen '4-Punkt-Baum')."
Die Ausgabe: Die KI schreibt ein kleines Programm (ein „Lemma"), das besagt: „Wenn die Straßenlängen $X, Y, Z$ betragen, dann ist die Gesamtlänge durch $W$ nach oben beschränkt."
Das Sicherheitsnetz: Der Code der KI wird nicht blind vertraut. Er wird in einen strengen mathematischen Rechner eingespeist (wie einen superpräzisen Taschenrechner namens Mathematica). Wenn der Rechner sagt, der Code sei falsch, versucht die KI es erneut. Wenn er „Korrekt" sagt, wird das Teil zur Sammlung hinzugefügt.

3. Die „Reflexions"-Schleife: Schwachstellen finden

Das ist der clevere Teil. Das System rät nicht einfach zufällig.

Das System versucht, die 86,6 %-Regel mit der aktuellen Sammlung von Puzzleteilen zu beweisen.
Es scheitert. Es findet eine spezifische „Engstelle" – eine seltsame Form von Straßen, bei der die aktuellen Teile nicht passen.
Das System sagt der KI: „Hey, hier bist du gescheitert. Schau dir diese spezifische Form an. Geh und schreibe ein neues Puzzleteil, das genau an diese Stelle passt."
Die KI generiert ein neues Lemma, der Rechner prüft es, und wenn es funktioniert, versucht das System erneut.

Es ist wie ein Videospiel, bei dem Sie immer wieder gegen eine Wand laufen, und das Spiel Ihnen genau sagt, wo Sie eine Brücke bauen müssen, um hindurchzukommen.

Das Ergebnis

Nach etwa 10 Runden dieser „Versuchen, Scheitern, Reflektieren, Verbessern"-Schleife baute das System eine Sammlung von Puzzleteilen auf, die so stark war, dass es schließlich eine neue, strengere Regel beweisen konnte:

Der Intelligente Weg beträgt mindestens 85,59 % der Länge des Direkten Weges.

Dies ist eine massive Verbesserung gegenüber dem vorherigen Rekord von 82,4 %, der fast 40 Jahre lang Bestand hatte.

Warum dies wichtig ist (laut der Arbeit)

Es ist günstig: Das gesamte Forschungsprojekt kostete nur ein paar hundert Dollar an Computerzeit.
Es ist schnell: Die KI benötigte nur ein paar Tage „Nachdenkens" (und einige tausend Aufrufe des Modells), um das zu leisten, was Menschen in Jahrzehnten nicht schaffen konnten.
Es ist rigoros: Die KI hat nicht einfach nur „geraten". Sie generierte Code, der mathematisch verifiziert wurde und zu 100 % korrekt ist. Der endgültige Beweis ist ein standardmäßiger mathematischer Beweis, der für sich allein steht, unabhängig von der KI.

Kurz gesagt: Die Forscher baten eine KI nicht, eine geniale Mathematikerin zu sein. Sie baten sie, eine brillante, unermüdliche Assistentin zu sein, die winzige, verifizierte Werkzeuge (Lemmata) baut, um Menschen dabei zu helfen, ein Problem zu lösen, das zuvor zu groß war, um es zu knacken. Sie verwandelten eine „Black-Box"-KI in eine transparente, schrittweise Entdeckungsmaschine.

Technischer Überblick: Zur Lösung der Gilbert-Pollak-Vermutung mittels Large Language Models

1. Problemstellung

Die Arbeit behandelt die Gilbert-Pollak-Vermutung (1968), ein bahnbrechendes offenes Problem der kombinatorischen Optimierung und der computergestützten Geometrie. Die Vermutung besagt, dass für jede endliche Menge von Punkten in der euklidischen Ebene das Verhältnis zwischen der Länge des Steiner-Minimalbaums (SMT) und des euklidischen minimalen Spannbaums (MST) durch $\sqrt{3}/2 \approx 0,866$ nach unten beschränkt ist. Dieses Verhältnis wird als Steiner-Verhältnis bezeichnet.

Während die Vermutung für kleine Anzahlen von Punkten ( $n \le 6$ ) verifiziert wurde, ist die allgemeine untere Schranke für beliebiges $n$ seit 1985 stagniert. Die bisherige untere Schranke des State-of-the-Art, etabliert durch Chung & Graham (1985), beträgt 0,824. Der Fortschritt ist aufgrund der kombinatorischen Explosion topologischer Strukturen, die für die Analyse erforderlich sind, sowie der Unlösbarkeit der geometrischen Verifikation bei manueller Herleitung ins Stocken geraten.

Die Autoren untersuchen, ob Large Language Models (LLMs), die sich in Wettbewerbsmathematik bewährt haben, erweitert werden können, um solche offenen, forschungsrelevanten Vermutungen zu bearbeiten. Sie stellen fest, dass das naive Auffordern von LLMs zur direkten Lösung der Vermutung häufig zu Halluzinationen und logischen Lücken führt, bedingt durch den riesigen, unbeschränkten Suchraum und die Knappheit forschungsrelevanter Konzepte in den Trainingsdaten.

2. Methodik

Die Autoren schlagen ein neuartiges KI-System vor, das eine direkte End-zu-End-Generierung von Beweisen vermeidet. Stattdessen zerlegt das System das Problem in einen strukturierten, iterativen Entdeckungsprozess, der durch Verifikationsfunktionen und Reflexion angetrieben wird.

2.1. Das Verifikationsframework

Die zentrale mathematische Strategie stützt sich auf einen induktionsbasierten Reduktionsbeweis (Du & Hwang, 1983). Um eine untere Schranke $\rho$ zu beweisen, muss gezeigt werden, dass für jede geometrische Konfiguration $w$ eine „Aufspaltung" des Baums existiert, sodass eine spezifische Aufspaltungsfunktion $F_\tau(w, \rho) \le 0$ erfüllt ist.

Verifikationsfunktionen: Um das kontinuierliche Minimax-Problem handhabbar zu machen, führt das System Verifikationsfunktionen ein. Dies sind obere Schranken von Aufspaltungsfunktionen, die spezifische strukturelle Einschränkungen erfüllen (Unimodalität entlang der Koordinatenachsen).
Eigenschaft des Vertex-Maximums: Ein wesentlicher theoretischer Beitrag ist der Nachweis, dass für diese Verifikationsfunktionen das globale Maximum über ein beschränktes Hyperrechteck an einem seiner Eckpunkte angenommen wird. Dies reduziert die Verifikation eines unendlichen kontinuierlichen Bereichs auf eine endliche Menge von Eckpunktprüfungen.
Branch-and-Bound: Das System verwendet einen Branch-and-Bound-Algorithmus, um den Parameterraum rekursiv zu partitionieren, die Bedingung an den Eckpunkten zu verifizieren und die Monotonie für unbeschränkte Bereiche zu überprüfen.

2.2. LLM-Agent und Lemma-Generierung

Anstatt das LLM zu bitten, die Vermutung zu beweisen, beauftragt das System es mit der Generierung regelbeschränkter geometrischer Lemmata, die als ausführbarer Code implementiert sind. Der Suchraum wird auf zwei spezifische Arten von Lemmata eingegrenzt:

Eingefangene reguläre Punkt-Lemmata: Beweis, dass unter bestimmten linearen Einschränkungen ein impliziter regulärer Punkt innerhalb eines beschränkten polygonalen Bereichs eingeschlossen ist, was Abstandsschranken ermöglicht.
Gültige 4-Punkt-Steiner-Baum-Lemmata: Beweis, dass unter spezifischen orthogonal konvexen Bedingungen eine bestimmte 4-Punkt-Steiner-Baum-Topologie gültig ist, was exakte Längenberechnungen ermöglicht.

Der LLM-Agent arbeitet in einer Schleife:

Auswahl: Er wählt relevante geometrische Prädikate (Typ A: intrinsische Eigenschaften; Typ B: ausreichende Einfangbedingungen) aus einem vordefinierten Satz aus.
Herleitung: Er verwendet symbolische Werkzeuge (Mathematica), um die Implikationen dieser Prädikate abzuleiten.
Vereinfachung: Er vereinfacht komplexe algebraische Bereiche in lineare oder orthogonal konvexe Einschränkungen, die für das Belohnungsmodell geeignet sind.
Codierung: Er gibt die abgeleiteten Bedingungen als C++-Funktionen (X_cond, AX_upper_bound usw.) aus, die als Verifikationsfunktionen dienen.

2.3. Iterativer Reflexionsmechanismus

Das System nutzt einen gezielten Reflexionsmechanismus, um Engpässe zu überwinden:

Bewertung: Das Belohnungsmodell versucht, eine Kandidaten-untere Schranke $\rho$ zu zertifizieren.
Engpass-Identifikation: Falls die Verifikation fehlschlägt, identifiziert das System den spezifischen „Engpassbereich" (eine Menge nicht-zertifizierter Hyperrechtecke), in dem die aktuellen Lemmata unzureichend sind.
Feedback: Dieser Bereich wird in einen strukturierten Prompt umgewandelt, der das LLM anweist, neue Lemmata zu generieren, die speziell auf die geometrischen Einschränkungen dieses Engpasses abzielen.
Verfeinerung: Die neuen Lemmata werden validiert und zur Menge der Verifikationsfunktionen hinzugefügt, und der Prozess wiederholt sich.

3. Hauptbeiträge

Neuartiges KI-System für theoretische Entdeckungen: Die Arbeit stellt ein System vor, das die Entdeckung intermediärer geometrischer Lemmata für ein jahrzehntealtes offenes Problem erfolgreich automatisiert und über die Standardlösung von Wettbewerbsproblemen hinausgeht.
Verifikationsfunktionen und Vertex-Eigenschaft: Die Autoren definieren Verifikationsfunktionen formal und beweisen die „Eigenschaft des Vertex-Maximums", die eine rigorose, rechnerisch handhabbare Verifikation unterer Schranken über kontinuierliche Bereiche ermöglicht.
Zerlegungsstrategie: Durch die Zerlegung der Vermutung in die Generierung spezifischer, regelbeschränkter Lemmata (Eingefangene Punkte und Gültige 4-Punkt-Bäume) anstelle vollständiger Beweise verwaltet das System den Suchraum effektiv und minimiert Halluzinationen.
Engpass-gesteuerte Reflexion: Die Einführung eines Reflexionsmechanismus, der die geometrischen Bereiche, die weitere Verbesserungen verhindern, explizit identifiziert und angreift, anstatt sich auf generische Selbstkorrektur zu verlassen.

4. Ergebnisse

Neue untere Schranke: Das System verbesserte die zertifizierte untere Schranke des Steiner-Verhältnisses erfolgreich von 0,824 (Chung & Graham, 1985) auf 0,8559.
Effizienz: Der gesamte Forschungsaufwand erforderte nur etwa 10 Iterationen der Verfeinerungsschleife.
Ressourcennutzung: Der Prozess umfasste ungefähr tausende LLM-Aufrufe und verbrauchte etwa 0,5 Millionen Tokens (ca. 35K pro Runde) über 4,6 Stunden reasoning-Zeit. Die gesamten Rechenkosten beliefen sich auf einige hundert Dollar.
Robustheit: Experimente mit verschiedenen LLM-Backbones (GPT-5 und Gemini 3 Pro) ergaben eine konsistente Konvergenz auf dieselbe untere Schranke und demonstrierten die Robustheit des Frameworks gegenüber der Modellwahl.
Verifikation: Alle generierten Lemmata wurden manuell auf Korrektheit überprüft, und die finale untere Schranke wurde über den gesamten Parameterraum hinweg rigoros mit symbolischen Werkzeugen (Zylindrische Algebraische Zerlegung) verifiziert.

5. Bedeutung und Behauptungen

Die Arbeit behauptet, das große Potenzial von LLM-basierten Systemen für die fortgeschrittene mathematische Forschung zu demonstrieren, insbesondere in Domänen, die tiefe geometrische Intuition und kombinatorische Suche erfordern.

Skalierbarkeit: Die Autoren argumentieren, dass ihr Ansatz ein skalierbares Paradigma bietet, bei dem LLMs die kreative Suche und Lemma-Generierung übernehmen, während symbolische Werkzeuge die formale Verifikation übernehmen. Diese Arbeitsteilung nutzt die Stärken beider Seiten.
Zugänglichkeit: Mit Gesamtkosten von nur einigen hundert Dollar legt die Arbeit nahe, dass LLM-unterstützte theoretische Forschung für Forscher ohne massive Rechenbudgets zugänglich ist.
Generalisierbarkeit: Die Autoren schlagen zwei Designprinzipien vor, von denen sie glauben, dass sie auf andere mathematische Entdeckungsprobleme übertragbar sind:
1. Aufbau eines strukturierten Denkraums durch Zerlegung von Problemen in parametrisierte Lemmata anstelle von End-zu-End-Beweisen.
2. Reflexion über lokale Verifikationsfehler, indem spezifische Engpassbereiche zurück an das Modell gefüttert werden, um eine gezielte Verfeinerung zu steuern.

Die Arbeit bewahrt Bescheidenheit hinsichtlich des Endergebnisses und stellt fest, dass, obwohl die untere Schranke signifikant verbessert wurde, die Vermutung selbst (0,866) weiterhin unbewiesen bleibt. Darüber hinaus erkennen die Autoren aktuelle Grenzen an, wie etwa die Abhängigkeit von menschlicher Verifikation für die Korrektheit der Lemmata und die Skalierbarkeitsprobleme der symbolischen Verifikation (CAD) für höherdimensionale oder komplexere Topologien. Sie schlagen vor, dass zukünftige Arbeiten formale Beweisassistenten (z. B. Lean) einbeziehen könnten, um eine vollständig autonome Entdeckung zu erreichen.