💻 computer science

Towards Solving the Gilbert-Pollak Conjecture via Large Language Models

Dit artikel presenteert een AI-systeem dat gebruikmaakt van grote taalmodellen om uitvoerbare geometrische lemma's te genereren en te verfijnen, waarmee een nieuwe gecertificeerde ondergrens van 0,8559 voor de Steiner-ratio wordt bereikt en aanzienlijke vooruitgang wordt geboekt richting het langdurige Gilbert-Pollak- conjectuur.

Oorspronkelijke auteurs: Yisi Ke, Tianyu Huang, Yankai Shu, Di He, Jingchu Gai, Liwei Wang

Gepubliceerd 2026-05-22

📖 5 min leestijd🧠 Diepgaand

CC BY 4.0

Oorspronkelijke auteurs: Yisi Ke, Tianyu Huang, Yankai Shu, Di He, Jingchu Gai, Liwei Wang

Oorspronkelijk artikel gelicentieerd onder CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Dit is een AI-gegenereerde uitleg van het onderstaande artikel. Het is niet geschreven of goedgekeurd door de auteurs. Raadpleeg het oorspronkelijke artikel voor technische nauwkeurigheid. Lees de volledige disclaimer

Stel je voor dat je een stedenbouwkundige bent die een groep huizen met wegen moet verbinden. Je hebt twee manieren om dit te doen:

De "Directe" Weg (Minimum Spanning Tree): Je verbindt de huizen direct met elkaar. Je mag geen nieuwe kruispunten aanleggen; je tekent alleen lijnen tussen de bestaande huizen.
De "Slimme" Weg (Steiner Minimal Tree): Je mag overal in de stad nieuwe, onzichtbare kruispunten aanleggen (zogenaamde Steiner-punten). Door deze extra knooppunten toe te voegen, kun je vaak een netwerk creëren dat korter is en minder asfalt vereist dan de directe weg.

De Grote Vraag:
Hoeveel korter kan de "Slimme" weg zijn in vergelijking met de "Directe" weg?

In 1968 deden wiskundigen Gilbert en Pollak een beroemde gok (een conjectuur). Ze zeiden: "Het maakt niet uit hoe je de huizen rangschikt, de Slimme Weg zal nooit minder dan 86,6% (specifiek $\sqrt{3}/2$ ) van de lengte van de Directe Weg zijn."

Decennialang probeerden wiskundigen dit te bewijzen. Het lukte hen om te bewijzen dat het ten minste 82,4% van de lengte was, maar daar bleven ze hangen. Het wiskundige probleem was als een gigantische, verwarde knoop die menselijke hersenen niet konden ontwarren omdat er te veel mogelijke vormen en hoeken waren om te controleren.

De Nieuwe Aanpak: De AI "Lemma-Fabriek"
Dit artikel beschrijft een nieuw systeem waarbij een AI (een Large Language Model) helpt bij het oplossen van deze knoop. Maar de AI probeert het hele probleem niet in één keer op te lossen – dat zou zijn alsof je een robot vraagt om in één seconde een hele roman te schrijven. In plaats daarvan bouwden de onderzoekers een gespecialiseerde fabriek voor de AI.

Hier is hoe het systeem werkt, met behulp van een eenvoudige analogie:

1. Het "Bewijs" is een Enorme Legpuzzel

Om de 86,6%-regel te bewijzen, moet je elke mogelijke vorm controleren die het wegennetwerk kan aannemen. Dit is onmogelijk om één voor één te doen.
In plaats daarvan gebruiken wiskundigen een strategie die inductie heet. Ze zeggen: "Als we kunnen bewijzen dat elke keer als we een stuk van het netwerk afsnijden, het resterende stuk nog steeds aan de regels voldoet, dan voldoet het hele ding aan de regels."

Hiervoor hebben ze kleine, specifieke regels nodig die lemma's heten. Denk aan een lemma als een enkel, perfect puzzelstukje dat zegt: "Als de wegen er zo uitzien, dan weten we met zekerheid dat de lengte ten minste dat is."

2. De Taak van de AI: Het Maken van de Puzzelstukjes

De onderzoekers vroegen de AI niet om de hele puzzel op te lossen. Ze vroegen haar iets veel kleiners te doen: Schrijf code die deze puzzelstukjes genereert.

