🤖 AI

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

Dit artikel introduceert NSPI, een neuro-symbolisch raamwerk dat grote taalmodellen benut om benaderende Sum-of-Squares-vermoedens te formuleren en symbolische berekening toepast om deze te verfijnen tot exacte, machine-gecontroleerde Lean-bewijzen, waardoor schaalbare geautomatiseerde bewijsvoering voor polynoomongelijkheden met tot 10 variabelen wordt bereikt.

Oorspronkelijke auteurs: Ruobing Zuo, Hanrui Zhao, Gaolei He, Zhengfeng Yang, Jianlin Wang

Gepubliceerd 2026-05-18

📖 4 min leestijd☕ Koffiepauze-leesvoer

CC BY 4.0

Oorspronkelijke auteurs: Ruobing Zuo, Hanrui Zhao, Gaolei He, Zhengfeng Yang, Jianlin 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 probeert te bewijzen dat een complexe, meerlagige taart altijd "voldoende zoet" is (wiskundig: niet-negatief), ongeacht hoe je hem snijdt of de ingrediënten verandert. In de wereld van de wiskunde heet dit het bewijzen van een polynoomongelijkheid.

Lange tijd hadden wiskundigen twee hoofdmanieren om dit te doen, maar beide hadden grote gebreken:

De "Pure Logica"-methode (Symbolisch): Dit is als proberen het taartprobleem op te lossen door elke enkele chemische reactie van de ingrediënten op een schoolbord op te schrijven. Het is perfect accuraat, maar als de taart te veel ingrediënten (variabelen) heeft, vult het schoolbord zich direct en crasht de methode. Het is te traag en rommelig voor grote problemen.
De "AI-gok"-methode (LLM's): Dit is als een zeer slimme, creatieve chef vragen om het recept te raden. De chef is snel en goed bij kleine taarten, maar wanneer de taart enorm en ingewikkeld wordt, begint de chef ingrediënten te hallucineren die niet bestaan of wiskundige fouten te maken. Ze kunnen niet bewijzen dat hun antwoord 100% waar is.

Dit artikel introduceert een nieuw team genaamd NSPI (Neuro-Symbolic Polynomial Inequality proving). Denk aan NSPI als een perfecte samenwerking tussen een creatieve chef en een strenge kwaliteitscontroleur.

Hier is hoe hun "assemblagelijn" stap voor stap werkt:

Stap 1: De Creatieve Chef (De LLM)

Eerst vraagt het team een Large Language Model (de "Chef") om naar een moeilijk wiskundig probleem te kijken. De Chef probeert niet direct de moeilijke wiskunde te doen. In plaats daarvan gebruikt hij zijn creativiteit om een structuur te raden.

De Analogie: Stel je voor dat de Chef zegt: "Ik wed dat deze taart bestaat uit drie specifieke lagen suikerklontjes die op elkaar gestapeld zijn."
In wiskundige termen raadt de LLM een Som-van-Kwadraten (SOS)-ontbinding. Hij suggereert: "Deze ingewikkelde uitdrukking is waarschijnlijk gewoon de som van een paar eenvoudigere dingen gekwadrateerd."
Cruciaal punt: De gok van de Chef is meestal een benadering. Het is dichtbij, maar het kan kleine decimale fouten bevatten (zoals zeggen dat een suikerklontje 1,0000001 gram weegt in plaats van precies 1).

Stap 2: De Kwaliteitscontroleur (Symbolische Correctie)

De gok van de Chef wordt doorgegeven aan de "Kwaliteitscontroleur", een krachtig computeralgebrasysteem.

De Analogie: De Controleur neemt het ruwe schets van de Chef en gebruikt een microscoop om de kleine fouten te herstellen. Hij gebruikt een techniek genaamd Newton's Methode (een wiskundige manier om in te zoomen op het exacte antwoord) en Rational Recovery (het omzetten van rommelige decimalen in schone, exacte breuken).
Als de Chef de lagen "ongeveer" 1,5, 2,3 en 0,7 had geraden, berekent de Controleur de exacte getallen: 3/2, 23/10 en 7/10.
Nu is de gok omgezet in een perfect, exact wiskundig certificaat.

Stap 3: De Rechtbankrechter (Lean Verificatie)

Tenslotte neemt het team dit exacte certificaat mee naar een "Rechter" genaamd Lean.

De Analogie: Lean is een strenge, onwankelbare rechter die elke stap van het werk van de Controleur controleert. Hij geeft niets om "gevoel" of "gokken". Hij accepteert alleen bewijzen die logisch waterdicht zijn.
Omdat de Controleur een exact certificaat heeft verstrekt, kan de Rechter gemakkelijk verifiëren: "Ja, als je deze exacte getallen kwadrateert en optelt, krijg je de oorspronkelijke taart. En omdat kwadraten altijd positief zijn, is de taart altijd zoet."
De Rechter geeft vervolgens een machinegecontroleerd bewijs af dat 100% gegarandeerd correct is.

Waarom is dit een grote zaak?

Het artikel testte dit team op 522 zeer moeilijke wiskundige problemen, waarvan sommige tot 10 verschillende variabelen (ingrediënten) hadden.

De Oude Logica-methoden gaven het op wanneer de problemen te groot werden (te veel ingrediënten).
De Oude AI-methoden raakten in de war en maakten fouten bij de grote problemen.
Het NSPI-team slaagde waar anderen faalden. Ze konden problemen met 10 variabelen oplossen die geen enkele andere methode aan kon.

De Conclusie

Het artikel beweert dat ze door een AI de vorm van de oplossing te laten raden en vervolgens wiskundige hulpmiddelen te gebruiken om de details te herstellen en een computer om de waarheid te verifiëren, een systeem hebben gebouwd dat complexe ongelijkheidsproblemen sneller en betrouwbaarder kan oplossen dan ooit tevoren. Ze hebben niet alleen geraden; ze hebben een brug gebouwd van een "goede gok" naar een "bewezen feit".

Wat ze NIET hebben beweerd:

Ze hebben niet gezegd dat dit ziekten zal genezen of de aandelenmarkt zal voorspellen.
Ze hebben niet beweerd dat dit werkt voor elk type wiskundig probleem, alleen voor het bewijzen dat bepaalde polynoomuitdrukkingen altijd positief zijn.
Ze hebben niet beweerd dat dit menselijke wiskundigen volledig vervangt, maar eerder dat het een zeer specifiek, moeilijk type redeneren automatiseert.

Technische Samenvatting: Van door LLM gegenereerde conjecturen tot Lean-formaliseringen

Probleemstelling

Geautomatiseerd bewijzen van polynoomongelijkheden is een fundamentele uitdaging in wiskundig redeneren, met name voor hoogdimensionale en multivariate gevallen. Bestaande aanpakken kampen met aanzienlijke schaalbaarheidsbeperkingen:

Puur symbolische methoden: Hoewel ze sterke garanties bieden, lijden methoden gebaseerd op Som-van-Kwadraten (SOS)-ontbinding en Semidefiniete Programmering (SDP) aan combinatorische explosie en snelle groei van tussentijdse expressies naarmate het aantal variabelen of de graad toeneemt. Ze falen vaak om gestructureerde, voor mensen leesbare bewijzen te produceren.
Puur op LLM gebaseerde methoden: Grote Taalmodellen (LLM's) geïntegreerd met bewijshulpmiddelen (zoals Lean, Isabelle) hebben veelbelovend getoond, maar worden beperkt door het gebrek aan hoogwaardige, geformaliseerde trainingsdata. Ze worstelen met complexe algebraïsche ongelijkheden, met name die met meer dan 5 variabelen, en missen vaak het vermogen om rigoureuze, machine-controleerbare certificaten te genereren.

De kernuitdaging is de kloof te overbruggen tussen heuristische ontdekking en rigoureuze formele verificatie, waardoor geautomatiseerd bewijzen van onbeperkte polynoomongelijkheden in hoogdimensionale settings (tot 10 variabelen) mogelijk wordt met machine-gecontroleerde correctheid.

Methodologie: NSPI-raamwerk

De auteurs stellen NSPI (Neuro-Symbolische SOS-gebaseerde Polynoomongelijkheid-Bewijzen) voor, een raamwerk dat de complementaire sterktes van LLM's en symbolische berekening integreert in een end-to-end pijplijn. Het proces bestaat uit drie hoofdfasen:

1. Neuronale Conjectuur (LLM-gestuurde SOS-generatie)

In plaats van LLM's uitsluitend te gebruiken voor zoekrichting, verheft NSPI ze tot primaire conjectuurgeneratoren.

Dataconstructie: De auteurs construeren een groot dataset van niet-negatieve polynoom-SOS-paren met twee nieuwe strategieën:
- Berekeningsgedreven: Genereren van Gram-matrices via spectrale verschuiving of LMI-optimalisatie om positief semi-definite (PSD) eigenschappen te waarborgen met gecontroleerde coëfficiënten.
- Structuurgedreven: Benutten van algebraïsche structuren zoals diagonaal overheersende (dd) en geschaalde diagonaal overheersende (sdd) matrices, die per ontwerp PSD-eigenschappen garanderen.
Training: Een tweestaps trainingsplan wordt toegepast:
- Koude start: Supervised Fine-Tuning (SFT) op meer dan één miljoen synthetische polynoom-SOS-paren om fundamenteel structureel redeneren te vestigen.
- Progressief Versterkend Leren: Curriculum-gebaseerde Group Relative Policy Optimization (GRPO) wordt toegepast op uitdagende gevallen (variabelenaantallen toenemend van 3–5 naar 9–10). De beloningsfunctie combineert nauwkeurigheid (numerieke fideliteit), naleving van formaat en straffen voor algebraïsche structuur om te waarborgen dat de LLM plausibele SOS-structuren genereert.
Output: De LLM stelt een benaderende SOS-ontbinding voor (een som van gekwadrateerde termen) voor een gegeven polynoom.

2. Symbolische Correctie (Exacte Rationale Herstelling)

Om de benaderende conjectuur van de LLM om te zetten in een rigoureus bewijs, verfijnt een symbolische correctiemodule de output:

Gauss–Newton-verfijning: De benaderende SOS-structuur wordt verfijnd met Newton-achtige iteratieve methoden om de achterwaartse fout tussen de geconjectureerde som-van-kwadraten en het doelpolynoom te minimaliseren. Dit levert een hoogprecisie numerieke Gram-matrix op.
Rationale Herstelling: De numerieke matrix wordt omgezet in een exacte rationale PSD-matrix. Afhankelijk van of de oplossing in het inwendige of op de rand van de PSD-kegel ligt, past het systeem orthogonale projectie of afgeknotte LDL $^\top$ -factorisatie toe in combinatie met simultane Diophantische approximatie. Deze stap waarborgt dat het resulterende SOS-certificaat exact is en vrij van drijvende-kommafouten.

3. Formele Verificatie (Lean-bewijsgeneratie)

Het exacte rationale SOS-certificaat wordt automatisch omgezet in een machine-controleerbaar Lean-bewijs.

Bewijstemplates: Vooraf gedefinieerde Lean-templates worden gevuld met de exacte SOS-termen.
Verificatie: De Lean-prover verifieert twee voorwaarden:
1. Gelijkheid: Het doelpolynoom is gelijk aan de uitgebreide SOS-expressie (geverifieerd via linear_combination).
2. Niet-negativiteit: De SOS-expressie is niet-negatief (geverifieerd via de positivity-tactiek, die recursief regels toepast zoals $x^2 \ge 0$ ).

Belangrijkste Bijdragen

Neuro-Symbolische Pijplijn: Het voorstellen van NSPI, een end-to-end raamwerk dat de generatie van volledige formele bewijzen voor polynoomongelijkheden automatiseert door neuronale conjectuur, symbolische correctie en formele verificatie te koppelen.
Principiële Betrouwbaarheidsbrug: Een nieuwe methode voor het integreren van op LLM gebaseerde heuristische generatie met symbolische exacte certificering. Dit transformeert neuronale conjecturen in machine-controleerbare bewijzen, waardoor schaalbaarheid naar hoogdimensionale multivariate gevallen (tot 10 variabelen) mogelijk wordt zonder te vertrouwen op enorme hoeveelheden reeds bestaande geformaliseerde trainingsdata.
Benchmark en Evaluatie: De constructie van PolyIneqBench, een uitdagende benchmark met 522 ongelijkheidsproblemen (3 tot 10 variabelen), inclusief real-world competitieproblemen en synthetische hoogdimensionale gevallen. Uitgebreide experimenten tonen aan dat NSPI de state-of-the-art symbolische solvers (Maple, Z3), puur op LLM gebaseerde bewijzers (DeepSeek-Prover-V2, Goedel-Prover) en bestaande hybride systemen (LIPS) overtreft, met name in hoogdimensionale scenario's.

Experimentele Resultaten

Prestatie: Op PolyIneqBench bereikte NSPI een slaagpercentage van 11,7% voor problemen met 10 variabelen, terwijl symbolische methoden (Maple, Z3) en puur op LLM gebaseerde bewijzers daalden tot bijna 0% of enkele cijfers.
Efficiëntie: NSPI behield de laagste gemiddelde uitvoertijd onder succesvolle solvers, wat een snelheidswinst van meer dan 10x toonde ten opzichte van meerdere op LLM gebaseerde bewijzers.
Schaalbaarheid: De progressieve versterkende leerstrategie verschuifde succesvol de capabilitygrens van het model naar hogere dimensies, met prestatiewinsten waargenomen naarmate het curriculum van 3–5 variabelen naar 9–10 variabelen verschuift.
Ablatie: Experimenten bevestigden dat zowel de synthetische koude-starttraining als het curriculum-gebaseerde GRPO cruciaal zijn voor het succes van het systeem.

Betekenis en Claims

Het artikel claimt een nieuw paradigma te vestigen in neuro-symbolisch stellingbewijzen waarbij LLM's fungeren als kernsymbolische conjectuurmotoren in plaats van louter zoekrichting. Door LLM's te behandelen als generators van symbolische priors (SOS-structuren) en te vertrouwen op symbolische berekening voor precisie en formele verificatie voor correctheid, adresseert de aanpak de bottleneck van data-schaarste bij puur neuronale methoden en de schaalbaarheidslimieten van puur symbolische methoden.

De auteurs positioneren NSPI als een significante uitbreiding van de grens voor geautomatiseerd bewijzen van polynoomongelijkheden, met succesvolle behandeling van hoogdimensionale gevallen (tot 10 variabelen) die voorheen onhandelbaar waren voor bestaande geautomatiseerde systemen. Het werk toont aan dat het combineren van heuristische ontdekking met rigoureuze certificering het praktische toepassingsgebied van geautomatiseerd wiskundig redeneren aanzienlijk kan verbreden.