<ul><li>Formally verifying properties of software code, especially with the emergence of LLM-generated code, is a highly desirable task.</li><li>This work introduces a framework that generates whole proofs in a formal language to be used in systems utilizing built-in tactics and automated theorem provers.</li><li>The framework includes components for generating natural language statements, an LLM that generates formal proofs, and a module employing heuristics for building the final proof.</li><li>The framework is validated using benchmark tests and the Isabelle proof assistant, and a dataset is curated for future training tasks.</li></ul>

Neural Theorem Proving: Generating and Structuring Proofs for Formal Verification

Discover more