Proof Strategy Extraction from LLMs for Enhancing Symbolic Provers

Dit paper introduceert Strat2Rocq, een methode die bewijsstrategieën uit grote taalmodellen extraheert en formaliseert als lemmata om het succespercentage van het symbolische bewijsinstrument CoqHammer te verhogen, terwijl deze lemmata ook de prestaties van taalmodel-agenten ten goede komen.

De kern

Stel je voor dat je een zeer slimme, maar soms wat onvoorspelbare kunstenaar hebt (de AI) en een zeer nauwkeurige, maar soms wat stijve architect (de traditionele bewijsmachine).

Deze paper, getiteld "Proof Strategy Extraction from LLMs for Enhancing Symbolic Provers", vertelt het verhaal van hoe we de creativiteit van de kunstenaar kunnen "stelen" om de architect slimmer te maken, zonder dat we de kunstenaar zelf nodig hebben om het werk te doen.

Hier is de uitleg in simpele taal:

1. Het Probleem: De Dure Kunstenaar vs. De Stijve Architect

In de wereld van softwareverificatie (het controleren of computerprogramma's veilig zijn) zijn er twee manieren om te werken:

• De Kunstenaar (LLM): Grote taalmodellen (zoals de AI die dit antwoord schrijft) zijn fantastisch in het bedenken van slimme oplossingen en patronen. Ze kunnen vaak direct zien waarom iets waar is. Maar ze zijn duur om te gebruiken, ze hebben veel stroom nodig, en als je geheimzinnige code hebt, wil je die niet naar een externe AI sturen (veiligheidsrisico).
• De Architect (Symbolische Prover): Dit zijn traditionele bewijsmachines (zoals CoqHammer). Ze zijn veilig, werken lokaal op je eigen computer en zijn heel betrouwbaar. Maar ze zijn soms "dom": ze missen de intuïtie. Ze kunnen een probleem niet oplossen omdat ze niet weten dat ze een bepaalde "trui" of "korte weg" moeten nemen, tenzij je het ze stap voor stap uitlegt.

De vraag van de onderzoekers: Kunnen we de "slimme trucs" van de Kunstenaar overnemen en ze in de hersenen van de Architect stoppen, zodat de Architect zelfstandig slimmer wordt?

2. De Oplossing: Strat2Rocq (De Vertaler)

De onderzoekers hebben een systeem bedacht dat ze Strat2Rocq noemen. Het werkt in twee fases, alsof je een geheim receptboek schrijft.

Fase 1: Het Leerproces (Offline)

Stel je voor dat je de Kunstenaar (de AI) vraagt om een moeilijk wiskundig probleem op te lossen.

1. De Kunstenaar schrijft een verhaal (een natuurlijke taal uitleg) over hoe het probleem opgelost wordt. "Eerst doe ik dit, dan zie ik dat dit hetzelfde is als dat..."
2. Het systeem leest dit verhaal en denkt: "Ah, deze Kunstenaar gebruikt een slimme truc hier!"
3. Het systeem vertaalt die slimme truc naar een wiskundige wet (een lemma) die de Architect precies begrijpt.
4. Dit gebeurt voor duizenden problemen. Het resultaat is een nieuwe wetboek vol met slimme trucs die de Kunstenaar kent, maar die nu in een taal zijn geschreven die de Architect kan lezen.

Analogie: Het is alsof je een meesterkok vraagt om een gerecht te koken. Jij kijkt toe, schrijft de "geheime ingrediënten" en "kooktechnieken" op, en zet ze in een receptenboek. Daarna hoef je de meesterkok niet meer uit te nodigen; je kunt zelf koken met zijn recepten.

Fase 2: Het Toepassen (Online)

Nu moet de Architect (CoqHammer) een nieuw, nog nooit eerder gezien probleem oplossen.

• Vroeger: De Architect keek in zijn oude, beperkte wetboek en zei: "Ik kan dit niet."
• Nu: De Architect opent het nieuwe receptenboek (de geëxtraheerde lemmas) dat vol staat met de slimme trucs van de Kunstenaar. Plotseling ziet hij: "Oh, ik ken deze truc! Als ik die toepas, is het probleem opgelost."

3. Wat leverde dit op?

De onderzoekers hebben dit getest op echte, open-source softwareprojecten (zoals een geverifieerde C-compiler).

• Resultaat: De Architect (CoqHammer) slaagde 13,41% vaker in het oplossen van problemen dan voorheen.
• Bijkomend voordeel: Zelfs de Kunstenaar (de AI-agent) werd beter als hij toegang had tot dit nieuwe receptenboek. Het bleek dat de trucs van de Kunstenaar ook voor de Kunstenaar zelf nuttig waren!

4. Waarom is dit belangrijk?

Dit is een game-changer voor drie redenen:

1. Veiligheid: Bedrijven hoeven hun geheime code niet meer naar een externe AI te sturen. Ze kunnen de slimme trucs lokaal gebruiken.
2. Kosten: Je hoeft geen dure AI-abonnementen te betalen voor elk bewijs. Je gebruikt een goedkope, lokale machine die nu slimmer is.
3. Begrip: Het helpt ons begrijpen hoe AI's eigenlijk "denken". Door hun trucs in wiskundige wetten te gieten, zien we precies welke patronen ze gebruiken.

Kort samengevat:
De onderzoekers hebben een manier gevonden om de "intuïtie" van een AI te vangen, te verpakken in een formeel wetboek, en die te geven aan een traditionele computer. Hierdoor wordt de computer slimmer, veiliger en goedkoper, zonder dat je de AI zelf hoeft in te zetten. Het is alsof je een genie zijn geheugenboek laat maken, zodat een gewone student (de computer) net zo slim kan presteren.

Technische samenvatting

Hier is een gedetailleerde technische samenvatting van het paper "Proof Strategy Extraction from LLMs for Enhancing Symbolic Provers" in het Nederlands.

Probleemstelling

Interactief bewijzen van stellingen (Interactive Theorem Proving - ITP) is een cruciale methode voor softwareverificatie, maar het schrijven van formele bewijzen vereist vaak aanzienlijke menselijke inspanning. Hoewel Large Language Models (LLMs) recentelijk sterke prestaties hebben geleverd in het automatiseren van bewijzen en traditionele symbolische bewijzers aanvullen, zijn er belangrijke beperkingen aan het gebruik van LLMs:

1. Kosten en Hardware: LLMs vereisen zware rekenkracht, wat ze ongeschikt maakt voor omgevingen met beperkte middelen (bijv. kleine veiligheidskritieke bedrijven).
2. Veiligheid: Veel bedrijven hebben vertrouwelijke codebases die niet naar externe LLM-diensten mogen worden gestuurd.
3. Afhankelijkheid: Pure symbolische bewijzers blijven daarom essentieel omdat ze kosteneffectief, veilig en lokaal uitvoerbaar zijn.

De kernvraag van dit onderzoek is: Kunnen we de interne bewijsstrategieën van LLMs extraheren om de capaciteiten van symbolische bewijzers te verbeteren?

Methodologie: Strat2Rocq

De auteurs introduceren Strat2Rocq, een raamwerk dat bewijsstrategieën uit LLMs haalt en deze formaliseert als lemmata in Rocq (de naam die in dit paper wordt gebruikt voor Coq/Rocq). Het proces verloopt in twee fasen:

Fase 1: Offline Lemma Mining (Extrahering)

In deze fase worden strategieën uit een trainingsset van stellingen gehaald zonder dat de LLM online betrokken is bij het daadwerkelijke bewijzen van nieuwe stellingen.

1. Generatie van Natuurlijke Taal (NL) Bewijzen: Voor elke stelling in de trainingsset vraagt het systeem de LLM om een stap-voor-stap bewijs in natuurlijke taal te genereren. Dit wordt gedaan omdat LLMs hierin vaak beter presteren dan in het direct genereren van formele code, en omdat de NL-stap de interne redenering van het model weerspiegelt.
2. Generalisatie en Formalisatie: De gegenereerde NL-bewijzen worden geanalyseerd. De LLM wordt gevraagd om specifieke inferentiestappen te generaliseren tot algemene lemmata en deze vervolgens te formaliseren in Rocq-code (autoformalisatie).
3. Validatie: Een "proof agent" (een iteratief proces) probeert de gegenereerde lemmata en hun bewijzen te valideren en fouten te herstellen. Alleen succesvol geverifieerde lemmata worden opgeslagen.

Fase 2: Online Stelling Bewijzen (Gebruik)

Wanneer een nieuwe stelling moet worden bewezen:

1. De geëxtraheerde lemmata worden toegevoegd aan de context van de nieuwe stelling.
2. Een pure symbolische bewijzer (CoqHammer, de state-of-the-art bewijzer voor Rocq) gebruikt deze extra lemmata om de stelling te bewijzen.
3. Belangrijk: De LLM wordt niet gebruikt tijdens het online bewijzen. De kennis is al ingebouwd in de vorm van lemmata. CoqHammer gebruikt zijn ingebouwde KNN-mechanisme om de meest relevante lemmata uit de uitgebreide context te selecteren.

Belangrijkste Bijdragen

1. Nieuw Onderzoeksveld: Het voorstellen van het probleem van het offline extraheren van bewijsstrategieën uit LLMs om symbolische bewijzers te versterken.
2. Strat2Rocq Framework: Een implementatie die LLM-genereren van natuurlijke taal bewijzen koppelt aan autoformalisatie, waardoor LLM-kennis in een voor symbolische bewijzers leesbare vorm (lemmata) wordt omgezet.
3. Empirische Validatie: Een uitgebreide evaluatie die aantoont dat deze methode de succesratio van bewijzen significant verhoogt, zowel voor symbolische bewijzers als voor LLM-agenten.

Resultaten

De evaluatie is uitgevoerd op open-source Rocq-projecten voor softwareverificatie (o.a. CompCert, Coq-Art, Ext-Lib, Vfa) met een dataset van 2.394 stellingen.

• Verbetering van Symbolische Bewijzers (CoqHammer):

  • Strat2Rocq verhoogde de succesratio van CoqHammer met gemiddeld 13,41%.
  • De verbetering was het grootst bij CompCert (een geverifieerde C-compiler), waar de succesratio met 17,75% steeg.
  • De methode helpt CoqHammer om complexe bewijzen te voltooien die normaal gesproken inductie vereisen (wat CoqHammer zelf niet ondersteunt) door deze te reduceren tot bestaande lemmata.

• Verbetering van LLM-Agenten:

  • De geëxtraheerde lemmata bleken ook nuttig voor LLM-proof agenten (die LLMs en bewijzers combineren).
  • De succesratio van een LLM-agent steeg met 4,00% wanneer de geëxtraheerde lemmata als context werden gebruikt.
  • Er werd een reductie in token-gebruik waargenomen, omdat CoqHammer meer stellingen onafhankelijk kon oplossen, waardoor minder LLM-calls nodig waren.

• Robuustheid:

  • De methode werkt met verschillende backend LLMs (getest met Claude 3.7 Sonnet en OpenAI o3-mini).
  • Het combineren van lemmata uit verschillende LLMs leverde nog betere resultaten op, wat suggereert dat hun interne strategieën elkaar aanvullen.
  • Een ablatiestudie toonde aan dat de stap van het genereren van een bewijs in natuurlijke taal essentieel is; zonder deze stap daalde het aantal geëxtraheerde lemmata met 63,56%.

Betekenis en Conclusie

Dit paper biedt een brug tussen twee werelden: de krachtige, maar dure en onzekere LLM's en de veilige, efficiënte symbolische bewijzers.

• Praktische Impact: Het stelt organisaties in staat om de "kennis" van geavanceerde LLM's te benutten voor softwareverificatie zonder afhankelijk te zijn van dure cloud-API's of blootstelling van vertrouwelijke code.
• Wetenschappelijke Impact: Het biedt een nieuwe manier om te begrijpen hoe LLMs formele bewijzen construeren. Door de interne strategieën van een LLM te vertalen naar een symbolisch model (lemmata), kunnen onderzoekers het "gedrag" van een LLM benaderen en analyseren binnen een deterministische omgeving.

Samenvattend bewijst Strat2Rocq dat het mogelijk is om de "black box" kennis van een LLM te distilleren naar een "witte doos" vorm (formele lemmata) die de prestaties van traditionele, veilige softwareverificatietools aanzienlijk verbetert.