Towards LLM-based Generation of Human-Readable Proofs in Polynomial Formal Verification

TL;DR

This paper explores using Large Language Models to generate human-readable proofs in Polynomial Formal Verification, aiming to improve proof accessibility and integration with reasoning engines in circuit verification.

Contribution

It introduces a novel approach of leveraging LLMs to produce understandable proofs for PFV, facilitating validation and future AI-assisted formal verification workflows.

Findings

LLMs can generate human-readable proofs for PFV

Proofs can be validated by reasoning engines

Interaction between LLMs and proof engines is feasible

Abstract

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.