LLM2SMT: Building an SMT Solver with Zero Human-Written Code

Dit paper presenteert LLM2SMT, een studie waarin een LLM-coderingsagent zonder enige menselijke code een complete SMT-oplosser voor QF_UF bouwt die concurrerend presteert op SMT-LIB-benchmarks.

De kern

Stel je voor dat je een meester-bakker bent, maar in plaats van zelf de cake te bakken, geef je een zeer slimme, maar soms wat slordige robot de instructies om een compleet bakkerijbedrijf op te zetten. En het gekke is: jij schrijft geen enkel recept. De robot doet het allemaal.

Dat is precies wat deze wetenschappelijke paper doet. De auteurs hebben een AI (een "Large Language Model" of LLM) gevraagd om een SMT-oplosser te bouwen. Dat klinkt als een ingewikkeld woord, maar laten we het zo uitleggen:

Wat is een SMT-oplosser? (De "Logische Detective")

Stel je voor dat je een enorme puzzel hebt met duizenden stukjes, waar sommige stukjes zeggen: "Als deze deur open is, moet die raam dicht zijn" en andere zeggen: "Deze sleutel past alleen in dit slot als het donker is." Een SMT-oplosser is een super-snel logisch detective die kijkt of er überhaupt een manier is om alle stukjes zo te leggen dat er geen tegenstrijdigheden ontstaan. Als het niet kan, zegt hij: "Onmogelijk!" en bewijst hij waarom.

Het Experiment: De Robot Bouwt de Detective

De onderzoekers (Mikoláš Janota en Mirek Olšák) wilden weten: Kan een AI software schrijven die zelf weer logische problemen oplost?

Ze gaven de AI een simpele opdracht: "Bouw een detective die logische puzzels oplost, maar schrijf zelf geen code."

• De AI: Gebruikte een model genaamd Claude.
• De Mensen: Schreven geen enkele regel code. Ze gaven alleen aanwijzingen, zoals "Gebruik deze grammatica" of "Kijk naar dit algoritme".
• Het Resultaat: De AI schreef een volledig werkend computerprogramma in C++.

De Strijd in de Keuken: Fouten en Oplossingen

Het ging niet allemaal van een leien dakje. De AI was slim, maar ook menselijk in zijn fouten:

1. De Vergeten Basis: De AI begon met een detective die alleen keek naar de inhoud, maar vergat hoe "en" en "of" werken. De onderzoekers moesten zeggen: "Hé, vergeet niet dat 'A en B' anders is dan 'A of B'."
2. De Eigen Uitvinding: De AI wilde een eigen, simpele "detective" bouwen in plaats van een bestaande, krachtige motor (CaDiCaL) te gebruiken. De onderzoekers moesten zeggen: "Gebruik die bestaande motor, die is sterker."
3. De Oneindige Loop: Soms bleef de AI hangen in een puzzel die te moeilijk was. De onderzoekers moesten een "stopknop" (time-out) toevoegen, zodat de AI niet urenlang bleef rekenen aan een onmogelijke taak.

De slimme truc: Toen de AI een fout maakte, lieten de onderzoekers hem niet zelf zoeken naar de fout. Ze gaven hem een "fuzzing"-tool (een robot die duizenden willekeurige, rare puzzels gooide) en een "delta-debugging"-tool (een robot die precies zocht waar het misging). Dit hielp de AI om zijn eigen fouten veel sneller te vinden dan als hij het "met de hand" had moeten doen.

De "Diamant"-Puzzel (De Preprocessing)

Er was een specifieke soort puzzel (de "equational diamond") waar de AI eerst vastliep. Het was als een doolhof waar je alle paden moet uitproberen.
De onderzoekers gaven de AI een hint: "Kijk naar de gemeenschappelijke delen in de paden."
De AI bedacht toen een slimme truc: Preprocessing.
Stel je voor dat je een doolhof hebt. In plaats van erin te rennen, kijkt de AI eerst naar de kaart en zegt: "Ah, als je links gaat, kom je hier uit. Als je rechts gaat, kom je ook hier uit. Laten we dat als een vast punt nemen." Hierdoor werd de puzzel in een flits opgelost.

