Towards LLM-based Generation of Human-Readable Proofs in Polynomial Formal Verification
Fuente:
arXiv
Saved in:
| Main Author: | |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866918038033399808 |
|---|---|
| author | Drechsler, Rolf |
| author_facet | Drechsler, Rolf |
| contents | Verification is one of the central tasks in circuit and system design. While simulation and emulation are widely used, complete correctness can only be ensured based on formal proof techniques. But these approaches often have very high run time and memory requirements. Recently, Polynomial Formal Verification (PFV) has been introduced showing that for many instances of practical relevance upper bounds on needed resources can be given. But proofs have to be provided that are human-readable.
Here, we study how modern approaches from Artificial Intelligence (AI) based on Large Language Models (LLMs) can be used to generate proofs that later on can be validated based on reasoning engines. Examples are given that show how LLMs can interact with proof engines, and directions for future work are outlined. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2505_23311 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Towards LLM-based Generation of Human-Readable Proofs in Polynomial Formal Verification Drechsler, Rolf Logic in Computer Science Hardware Architecture Symbolic Computation 68W30, 68M07, 68W35 B.2.1; B.6.3; F.2.2 Verification is one of the central tasks in circuit and system design. While simulation and emulation are widely used, complete correctness can only be ensured based on formal proof techniques. But these approaches often have very high run time and memory requirements. Recently, Polynomial Formal Verification (PFV) has been introduced showing that for many instances of practical relevance upper bounds on needed resources can be given. But proofs have to be provided that are human-readable. Here, we study how modern approaches from Artificial Intelligence (AI) based on Large Language Models (LLMs) can be used to generate proofs that later on can be validated based on reasoning engines. Examples are given that show how LLMs can interact with proof engines, and directions for future work are outlined. |
| title | Towards LLM-based Generation of Human-Readable Proofs in Polynomial Formal Verification |
| topic | Logic in Computer Science Hardware Architecture Symbolic Computation 68W30, 68M07, 68W35 B.2.1; B.6.3; F.2.2 |
| url | https://arxiv.org/abs/2505.23311 |