A Neuro-Symbolic Approach for Reliable Proof Generation with LLMs: A Case Study in Euclidean Geometry

Dit paper introduceert een neuro-symbolische aanpak die grote taalmodellen combineert met analoge probleemoplossing en een formele verificateur om de betrouwbaarheid en nauwkeurigheid van het genereren van wiskundige bewijzen in de euclidische meetkunde aanzienlijk te verbeteren.

De kern

Stel je voor dat je een zeer slimme, creatieve schrijver hebt die alles over de wereld weet. Hij kan prachtige verhalen vertellen, gedichten schrijven en zelfs complexe ideeën uitleggen. Maar als je hem vraagt om een wiskundig bewijs te schrijven – een strikt logisch stappenplan dat 100% foutloos moet zijn – dan loopt hij vast. Hij begint te gissen, maakt logische fouten en komt met antwoorden die "klinken alsof ze waar zijn", maar die in de wiskunde niet kloppen.

Dit is precies het probleem dat de auteurs van dit paper proberen op te lossen. Ze hebben een slimme manier bedacht om deze "schrijver" (een Large Language Model of LLM) te helpen met wiskunde, door hem te koppelen aan een strenge controleur en een slimme bibliothecaris.

Hier is hoe hun systeem werkt, vertaald naar alledaagse taal:

1. De Probleemstelling: De "Gokker" vs. De "Logica"

Grote taalmodellen (zoals de AI die dit antwoord voor je schrijft) werken op basis van patronen. Ze raden het volgende woord op basis van wat ze eerder hebben gelezen. In een verhaal is dat geweldig. In wiskunde is het gevaarlijk, want daar mag er geen enkele fout zijn. Een bewijs moet logisch waterdicht zijn, niet alleen maar "plausibel" klinken.

2. De Oplossing: Een Neuro-Symbolische "Drie-Handen"

De auteurs hebben een systeem bedacht dat drie krachten combineert:

A. De Slimme Bibliothecaris (Analogieën)

Stel je voor dat je een lastig meetkundig probleem moet oplossen. In plaats van blind te gokken, roept de AI een slimme bibliothecaris aan.

• Wat doet hij? Hij kijkt naar jouw probleem en zoekt in een enorme bibliotheek naar andere problemen die er structuurtechnisch op lijken.
• Het voorbeeld: Als jij een probleem hebt over een driehoek met een hoek van 40 graden, zoekt hij een ander probleem met een driehoek en een hoek van 30 graden, maar met exact dezelfde logische opbouw.
• Het effect: De AI zegt: "Ah! Ik heb dit al eerder gezien! In dat andere geval gebruikten ze deze specifieke regels. Laten we die regels ook hier proberen." Dit helpt de AI om de juiste "startpositie" te kiezen in plaats van te raden.

B. De Strenge Controleur (De Verifier)

Nu heeft de AI een bewijs geschreven. Maar is het goed?

• De rol: Hier komt een strenge wiskundige controleur (een computerprogramma, geen mens) in beeld. Deze controleur kijkt niet naar de mooie zinnen, maar checkt elke stap als een logische puzzel.
• Het feedback-loop: Als de AI een fout maakt (bijvoorbeeld: "Ik gebruik deze regel, maar de voorwaarden zijn nog niet bewezen"), zegt de controleur: "Stop! Je bent te snel gegaan. Je hebt stap 2 nog niet bewezen, dus stap 3 mag niet."
• De cyclus: De AI krijgt dit bericht, past zijn bewijs aan en probeert het opnieuw. Dit gaat door totdat de controleur zegt: "Goed, dit klopt."

C. De "Neuro-Symbolische" Mix

• Neuro: De creatieve, mensachtige AI die de bewijzen schrijft.
• Symbolisch: De strenge, logische controleur die de feiten checkt.
  Samen vormen ze een team dat sterker is dan de som der delen.

3. Wat was het resultaat?

De auteurs hebben dit getest op honderden meetkundeproblemen (zoals die je op het SAT-examen in de VS ziet).

