Cobblestone: A Divide-and-Conquer Approach for Automating Formal Verification

Probleemstelling

Formele verificatie met bewijsassistenten zoals Coq is een krachtige methode om softwarekwaliteit te garanderen en bugs wiskundig uit te sluiten. Echter, het handmatig schrijven van deze bewijzen vereist aanzienlijke expertise en tijd. Hoewel machine learning (ML) en grote taalmodellen (LLM's) zijn ingezet om bewijzen automatisch te synthetiseren, lopen bestaande benaderingen tegen beperkingen aan:

1. Hele bewijzen genereren: Benaderingen die proberen een volledig bewijs in één keer te genereren (zonder gebruik te maken van tussentijdse staten), missen vaak de context die nodig is voor complexe redenering.
2. Tactiek-voor-tactiek zoeken: Benaderingen die stap voor stap een bewijs opbouwen, worstelen met de complexe zoekruimte omdat ze lokaal geoptimaliseerd zijn zonder een hoog niveau bewijsplan.
3. Onzekerheid van LLM's: LLM's kunnen onjuiste bewijzen genereren. Bestaande tools falen vaak omdat ze niet effectief kunnen omgaan met fouten in een gedeeltelijk bewijs of niet weten hoe ze een mislukte poging moeten herstructureren.

Methodologie: Cobblestone

Cobblestone is een nieuw, op LLM's gebaseerd systeem dat een "divide-and-conquer" (verdelings- en veroverings) strategie hanteert om de voordelen van het genereren van hele bewijzen te combineren met de precisie van lokale exploratie. Het systeem is volledig geautomatiseerd, maar kan ook externe input gebruiken.

De kerncomponenten van de methode zijn:

1. Divide-and-Conquer Strategie:

   • In plaats van te proberen het oorspronkelijke doel direct te bewijzen, probeert Cobblestone eerst een volledig bewijs te genereren.
   • Als dit faalt, analyseert het de structuur van het bewijs om te bepalen welke subdoelen (subgoals) wel en welke niet zijn bewezen.
   • Het systeem behoudt de correcte delen van het bewijs en rekurseert (roept zichzelf recursief op) alleen voor de mislukte subdoelen. Hierdoor wordt het probleem opgesplitst in kleinere, beheersbare stukken die makkelijker te bewijzen zijn.

2. Fail-Safe Mode (Veilige Uitvoering):

   • Dit is een innovatieve methode om gegenereerde bewijzen uit te voeren in Coq. In tegenstelling tot standaard uitvoering die stopt bij de eerste fout, voert Fail-Safe Mode het bewijs uit door de bewijsstructuur (prefixen en subbewijzen met bullets) te traverseren.
   • Bij een fout wordt het resterende deel van dat specifieke subbewijs tijdelijk vervangen door een admit (een tijdelijke acceptatie van een niet-bewezen doel).
   • Hierdoor kan het systeem identificeren welke delen van het bewijs correct zijn ("correct") en welke delen mislukken ("in progress"), zelfs als er fouten in het midden van het script staan.

3. Integratie van CoqHammer:

   • Cobblestone combineert neurale bewijssynthese met SMT-oplossers via CoqHammer.
   • Het gebruikt CoqHammer zowel op het initiële doel als op de gereduceerde subdoelen tijdens de recursieve calls. Omdat kleinere subdoelen vaak eenvoudiger zijn, is de kans dat een SMT-oplosser succes heeft groter dan bij het oorspronkelijke complexe doel.

4. LLM Sampling:

   • Het systeem gebruikt een instructie-tuned LLM (zoals GPT-4) om kandidaat-bewijzen te genereren.
   • Het gebruikt diverse prompts (met en zonder context, met en zonder "Chain-of-Thought" redenering) om variatie in de gegenereerde bewijzen te creëren.
   • Het systeem selecteert vervolgens de beste fragmenten uit meerdere pogingen om een volledig correct bewijs te assembleren.

Belangrijkste Bijdragen

1. Cobblestone: Een nieuw bewijssynthese-approach dat een middenweg vormt tussen het genereren van hele bewijzen en tactiek-voor-tactiek zoeken, door gebruik te maken van gedeeltelijke successen van mislukte bewijzen.
2. Fail-Safe Mode: Een nieuwe methode om bewijzen uit te voeren die fouten lokaliseert en correcte delen isoleert, waardoor het systeem kan hergebruiken wat wel werkt.
3. Uitgebreide Evaluatie: Een evaluatie op vier benchmarks (CoqGym, coq-wigderson, coq-bb5, PnVRocqLib) met strikte controle op data-lekkage (gebruik van projecten die na de training van GPT-4 zijn gepubliceerd).
4. Externe Input: Onderzoek naar hoe externe input (zoals relevante lemmata of een bewijsstructuur van een mens) de prestaties kan verbeteren, wat een pad naar semi-automatische verificatie aangeeft.

Resultaten

Cobblestone werd geëvalueerd op 400 theorema's (100 per benchmark) en vergeleken met state-of-the-art tools zoals Proverbot9001, CoqHammer, PALM en Rango.

• Prestaties: Cobblestone bewees 48% van de theorema's in de CoqGym-benchmark en 38% in de Wigderson-benchmark. Dit is significant hoger dan bestaande niet-LLM tools (CoqHammer: ~30%, Proverbot9001: ~17%) en ook hoger dan andere LLM-baselines.
• Complementariteit: Cobblestone bewijst veel theorema's die andere tools niet kunnen bewijzen. De combinatie van Cobblestone met andere tools (zoals PALM) leidt tot een aanzienlijk hoger totaal aantal bewezen theorema's (bijv. 63% op CoqGym100).
• Efficiëntie: Gemiddeld kost een Cobblestone-run $1.25 en duurt 14,7 minuten.
• Invloed van Externe Input: Met "orakels" (perfecte kennis van relevante lemmata of bewijsopbouw) kon Cobblestone tot 58% van de theorema's bewijzen.
• LLM-onafhankelijkheid: Het systeem werkt met verschillende modellen (GPT-4, GPT-3.5, Claude 3 Opus) en presteert consistent beter dan baselines op elk model.

Betekenis en Conclusie

Dit paper toont aan dat formele verificatie kan worden geautomatiseerd door slimme strategieën te gebruiken die de beperkingen van LLM's omzeilen. In plaats van te vertrouwen op één perfecte generatie, gebruikt Cobblestone de "ruis" van mislukte pogingen om de zoekruimte te verkleinen.

De belangrijkste inzichten zijn:

• Het gebruik van gedeeltelijke voortgang (het behouden van correcte subbewijzen) is cruciaal voor succes.
• Het combineren van LLM's met traditionele SMT-oplossers (hammers) in een recursieve structuur levert betere resultaten op dan het gebruik van een van beide alleen.
• Externe input (van mensen of andere tools) kan de prestaties drastisch verbeteren, wat suggereert dat de toekomst van formele verificatie ligt in interactieve, semi-automatische systemen waarbij mens en machine samenwerken.

Cobblestone biedt een schaalbare, kosteneffectieve en reproduceerbare aanpak die de drempel voor formele verificatie in de software-engineering verlaagt.