Saved in:
| Main Authors: | , , , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | https://arxiv.org/abs/2511.02521 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866910183777632256 |
|---|---|
| author | Peled, Romy Kroening, Daniel Tautschnig, Michael Vizel, Yakir |
| author_facet | Peled, Romy Kroening, Daniel Tautschnig, Michael Vizel, Yakir |
| contents | Large Language Models (LLMs) have shown potential for solving mathematical tasks. We show that LLMs can be utilized to generate proofs by induction for hardware verification and thereby replace some of the manual work done by Formal Verification engineers and deliver 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 84% of our problem set, at least one of the prompt setups succeeded in producing a provably correct inductive argument. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2511_02521 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Large Lemma Miners: Can LLMs do Induction Proofs for Hardware? Peled, Romy Kroening, Daniel Tautschnig, Michael Vizel, Yakir Logic in Computer Science Large Language Models (LLMs) have shown potential for solving mathematical tasks. We show that LLMs can be utilized to generate proofs by induction for hardware verification and thereby replace some of the manual work done by Formal Verification engineers and deliver 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 84% of our problem set, at least one of the prompt setups succeeded in producing a provably correct inductive argument. |
| title | Large Lemma Miners: Can LLMs do Induction Proofs for Hardware? |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2511.02521 |