Large Lemma Miners: Can LLMs do Induction Proofs for Hardware?

1. Probleemstelling

Formele verificatie (FV) is cruciaal voor het waarborgen van de correctheid van hardwareontwerpen (RTL). Het verifiëren van complexe industriële ontwerpen blijft echter een knelpunt vanwege het "bit-niveau"-karakter van de meeste model-checking tools. Deze tools hebben moeite om hoog-niveau, bit-agnostische wiskundige bewijzen te construeren die vereist zijn voor complexe eigenschappen.

De standaardaanpak om dit op te lossen is bewijs door induktie, wat auxiliaire lemma's (induktieve versterkingen) vereist om een eigenschap te bewijzen. Het genereren van deze lemma's is momenteel een handmatige, arbeidsintensieve taak die wordt uitgevoerd door expert FV-engineers. Het artikel adresseert de vraag: Kunnen Large Language Models (LLMs) het minen van deze auxiliaire lemma's automatiseren om geldige induktieve argumenten te construeren voor hardwareverificatie?

2. Methodologie: Een Neurosymbolische Aanpak

De auteurs stellen een neurosymbolisch raamwerk voor dat de generatieve capaciteiten van LLMs combineert met de striktheid van formele symbolische tools. Het systeem vertrouwt niet uitsluitend op de output van de LLM; in plaats daarvan gebruikt het de LLM om kandidaten te genereren en een formele solver om deze te verifiëren en te filteren.

A. Kerncomponenten

1. LLM Prompting Frameworks: Er worden twee verschillende strategieën gebruikt om kandidaat-lemma's te genereren:

   • Non-Agentic (Enkele Prompt): Gebruikt een Few-Shot prompt met $k$ voorbeelden van (RTL-ontwerp, Eigenschap, Induktieve Lemma's) triples. De voorbeelden worden geselecteerd via semantische gelijkenis (met behulp van sentence transformers) uit een vooraf geconstrueerde Chain-of-Thought (CoT) pool. De LLM wordt $n$ keer bemonsterd met dezelfde prompt om diverse kandidaten te verzamelen.
   • Agentic (Iteratieve Interactie): Framing van lemma-generatie als een lus. De LLM stelt lemma's voor, die worden gecontroleerd door de formele tool. Als de controle faalt, levert de tool feedback (aangevend welke lemma's faalden en waarom) en een "reparatie"-bericht. De LLM verfijnt vervolgens zijn suggesties in volgende beurten (tot 5 iteraties).

2. Formeel Redeneringsalgoritme (FINDINDSTRENGTH):

   • Dit algoritme neemt de set kandidaat-lemma's die door de LLM zijn gegenereerd en probeert een subset te vinden die een geldige Induktieve Versterking vormt.
   • Induktieve Versterking: Een set lemma's $L$ zodanig dat $L \land \text{Eigenschap}$ een induktieve invariant is (voldoet aan initiatie en consecutie).
   • Proces:
     1. Filtering: Controleert of individuele lemma's induktieve invarianten zijn (met behulp van 1-induktie) of gelden tot een gebonden diepte (met behulp van Bounded Model Checking, BMC).
     2. Sortering: Prioriteert lemma's die bekend staan als induktieve invarianten boven die welke alleen binnen een grens gelden.
     3. Subset Search: Itereert door prefixes van de gesorteerde lijst om de kleinste subset te vinden die, wanneer geconjungeerd met de doeleigenschap, een geldige induktieve invariant vormt.
   • Tooling: Geïmplementeerd met EBMC (een formele verificatietool) met $k$-induktie en BMC.

B. Dataset

Het raamwerk werd geëvalueerd op 110 verificatietaken bestaande uit:

• 58 SystemVerilog-ontwerpen (uit bronnen zoals VCEGAR, VIS, v2c en aangepaste FIFO/Arbiter/CAM-ontwerpen).
• 47 uit C-programma's afgeleide voorbeelden: C-code vertaald naar SystemVerilog Finite State Machines (FSMs) om generalisatie te testen.
• CoT Pool: Een kleine set handgeschreven voorbeelden gebruikt voor few-shot prompting.

