💻 computer science

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

This paper demonstrates that a neurosymbolic approach combining large language models with formal symbolic tools can successfully generate provably correct induction proofs for hardware verification, achieving an 84% success rate on mid-size open-source RTL designs.

Original authors: Romy Peled, Daniel Kroening, Michael Tautschnig, Yakir Vizel

Published 2026-05-04

📖 4 min read☕ Coffee break read

CC BY 4.0

Original authors: Romy Peled, Daniel Kroening, Michael Tautschnig, Yakir Vizel

Original paper licensed under CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ This is an AI-generated explanation of the paper below. It is not written or endorsed by the authors. For technical accuracy, refer to the original paper. Read full disclaimer

Imagine you are trying to prove that a complex machine (like a digital circuit in a computer chip) will never do something dangerous, like crashing or leaking data. In the world of hardware engineering, this is called Formal Verification.

Usually, proving this requires a human expert to write a mathematical "shield" (called an inductive invariant) that covers every possible state the machine could ever be in. It's like trying to write a rulebook that covers every single move a chess player could make, forever. This is incredibly hard, time-consuming, and often requires the human to invent clever "helper rules" (lemmas) to make the proof work.

This paper asks a simple question: Can an AI (specifically a Large Language Model or LLM) act as a "mining machine" to find these helper rules for us?

Here is the breakdown of their approach, using everyday analogies:

1. The Problem: The "Bit-Level" Wall

Current computer tools are like very diligent but short-sighted accountants. They check every single bit of data (0s and 1s) one by one. If the machine is huge, the accountant gets overwhelmed and gives up.
Human experts, however, think in "high-level concepts." They don't count every grain of sand; they see the shape of the beach. The authors wanted to see if an AI could learn to think like the human expert and generate those high-level helper rules.

2. The Solution: A "Neurosymbolic" Team

The authors didn't just ask the AI to "guess" the answer. They built a team with two distinct roles, like a Creative Writer and a Strict Editor.

The Creative Writer (The LLM): This is the AI. Its job is to brainstorm. It looks at the hardware design and the safety rule, then spits out a list of potential helper rules (lemmas).
- The Catch: The AI is creative but unreliable. Sometimes it writes brilliant rules; other times it writes nonsense, rules that don't make sense, or rules that are mathematically wrong. It "hallucinates."
The Strict Editor (The Formal Tool): This is a traditional, rigid computer program. It doesn't care about creativity; it only cares about truth. It takes the AI's list of rules and rigorously checks them. If a rule is even slightly wrong, the Editor rejects it. If a rule works, the Editor keeps it.

3. The Two Strategies

The team tried two different ways to organize this Writer-Editor relationship:

Strategy A: The "Batch" Approach (Non-Agentic)
Imagine asking the AI, "Give me 50 ideas for a helper rule," all at once. The AI writes 50 drafts. The Editor then goes through the pile, throwing away the bad ones and keeping the good ones to see if they solve the problem.
Strategy B: The "Conversation" Approach (Agentic)
This is more like a real dialogue. The AI suggests a rule. The Editor checks it and says, "No, that one is wrong because of X." The AI reads the feedback, learns from the mistake, and tries again. They keep looping back and forth until they find a rule that works. The paper found this "conversation" style was often more efficient.

4. The Results: Mining for Gold

The team tested this system on 110 different hardware designs (ranging from simple counters to complex memory systems).

The Success Rate: For 84% of the problems, their system successfully found a set of helper rules that proved the hardware was safe.
The "Hallucination" Issue: The AI generated thousands of rules. Many were garbage (syntax errors, logical fallacies). But because the "Strict Editor" was there to filter them out, the garbage didn't matter. The system only kept the gold.
Beating the Experts: They tested their system on the hardest problems that even the world's best commercial verification tools (the "super-accounts") failed to solve. Their AI-assisted approach managed to solve some of these "impossible" cases.

