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

Peled, Romy; Kroening, Daniel; Tautschnig, Michael; Vizel, Yakir

doi:10.24963/ijcai.2026/444

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

Romy Peled, Daniel Kroening, Michael Tautschnig, Yakir Vizel

Download BibTeX Cite

Proceedings of the Thirty-Fifth International Joint Conference on Artificial Intelligence. Main Track. Pages 3988-3998.

https://doi.org/10.24963/ijcai.2026/444

Keywords

Natural Language Processing: Language models
Natural Language Processing: Applications
Knowledge Representation and Reasoning: Automated reasoning and theorem proving

Abstract

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 %alleviating some of the manual effort

done by Formal Verification engineers and deliver value to industry.

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

90% of our problem set, at least one of the prompt setups succeeded in producing a provably correct inductive argument.

Romy Peled, Daniel Kroening, Michael Tautschnig, and Yakir Vizel. 2026. Large Lemma Miners: Can LLMs Do Induction Proofs for Hardware?. In Proceedings of the Thirty-Fifth International Joint Conference on Artificial Intelligence, IJCAI-26. IJCAI, 3988–3998. https://doi.org/10.24963/ijcai.2026/444

@inproceedings{ijcai2026p444,
  title     = {Large Lemma Miners: Can LLMs Do Induction Proofs for Hardware?},
  author    = {Peled, Romy and Kroening, Daniel and Tautschnig, Michael and Vizel, Yakir},
  booktitle = {Proceedings of the Thirty-Fifth International Joint Conference on
               Artificial Intelligence, {IJCAI-26}},
  publisher = {International Joint Conferences on Artificial Intelligence Organization},
  editor    = {Diego Calvanese},
  pages     = {3988--3998},
  year      = {2026},
  month     = {8},
  note      = {Main Track},
  doi       = {10.24963/ijcai.2026/444},
  url       = {https://doi.org/10.24963/ijcai.2026/444},
}

TY  - CPAPER
TI  - Large Lemma Miners: Can LLMs Do Induction Proofs for Hardware?
AU  - Peled, Romy
AU  - Kroening, Daniel
AU  - Tautschnig, Michael
AU  - Vizel, Yakir
T2  - Proceedings of the Thirty-Fifth International Joint Conference on Artificial Intelligence, IJCAI-26
PB  - International Joint Conferences on Artificial Intelligence Organization
PY  - 2026
SP  - 3988
EP  - 3998
DO  - 10.24963/ijcai.2026/444
UR  - https://doi.org/10.24963/ijcai.2026/444
ER  -