• Zonder hulp: De AI haalde het antwoord vaak niet of maakte veel fouten in de logica.
• Met hulp: Toen ze de "bibliothecaris" en de "controleur" inschakelden, steeg het succespercentage enorm.
  • Bij de slimste modellen (zoals OpenAI's o1) ging het succes van ongeveer 10% naar 80%.
  • Bij andere modellen zag men vergelijkbare enorme sprongen.

4. Waarom is dit belangrijk?

Stel je voor dat je een AI wilt gebruiken om medicijnen te ontwikkelen, bruggen te ontwerpen of veiligheidssoftware te schrijven. Je kunt het niet hebben dat de AI "misschien" het juiste antwoord geeft. Het moet 100% zeker zijn.

Dit paper laat zien dat we AI's niet hoeven te "herschrijven" om ze slim te maken. We hoeven ze alleen maar te koppelen aan:

1. Voorbeelden van soortgelijke problemen (om de weg te wijzen).
2. Een controlemechanisme dat de feiten checkt (om fouten te corrigeren).

Samenvattend in één zin:

Het is alsof je een creatieve student (de AI) laat studeren voor een examen door hem eerst te laten kijken naar de oplossingen van vergelijkbare oude examens (de analogieën), en hem vervolgens elke stap te laten controleren door een strenge leraar (de verifier) totdat het antwoord perfect is.

Dit maakt AI niet alleen slimmer, maar vooral betrouwbaarder voor taken waar fouten geen optie zijn.

Technische samenvatting

Hier is een gedetailleerde technische samenvatting van het paper "A Neuro-Symbolic Approach for Reliable Proof Generation with LLMs: A Case Study in Euclidean Geometry" in het Nederlands.

Probleemstelling

Grote Taalmodellen (LLMs) presteren uitstekend in veel taken, maar worstelen met formele domeinen die strenge logische deductie en symbolisch redeneren vereisen, zoals het genereren van wiskundige bewijzen. De architectuur van LLMs is gebaseerd op probabilistische sequentiegeneratie op basis van patronen in tekst, wat leidt tot gebrek aan absolute waarheid en ambiguïteit in wiskundige redenering. Bovendien vereisen bewijzen een langdurige logische coherentie en hiërarchisch redeneren, wat voor huidige modellen moeilijk is. Bestaande modellen neigen vaak naar patroonherkenning in plaats van echt wiskundig inzicht, wat resulteert in fouten bij zelfs kleine veranderingen in probleemstellingen.

Het paper stelt dat het mogelijk maken van LLMs om verifieerbare en rigoureuze bewijzen te genereren, essentieel is voor het verbeteren van betrouwbaarheid, nauwkeurigheid en consistentie, vooral voor veiligheidskritische toepassingen.

Methodologie: Een Neuro-Symbolische Aanpak

De auteurs introduceren een hybride systeem dat de generatieve kracht van LLMs combineert met twee gestructureerde, symbolische componenten: analoge gids en symbolische verificatie. Het systeem is getest op het FormalGeo-7k dataset, bestaande uit SAT-niveau Euclidische meetkundeproblemen.

Het proces verloopt in vier fasen:

1. Probleemabstractie:

   • Om oppervlakkige verschillen (zoals namen van lijnen of specifieke getallen) te negeren en de onderliggende structuur te benadrukken, worden alle problemen geabstraheerd. Entiteitsnamen worden vervangen door <word> en getallen door <num>.
   • Dit maakt het mogelijk om structureel vergelijkbare problemen te identificeren, ongeacht de specifieke oppervlakkige details.

2. Retrieval van Analogieën (Analogical Guidance):

   • Het systeem zoekt in de dataset naar problemen die structureel vergelijkbaar zijn met het doelprobleem. Dit wordt gedaan door de Jaccard-similariteit te berekenen over de abstracte representaties van constructie, voorwaarden en doel.
   • Een regressor (een simpel neuraal netwerk) is getraind om de waarschijnlijkheid van een vergelijkbaar bewijs te voorspellen op basis van de structuur van het probleem.
   • De top-k meest vergelijkbare problemen, inclusief hun volledige formele bewijzen, worden gebruikt als few-shot voorbeelden (in-context learning) voor de LLM.
   • Efficiëntie: In plaats van de volledige theorema-dictie (196 theorema's) aan de prompt toe te voegen, wordt de dictie beperkt tot alleen die theorema's die voorkomen in de bewijzen van de gevonden analogieën. Dit verkleint de zoekruimte en verlaagt de kosten aanzienlijk (van ~18k tokens naar ~2,5k tokens).

3. LLM Bewijsgeneratie:

   • De LLM (bijv. OpenAI o1 of Gemini-2.5-Flash) genereert een bewijs voor het doelprobleem, geleid door de analoge voorbeelden en de beperkte theorema-dictie. Het doel is om een formele reeks stappen te produceren die het doel afleiden uit de gegeven voorwaarden.

4. Symbolische Verificatie en Iteratieve Feedback:

   • Een externe symbolische verificador (gebaseerd op de Z3 Theorem Prover en SMT-oplossers) controleert het gegenereerde bewijs.
   • De verificador kent de oplossing niet vooraf; het controleert of het numerieke antwoord logisch volgt uit de in het bewijs gestelde constraints.
   • Foutencategorieën: De verificador identificeert drie soorten fouten en geeft gestructureerde feedback:
     1. Syntaxisfouten: Ongeldige theorema-aanroepen.
     2. Premisse-overtreding: Een theorema wordt aangeroepen zonder dat de vereiste voorwaarden eerder zijn bewezen.
     3. Doel niet bereikt: Het bewijs is syntactisch correct maar leidt niet tot het juiste doel of een inconsistent resultaat.
   • De feedback wordt teruggekoppeld naar de LLM, die het bewijs herbouwt. Dit proces herhaalt zich tot een geldig bewijs is gevonden of een maximum aantal pogingen is bereikt.

Belangrijkste Bijdragen

• Neuro-Symbolisch Systeem: Een nieuwe architectuur die LLMs ondersteunt bij bewijsgeneratie via analogie en verificatie.
• Gestructureerde Verificatie: Ontwerp van een verificador die het hele bewijs controleert (niet alleen het eindantwoord) en gedetailleerde feedback geeft.
• Kostenreductie: Door het gebruik van analogieën wordt de theorema-dictie dynamisch ingekrompen, wat de contextgrootte en API-kosten drastisch verlaagt.
• Openbare Beschikbaarheid: De code, data en evaluatiescripts worden vrijgegeven.

Resultaten

De methode werd geëvalueerd op 50 problemen (verdeeld over moeilijkheidsgraden 1-5) met de modellen OpenAI o1 en Gemini-2.5-Flash.

• Prestatieverbetering:
  • Voor OpenAI o1: De nauwkeurigheid steeg van 10% (basislijn) naar 80% met de volledige pijplijn (analogie + verificador + meerdere runs). Dit is een verbetering van 58%–70%.
  • Voor Gemini-2.5-Flash: De nauwkeurigheid steeg van 22% naar 86%, een verbetering van 52%–64%.
• Ablatiestudies:
  • Analogie: Het toevoegen van analoge voorbeelden alleen (zonder verificador) verbeterde de prestaties al aanzienlijk (van 10% naar 48% voor o1).
  • Verificatie: Iteratieve feedback door de verificador zorgde voor een extra stijging van ongeveer 20% in nauwkeurigheid.
  • Meerdere runs: Het toestaan van meerdere onafhankelijke pogingen hielp vooral bij moeilijkere problemen.
• Nauwkeurigheid vs. Antwoord: De basislijn vond vaak het juiste numerieke antwoord, maar kon dit niet onderbouwen met een correct bewijs. De voorgestelde methode verbeterde zowel de bewijsnauwkeurigheid als de kans op het vinden van het juiste numerieke antwoord (100% succes op antwoorden vs. 90% voor de basislijn).
• Efficiëntie: De methode vereist gemiddeld minder pogingen (retries) en runs dan de basislijn om tot een oplossing te komen.

Betekenis en Toekomstperspectief

Dit werk demonstreert dat neuro-symbolische methoden de betrouwbaarheid van LLMs in formele domeinen aanzienlijk kunnen verbeteren. Door de LLM te koppelen aan een symbolische verificador en gebruik te maken van analoge redenering, wordt het risico op hallucinaties en logische fouten geminimaliseerd.

• Toepassingen: De aanpak is veelbelovend voor wiskundeonderwijs (waar studenten feedback kunnen krijgen op hun bewijzen), wetenschappelijk onderzoek en veiligheidskritieke systemen waar correctheid cruciaal is.
• Beperkingen: Het systeem is momenteel beperkt tot Euclidische meetkunde en heeft geen toegang tot visuele diagrammen (hoewel multimodale modellen vaak slechter presteren op visuele aspecten van meetkundeproblemen). Ook ondersteunt de verificador nog geen inverse trigonometrische functies.
• Toekomst: De auteurs plannen uitbreiding naar andere domeinen, verbetering van de analogie-retrieval en integratie van meer geavanceerde verificatiemethoden (zoals model checking).

Concluderend biedt deze studie een schaalbaar blauwdruk voor het bouwen van betrouwbare AI-systemen in STEM-domeinen door de flexibiliteit van LLMs te combineren met de precisie van formele logica.