Abstract English: Large Language Models (LLMs) have shown potential in solving mathematical tasks, as demonstrated by their performance on Math Olympiad problems. Motivated by this, we study whether LLMs can be leveraged to generate proofs by induction for hardware verification.
Hardware verification is a challenging task that requires experienced formal verification (FV) engineers. One of the most useful techniques FV engineers use is proof by induction: they prove auxiliary lemmas such that, when used as assumptions, the property of interest becomes inductive, and hence manageable for automatic formal verification tools.
In this work, we show that LLMs can replicate some of this process by suggesting lemmas that help construct a proof by induction for hardware verification, indicating that the mathematical reasoning abilities of LLMs may hold industrial value.
We present a neurosymbolic approach that includes two prompting frameworks to generate candidate invariants, which are checked using a formal, symbolic tool. Our results indicate that with sufficient reprompting, LLMs are able to generate inductive arguments for mid-size open-source RTL designs. For 87% of our problem set, at least one of the prompt setups succeeded in producing a provably correct inductive argument.