5. What This Means (and Doesn't Mean)

What it does: It automates the "mining" of the helper rules. It takes the heavy lifting of brainstorming mathematical lemmas away from human engineers.
What it doesn't do: It doesn't replace the human engineer entirely. The human still needs to set up the system and interpret the results. Also, the system currently needs the hardware code in a specific format (SystemVerilog); it can't work on the raw "blueprints" (netlists) that some older tools use.

In a nutshell: The authors built a system where an AI acts as a chaotic brainstorming partner, and a strict computer program acts as the quality control filter. Together, they can automatically generate the mathematical proofs needed to ensure hardware is safe, solving problems that were previously too difficult for standard tools to handle alone.

1. Problem Statement

Formal Verification (FV) is critical for ensuring the correctness of hardware designs (RTL). However, verifying complex industrial designs remains a bottleneck due to the "bit-level" nature of most model checking tools. These tools struggle to construct high-level, bit-agnostic mathematical proofs required for complex properties.

The standard approach to solving this is Proof by Induction, which requires auxiliary lemmas (inductive strengthenings) to prove a property. Currently, generating these lemmas is a manual, labor-intensive task performed by expert FV engineers. The paper addresses the question: Can Large Language Models (LLMs) automate the mining of these auxiliary lemmas to construct valid inductive arguments for hardware verification?

2. Methodology: A Neurosymbolic Approach

The authors propose a neurosymbolic framework that combines the generative capabilities of LLMs with the rigor of formal symbolic tools. The system does not rely solely on the LLM's output; instead, it uses the LLM to generate candidates and a formal solver to verify and filter them.

A. Core Components

LLM Prompting Frameworks: Two distinct strategies are used to generate candidate lemmas:
- Non-Agentic (Single Prompt): Uses a Few-Shot prompt containing $k$ examples of (RTL Design, Property, Inductive Lemmas) triples. The examples are selected via semantic similarity (using sentence transformers) from a pre-constructed Chain-of-Thought (CoT) pool. The LLM is sampled $n$ times with the same prompt to gather diverse candidates.
- Agentic (Iterative Interaction): Frames lemma generation as a loop. The LLM proposes lemmas, which are checked by the formal tool. If the check fails, the tool provides feedback (indicating which lemmas failed and why) and a "repair" message. The LLM then refines its suggestions in subsequent turns (up to 5 iterations).
Formal Reasoning Algorithm (FINDINDSTRENGTH):
- This algorithm takes the set of candidate lemmas generated by the LLM and attempts to find a subset that forms a valid Inductive Strengthening.
- Inductive Strengthening: A set of lemmas $L$ such that $L \land \text{Property}$ is an inductive invariant (satisfies initiation and consecution).
- Process:
  1. Filtering: Checks if individual lemmas are inductive invariants (using 1-induction) or hold up to a bounded depth (using Bounded Model Checking, BMC).
  2. Sorting: Prioritizes lemmas known to be inductive invariants over those that only hold within a bound.
  3. Subset Search: Iterates through prefixes of the sorted list to find the smallest subset that, when conjoined with the target property, forms a valid inductive invariant.
- Tooling: Implemented using EBMC (a formal verification tool) with $k$ -induction and BMC.

B. Dataset

The framework was evaluated on 110 verification tasks comprising:

58 SystemVerilog designs (from sources like VCEGAR, VIS, v2c, and custom FIFO/Arbiter/CAM designs).
47 C-program derived examples: C code translated into SystemVerilog Finite State Machines (FSMs) to test generalization.
CoT Pool: A small set of manually written examples used for few-shot prompting.

3. Key Contributions

Neurosymbolic Lemma Generation: Demonstrates the first use case of using LLMs specifically to mine auxiliary lemmas for constructing formal proofs in hardware verification.
Dual Prompting Framework: Implements and compares a static Few-Shot approach against an iterative Agentic approach, showing that the latter can steer the LLM away from incorrect paths.
Empirical Evaluation: Provides a comprehensive study on 110 tasks, highlighting that LLMs can successfully generate non-trivial inductive arguments for mid-size open-source RTL designs.
Handling Hallucinations: Proves that while LLMs hallucinate (producing syntactically invalid or logically incorrect lemmas), a formal filtering layer can effectively extract the correct proofs from the noise.

4. Experimental Results

The experiments were conducted on Amazon EC2 instances using six 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).

Success Rate: The framework successfully generated provably correct inductive arguments for 84% of the 110 verification tasks.
- Agentic Setup: Solved 92/110 examples (84% success rate).
- Non-Agentic Setup: Solved 84/110 examples (76% success rate).
Model Performance: Claude 4.5-Opus performed the best, solving 88 examples in the Agentic setup.
Comparison with SOTA Tools:
- The authors identified 31 "challenging" benchmarks where state-of-the-art industrial tools (JasperGold, VC-Formal, rIC3) failed to prove the property within a 10-minute timeout.
- The LLM-based approach solved instances that these SOTA tools could not, particularly in cases requiring complex inductive strengthenings (e.g., specific FIFO and Arbiter designs).
- In some cases where the LLM found the correct lemma but the formal check timed out, the result was still considered a success in terms of lemma generation, as the bottleneck was the verification tool's runtime, not the LLM's reasoning.
Error Analysis:
- LLMs occasionally hallucinated SVA syntax (e.g., invalid operators, undefined variables) or used non-ASCII characters.
- The Agentic setup was more efficient, often finding solutions with fewer total lemmas by iteratively refining the search space.

5. Significance and Impact

Industrial Value: This approach has the potential to significantly reduce the manual effort required by Formal Verification engineers. By automating the discovery of auxiliary lemmas, it lowers the barrier to applying formal methods to complex hardware designs.
Beyond Memorization: The results suggest that LLMs are performing genuine reasoning rather than simple memorization, as they successfully generalized to C-derived examples and handled variations in parameter instantiation and register naming.
Future Directions: The authors plan to extend the framework to handle multiple properties simultaneously, scale to larger industrial designs, and validate the approach in a real-world industrial setting.

Conclusion: The paper establishes that LLMs, when coupled with formal verification tools in a neurosymbolic loop, are a viable and powerful method for automating the most difficult part of hardware induction proofs: the discovery of auxiliary lemmas.