Towards Large Language Model Aided Program Refinement

TL;DR

This paper introduces LLM4PR, a tool that combines formal refinement techniques with large language models to automatically generate and verify correct code from specifications, enhancing automation and reliability.

Contribution

The paper presents a novel integration of formal refinement methods with LLMs, ensuring correctness in automatically generated code from informal specifications.

Findings

Successfully implemented with GPT-4, Coq, and Coqhammer.

Achieved automated code generation with correctness guarantees.

Evaluated on HumanEval and EvalPlus datasets.

Abstract

Program refinement involves correctness-preserving transformations from formal high-level specification statements into executable programs. Traditional verification tool support for program refinement is highly interactive and lacks automation. On the other hand, the emergence of large language models (LLMs) enables automatic code generations from informal natural language specifications. However, code generated by LLMs is often unreliable. Moreover, the opaque procedure from specification to code provided by LLM is an uncontrolled black box. We propose LLM4PR, a tool that combines formal program refinement techniques with informal LLM-based methods to (1) transform the specification to preconditions and postconditions, (2) automatically build prompts based on refinement calculus, (3) interact with LLM to generate code, and finally, (4) verify that the generated code satisfies the conditions of refinement calculus, thus guaranteeing the correctness of the code. We have implemented our tool using GPT4, Coq, and Coqhammer, and evaluated it on the HumanEval and EvalPlus datasets.