De Beperking: De AI krijgt te horen: "Je mag alleen code schrijven die een specifieke geometrische vorm beschrijft (zoals een 'Trapped Regular Point' of een '4-Point Tree')."
De Output: De AI schrijft een klein programma (een "lemma") dat zegt: "Als de weglengtes $X, Y, Z$ zijn, dan is de totale lengte begrensd door $W$ ."
Het Veiligheidsnet: De code van de AI wordt niet blindelings vertrouwd. Het wordt ingevoerd in een strikte wiskundige rekenmachine (zoals een super-nauwkeurige rekenmachine genaamd Mathematica). Als de rekenmachine zegt dat de code fout is, probeert de AI het opnieuw. Als het "Correct" zegt, wordt het stukje aan de collectie toegevoegd.

3. De "Reflectie"-lus: Het Vinden van de Zwakke Plekken

Dit is het slimme deel. Het systeem raadt niet zomaar willekeurig.

Het systeem probeert de 86,6%-regel te bewijzen met de huidige collectie puzzelstukjes.
Het faalt. Het vindt een specifieke "bottleneck" – een vreemde vorm van wegen waar de huidige stukjes niet in passen.
Het systeem vertelt de AI: "Hé, je bent hier gefaald. Kijk naar deze specifieke vorm. Ga een nieuw puzzelstukje schrijven dat precies op deze plek past."
De AI genereert een nieuw lemma, de rekenmachine controleert het, en als het werkt, probeert het systeem het opnieuw.

Het is als een videospel waar je steeds tegen een muur aanloopt, en het spel vertelt je precies waar je een brug moet bouwen om erlangs te komen.

Het Resultaat

Na ongeveer 10 rondes van deze "probeer, faal, reflecteer, verbeter"-lus, bouwde het systeem een collectie puzzelstukjes die zo sterk was dat het eindelijk een nieuwe, strakkere regel kon bewijzen:

De Slimme Weg is ten minste 85,59% van de lengte van de Directe Weg.

Dit is een enorme verbetering ten opzichte van het vorige record van 82,4%, dat bijna 40 jaar had gestaan.

Waarom Dit Belangrijk Is (Volgens het Artikel)

Het is Goedkoop: Het hele onderzoeksproject kostte slechts een paar honderd dollar aan computertijd.
Het is Snel: Het kostte de AI slechts een paar dagen "nadenken" (en enkele duizenden oproepen aan het model) om te doen wat mensen decennialang niet konden.
Het is Strenge: De AI "gokte" niet zomaar. Het genereerde code die wiskundig was geverifieerd als 100% correct. Het uiteindelijke bewijs is een standaard wiskundig bewijs dat op zichzelf staat, onafhankelijk van de AI.