Het Bewijs: De "Lean" Certificaat

Als de detective zegt "Dit is onmogelijk", moet hij dat kunnen bewijzen. De AI moest niet alleen de oplossing vinden, maar ook een wiskundig bewijs schrijven in een taal genaamd Lean (een taal voor wiskundigen om hun werk te verifiëren).
Dit was het moeilijkste deel. De AI dacht soms dat het bewijs klaar was, terwijl het nog gaten had. De onderzoekers moesten een voorbeeld geven van een perfect bewijs. Uiteindelijk lukte het: de AI schreef een bewijs dat door een onafhankelijke controleur (Lean) als correct werd goedgekeurd.

Het Eindresultaat

Hoe goed was deze door een AI gebouwde detective?

• Hij loste 7.468 van de bekende puzzels op.
• De beroemde, door mensen gemaakte detectives (zoals Z3 en CVC5) losten er iets meer op (rond de 7.500), maar de AI-detective deed het bijna net zo goed.
• En dat allemaal zonder dat een mens ook maar één regel code had geschreven!

De Les voor de Toekomst

De conclusie is: Ja, AI kan software schrijven die zelf redeneert. Maar het is geen magische toverstaf.

• Je moet de AI sturen (met duidelijke regels).
• Je moet hem laten testen (met tools die fouten opsporen).
• Je moet waken (want kleine foutjes kunnen grote problemen veroorzaken).

Het is alsof je een zeer getalenteerde leerling hebt die alles kan leren, maar die nog steeds een strenge meester nodig heeft om te voorkomen dat hij de verkeerde deur open doet. Maar als je die begeleiding geeft, kan die leerling een meesterwerk neerzetten waar zelfs de oude meesters trots op zouden zijn.

Technische samenvatting

Hier is een gedetailleerde technische samenvatting van het paper "LLM2SMT: Building an SMT Solver with Zero Human-Written Code" in het Nederlands.

Probleemstelling