3. Belangrijkste Bijdragen

1. Neurosymbolische Lemma-Generatie: Demonstreert het eerste gebruiksscenario van het gebruik van LLMs specifiek om auxiliaire lemma's te minen voor het construeren van formele bewijzen in hardwareverificatie.
2. Dual Prompting Framework: Implementeert en vergelijkt een statische Few-Shot-aanpak met een iteratieve Agentic-aanpak, waarbij blijkt dat de laatste de LLM kan sturen weg van onjuiste paden.
3. Empirische Evaluatie: Biedt een uitgebreide studie over 110 taken, waarbij wordt benadrukt dat LLMs succesvol niet-triviale induktieve argumenten kunnen genereren voor mid-size open-source RTL-ontwerpen.
4. Omgaan met Hallucinaties: Bewijst dat hoewel LLMs hallucineren (het produceren van syntactisch ongeldige of logisch onjuiste lemma's), een formele filterlaag effectief de juiste bewijzen uit de ruis kan halen.

4. Experimentele Resultaten

De experimenten werden uitgevoerd op Amazon EC2-instanties met zes state-of-the-art LLMs (GPT-5, Claude 3.7, Claude 4 Sonnet, Claude 4.5 Sonnet, Claude 4.5 Haiku, Claude 4.5 Opus).

• Succespercentage: Het raamwerk genereerde succesvol bewijsbaar correcte induktieve argumenten voor 84% van de 110 verificatietaken.
  • Agentic Setup: Loste 92/110 voorbeelden op (84% succespercentage).
  • Non-Agentic Setup: Loste 84/110 voorbeelden op (76% succespercentage).
• Modelprestaties: Claude 4.5-Opus presteerde het beste en loste 88 voorbeelden op in de Agentic setup.
• Vergelijking met SOTA-tools:
  • De auteurs identificeerden 31 "uitdagende" benchmarks waar state-of-the-art industriële tools (JasperGold, VC-Formal, rIC3) faalden om de eigenschap binnen een time-out van 10 minuten te bewijzen.
  • De op LLM gebaseerde aanpak loste instanties op die deze SOTA-tools niet konden, met name in gevallen die complexe induktieve versterkingen vereisten (bijv. specifieke FIFO- en Arbiter-ontwerpen).
  • In sommige gevallen waarin de LLM het juiste lemma vond maar de formele controle time-out kreeg, werd het resultaat toch beschouwd als een succes qua lemma-generatie, aangezien het knelpunt de runtime van de verificatietool was en niet het redeneren van de LLM.
• Foutanalyse:
  • LLMs hallucineerden af en toe SVA-syntax (bijv. ongeldige operators, niet-gedefinieerde variabelen) of gebruikten niet-ASCII karakters.
  • De Agentic setup was efficiënter, vaak oplossingen vindend met minder totale lemma's door iteratief het zoekruimte te verfijnen.

5. Betekenis en Impact

• Industriële Waarde: Deze aanpak heeft het potentieel om de handmatige inspanning die vereist is door Formal Verification-engineers aanzienlijk te verminderen. Door het ontdekken van auxiliaire lemma's te automatiseren, verlaagt het de drempel voor het toepassen van formele methoden op complexe hardwareontwerpen.
• Voorbij Memoriseren: De resultaten suggereren dat LLMs echte redenering uitvoeren in plaats van eenvoudig memoriseren, aangezien ze succesvol generaliseerden naar uit C afgeleide voorbeelden en omgingen met variaties in parameter-instantiatie en register-naming.
• Toekomstige Richtingen: De auteurs plannen het raamwerk uit te breiden om meerdere eigenschappen simultaan te behandelen, te schalen naar grotere industriële ontwerpen en de aanpak te valideren in een echte industriële setting.

Conclusie: Het artikel stelt vast dat LLMs, wanneer gekoppeld aan formele verificatietools in een neurosymbolische lus, een levensvatbare en krachtige methode zijn voor het automatiseren van het moeilijkste deel van hardware-induktiebewijzen: het ontdekken van auxiliaire lemma's.