Kortom: De onderzoekers vroegen een AI niet om een genie-wiskundige te zijn. Ze vroegen haar om een briljante, onvermoeibare assistent te zijn die kleine, geverifieerde hulpmiddelen (lemma's) bouwt om mensen te helpen een probleem op te lossen dat voorheen te groot was om te kraken. Ze veranderden een "black box" AI in een transparante, stap-voor-stap ontdekkingsmotor.

Technische Samenvatting: Op weg naar het oplossen van de Gilbert-Pollak-conjectuur via Large Language Models

1. Probleemstelling

Het artikel behandelt de Gilbert-Pollak-conjectuur (1968), een fundamenteel open probleem in combinatorische optimalisatie en computationele meetkunde. De conjectuur stelt dat voor elke eindige verzameling punten in het Euclidische vlak de verhouding tussen de lengte van de Steiner-minimale boom (SMT) en de Euclidische minimale opspannende boom (MST) een ondergrens heeft van $\sqrt{3}/2 \approx 0,866$ . Deze verhouding staat bekend als de Steiner-verhouding.

Hoewel de conjectuur is geverifieerd voor kleine aantallen punten ( $n \le 6$ ), is de algemene ondergrens voor willekeurige $n$ sinds 1985 stilstaan. De vorige state-of-the-art ondergrens, vastgesteld door Chung & Graham (1985), bedraagt 0,824. Vooruitgang is tot stilstand gekomen door de combinatorische explosie van topologische structuren die voor analyse vereist zijn, en de onbehandelbaarheid van de geometrische verificatie die betrokken is bij handmatige afleiding.

De auteurs onderzoeken of Large Language Models (LLM's), die bekwaamheid hebben getoond op het gebied van wiskunde op wedstrijd niveau, kunnen worden uitgebreid om dergelijke open conjecturen op onderzoeks niveau aan te pakken. Zij merken op dat het naïef opvragen van LLM's om de conjectuur direct op te lossen vaak resulteert in hallucinaties en logische gaten, vanwege de enorme, onbeperkte zoekruimte en de schaarste aan concepten op onderzoeks niveau in de trainingsdata.

2. Methodologie

De auteurs stellen een nieuw AI-systeem voor dat directe end-to-end bewijsgeneratie vermijdt. In plaats daarvan decomposeert het systeem het probleem in een gestructureerd, iteratief ontdekkingsproces dat wordt aangedreven door verificatiefuncties en reflectie.

2.1. Het Verificatiekader

De kern van de wiskundige strategie berust op een op induktie gebaseerd reductieargument (Du & Hwang, 1983). Om een ondergrens $\rho$ te bewijzen, moet men aantonen dat voor elke geometrische configuratie $w$ , er een "splitsing" van de boom bestaat waarbij een specifieke splitsingsfunctie $F_\tau(w, \rho) \le 0$ .

Verificatiefuncties: Om het continue minimax-probleem behandelbaar te maken, introduceert het systeem verificatiefuncties. Dit zijn bovengrenzen van splitsingsfuncties die aan specifieke structurele beperkingen voldoen (unimodaliteit langs coördinaatassen).
Eigenschap van het Hoekpuntmaximum: Een belangrijke theoretische bijdrage is het bewijzen dat voor deze verificatiefuncties het globale maximum over een begrensde hyperrechthoek wordt bereikt in een van de hoekpunten. Dit reduceert de verificatie van een oneindig continu domein tot een eindige set van hoekpuntcontroles.
Branch-and-Bound: Het systeem maakt gebruik van een Branch-and-Bound-algoritme om de parameterruimte recursief te partitioneren, waarbij de voorwaarde wordt geverifieerd in de hoekpunten en monotonie wordt gecontroleerd voor onbegrensde gebieden.

2.2. LLM-agent en Lemma-generatie

In plaats van de LLM te vragen de conjectuur te bewijzen, geeft het systeem de taak om regel-gedwongen geometrische lemma's te genereren die worden geïmplementeerd als uitvoerbare code. De zoekruimte wordt beperkt tot twee specifieke soorten lemma's:

Vastzittende Regelmatige Punten Lemma's: Het bewijzen dat onder bepaalde lineaire beperkingen een impliciet regelmatig punt is opgesloten binnen een begrensde veelhoekige regio, wat afstands grenzen mogelijk maakt.
Geldige 4-Punt Steiner-boom Lemma's: Het bewijzen dat onder specifieke orthogonaal convexe voorwaarden een specifieke 4-punt Steiner-boom topologie geldig is, wat exacte lengteberekeningen mogelijk maakt.

De LLM-agent werkt in een lus:

Selectie: Het selecteert relevante geometrische predicaten (Type A: intrinsieke eigenschappen; Type B: voldoende vastzettingsvoorwaarden) uit een vooraf gedefinieerde set.
Afleiding: Het gebruikt symbolische hulpmiddelen (Mathematica) om de implicaties van deze predicaten af te leiden.
Vereenvoudiging: Het vereenvoudigt complexe algebraïsche regio's tot lineaire of orthogonaal convexe beperkingen die geschikt zijn voor het beloningsmodel.
Codering: Het geeft de afgeleide voorwaarden uit als C++-functies (X_cond, AX_upper_bound, etc.) die dienen als verificatiefuncties.

2.3. Iteratief Reflectiemechanisme

Het systeem maakt gebruik van een gericht reflectiemechanisme om knelpunten te overwinnen:

Evaluatie: Het beloningsmodel probeert een kandidaat-ondergrens $\rho$ te certificeren.
Knelpuntidentificatie: Als verificatie faalt, identificeert het systeem het specifieke "knelpuntgebied" (een set van niet-gecertificeerde hyperrechthoeken) waar de huidige lemma's ontoereikend zijn.
Feedback: Dit gebied wordt omgezet in een gestructureerde prompt, waarbij de LLM instructies krijgt om nieuwe lemma's te genereren die specifiek gericht zijn op de geometrische beperkingen van dit knelpunt.
Verfijning: De nieuwe lemma's worden gevalideerd en toegevoegd aan de set verificatiefuncties, en het proces wordt herhaald.

3. Belangrijkste Bijdragen

Nieuw AI-systeem voor Theoretische Ontdekking: Het artikel presenteert een systeem dat succesvol de ontdekking van intermediaire geometrische lemma's voor een decennia oud open probleem automatiseert, en verder gaat dan standaard probleemoplossing op wedstrijd niveau.
Verificatiefuncties en Hoekpuntmaximum Eigenschap: De auteurs definiëren formeel verificatiefuncties en bewijzen de "Hoekpuntmaximum Eigenschap", wat een rigoureuze, computationeel behandelbare verificatie van ondergrenzen over continue domeinen mogelijk maakt.
Decompositiestrategie: Door de conjectuur te decomponeren in de generatie van specifieke, regel-gedwongen lemma's (Vastzittende Punten en Geldige 4-Punt Bomen) in plaats van volledige bewijzen, beheert het systeem effectief de zoekruimte en minimaliseert het hallucinaties.
Knelpunt-gedreven Reflectie: De introductie van een reflectiemechanisme dat expliciet de geometrische regio's identificeert en aanvalt die verdere verbetering belemmeren, in plaats van te vertrouwen op generieke zelfcorrectie.

4. Resultaten

Nieuwe Ondergrens: Het systeem slaagde erin de gecertificeerde ondergrens van de Steiner-verhouding te verbeteren van 0,824 (Chung & Graham, 1985) naar 0,8559.
Efficiëntie: De gehele onderzoeksinspanning vereiste slechts ongeveer 10 iteraties van de verfijningslus.
Ressourcengebruik: Het proces omvatte ongeveer duizenden LLM-aanroepen en verbruikte ongeveer 0,5 miljoen tokens (ongeveer 35K per ronde) over 4,6 uur redeneertijd. De totale computatiekosten bedroegen enkele honderden dollars.
Robuustheid: Experimenten met verschillende LLM-achtergronden (GPT-5 en Gemini 3 Pro) leverden consistente convergentie naar dezelfde ondergrens op, wat de robuustheid van het kader voor modelkeuze aantoont.
Verificatie: Alle gegenereerde lemma's werden handmatig gecontroleerd op correctheid, en de uiteindelijke ondergrens werd rigoureus geverifieerd over de gehele parameterruimte met behulp van symbolische hulpmiddelen (Cylindrical Algebraic Decomposition).

5. Betekenis en Claims

Het artikel claimt het sterke potentieel aan te tonen van op LLM gebaseerde systemen voor geavanceerd wiskundig onderzoek, specifiek in domeinen die diepe geometrische intuïtie en combinatorische zoektochten vereisen.

Schaalbaarheid: De auteurs betogen dat hun aanpak een schaalbaar paradigma biedt waarbij LLM's creatieve zoektochten en lemma-generatie afhandelen, terwijl symbolische hulpmiddelen formele verificatie uitvoeren. Deze taakverdeling benut de sterke punten van beide.
Toegankelijkheid: Met totale kosten van slechts enkele honderden dollars suggereert het werk dat door LLM's ondersteund theoretisch onderzoek toegankelijk is voor onderzoekers zonder enorme computebudgetten.
Generaliseerbaarheid: De auteurs stellen twee ontwerpprincipes voor die zij geloven overdraagbaar zijn naar andere wiskundige ontdekkingsproblemen:
1. Het construeren van een gestructureerde redeneerruimte door problemen te decomponeren in geparametriseerde lemma's in plaats van end-to-end bewijzen.
2. Reflecteren op lokale verificatiefouten door specifieke knelpuntregio's terug te voeren naar het model om gerichte verfijning te sturen.

Het artikel blijft bescheiden wat het eindresultaat betreft, en merkt op dat hoewel de ondergrens aanzienlijk is verbeterd, de conjectuur zelf (0,866) nog steeds onbewezen blijft. Bovendien erkennen de auteurs huidige beperkingen, zoals de afhankelijkheid van menselijke verificatie voor de correctheid van lemma's en de schaalbaarheidsproblemen van symbolische verificatie (CAD) voor hogere dimensies of complexere topologieën. Zij suggereren dat toekomstig werk formeel bewijsassistenten (bijvoorbeeld Lean) kan omvatten om volledig autonome ontdekking te bereiken.