De vraag of Large Language Models (LLM's) software kunnen schrijven die zelf redeneert, is een onderbelicht gebied binnen de AI-wetenschap. Hoewel LLM's al succesvol worden ingezet voor het genereren van code en het formaliseren van wiskundige bewijzen, is het onduidelijk of ze complexe, betrouwbare automatische redeneertools kunnen ontwikkelen. De uitdaging ligt in de complexiteit van SMT-oplossers (Satisfiability Modulo Theories): kleine fouten in de logica kunnen leiden tot subtiele, moeilijk op te sporen fouten die de correctheid van het hele systeem ondermijnen. Het paper onderzoekt of een LLM-agent, zonder dat er één regel code door een mens is geschreven, een functionele SMT-oplosser kan bouwen voor de theorie van ongedefinieerde functies zonder kwantoren (QF_UF).

Methodologie

Het onderzoek werd uitgevoerd met een LLM-coderingsagent (Claude Code met het Sonnet 4.6-model) die een volledig project initieerde en uitvoerde.

1. Architectuur en Implementatie:

   • De agent schreef de oplossing in C++20 met gebruik van CMake voor build-automatisering.
   • De parser werd gegenereerd met ANTLR op basis van de SMT-LIB v2-grammatica.
   • Voor de SAT-kern werd de agent eerst geprobeerd een eigen rudimentaire solver te schrijven, maar werd later aangestuurd om CaDiCaL te integreren via de IPASIR-UP interface.
   • De theorie-oplosser implementeert het Nieuwenhuis-Oliveras congruentie-sluitingsalgoritme (congruence closure) voor de theorie van gelijkheid met ongedefinieerde functies (QF-EUF).
   • Het systeem ondersteunt het genereren van bewijzen in Lean, een interactief bewijssysteem.

2. Ontwikkelproces en Debugging:

   • Zero Human-Code: Geen mens schreef code; menselijke interventie beperkte zich tot het geven van prompts, het instellen van randvoorwaarden (zoals time-outs) en het evalueren van resultaten.
   • Foutoplossing: De agent corrigeerde fouten autonoom wanneer deze werden gepresenteerd met inputbestanden die tot verkeerde antwoorden leidden.
   • Geavanceerde Testtechnieken: Om de agent te helpen bij het vinden van bugs, werden fuzzing (willekeurige formulegeneratie) en delta-debugging (differentiële testing tegen een referentie-oplosser) geïmplementeerd. Dit verminderde de token-gebruikskosten en verhoogde de efficiëntie.
   • Preprocessing: De agent ontwikkelde een preprocessing-techniek om "equational diamond"-problemen (combinatorische explosie in disjuncties) op te lossen door gemeenschappelijke consequenties van takken te extraheren en als unit-equalities toe te voegen.

3. Certificatie (Bewijsgeneratie):

   • Voor satisfiable formules werd het gegenereerde model geverifieerd door het terug te coderen als SMT-probleem.
   • Voor unsatisfiable formules moest de agent een bewijs in Lean genereren. Dit vereiste een specifieke architectuur: theorema's voor theorema-lemmata (opgelost met grind) en een hoofdbewijs voor de propositional fragment (opgelost met bv_decide).

Belangrijkste Bijdragen

• Eerste volledig gegenereerde SMT-oplosser: Dit is een case study waarin een complete DPLL(T)-stijl SMT-oplosser voor QF_UF is gebouwd zonder menselijke code.
• Validatie van LLM-vaardigheden: Het bewijst dat LLM's complexe algoritmen (zoals congruentie-sluiting) kunnen implementeren en kunnen debuggen, mits ze worden ondersteund door gestructureerde feedback en testtools.
• Preprocessing-innovatie: De agent bedacht zelf een effectieve preprocessing-methode voor een specifiek type benchmarkprobleem (equational diamonds) dat standaard DPLL(T)-oplossers vaak vertraagt.
• Lean-integratie: Het systeem is in staat om interne redeneringen om te zetten in formeel verifieerbare Lean-bewijzen, hoewel dit de grootste uitdaging bleek.

Resultaten

De prestaties werden getest op de SMT-LIB benchmarks (QF_UF) en vergeleken met gevestigde oplossers zoals z3 en cvc5.

• Oplossingscapaciteit: De LLM2SMT-oplosser loste 7.468 van de 7.500+ instances op.
  • Vergelijking: z3 loste 7.500 op, cvc5 7.494. De LLM-oplosser is dus concurrerend, hoewel iets minder robuust dan de volwassen referenties.
• Snelheid: De versie zonder theorie-propagatie presteerde verrassend goed, soms zelfs sneller dan de versie met propagatie op deze specifieke benchmarks, wat suggereert dat propagatie-overhead op sommige problemen niet lonend is.
• Certificatie: Van de 285 geverifieerde instances (met preprocessing) faalde Lean bij 2.244 gevallen (voornamelijk door time-outs of stack-overflow in Lean zelf), maar geen enkel onjuist bewijs werd gevonden. Dit bevestigt de correctheid van de gegenereerde logica, zelfs als de bewijsgeneratie niet altijd succesvol was.

Betekenis en Conclusie

Het paper concludeert dat het antwoord op de vraag "Kunnen LLM's automatische redeneertools ontwikkelen?" een kwalificerend "ja" is.

• Succesfactoren: Systematische fuzzing, delta-debugging, expliciete resource-limieten (time-outs) en zorgvuldige specificatie van de invoertaal zijn essentieel. Zonder deze "scaffolding" (ondersteuning) faalt de agent vaak op triviale maar kritieke fouten (zoals het niet onderscheiden van Boolese termen en proposities).
• Beperkingen:
  • Correctheid: Correctheid kan niet worden aangenomen; de agent heeft constante menselijke begeleiding en concrete voorbeelden nodig om subtiele logica-fouten te corrigeren.
  • Bewijsgeneratie: Het genereren van bewijzen bleek de moeilijkste taak. De agent had moeite om de complexiteit van het bewijssysteem (Lean) te begrijpen en vereiste menselijke voorbeelden om de juiste structuur voor theorema's en axioma's te hanteren.
• Toekomst: De studie toont aan dat LLM's potentieel hebben om nieuwe redeneertools te bouwen en technieken uit wetenschappelijke literatuur te implementeren, maar dat menselijke supervisie cruciaal blijft voor het garanderen van robuustheid en correctheid in kritieke systemen.