# Towards Large Language Model Aided Program Refinement

arXiv: https://arxiv.org/abs/2406.18616 · HTML: https://mlsanity.com/paper/2406.18616/

## Key facts

- Cited by 2 papers in the map (data through 14 Oct 2026).
- Builds on 20 of its 45 references that are in the map.
- First posted on arXiv 26 Jun 2024.

## Builds on (most cited first, 20 of 20)

- [Chain-of-Thought Prompting Elicits Reasoning in Large Language Models](https://mlsanity.com/paper/2201.11903/) (2022)
- [Evaluating Large Language Models Trained on Code](https://mlsanity.com/paper/2107.03374/) (2021)
- [A Survey of Large Language Models](https://mlsanity.com/paper/2303.18223/) (2023)
- [Code Llama: Open Foundation Models for Code](https://mlsanity.com/paper/2308.12950/) (2023)
- [Is Your Code Generated by ChatGPT Really Correct? Rigorous Evaluation of Large Language Models for Code Generation](https://mlsanity.com/paper/2305.01210/) (2023)
- [LeanDojo: Theorem Proving with Retrieval-Augmented Language Models](https://mlsanity.com/paper/2306.15626/) (2023)
- [Generative Language Modeling for Automated Theorem Proving](https://mlsanity.com/paper/2009.03393/) (2020)
- [HyperTree Proof Search for Neural Theorem Proving](https://mlsanity.com/paper/2205.11491/) (2022)
- [Formal Mathematics Statement Curriculum Learning](https://mlsanity.com/paper/2202.01344/) (2022)
- [Proof Artifact Co-training for Theorem Proving with Language Models](https://mlsanity.com/paper/2102.06203/) (2021)
- [Thor: Wielding Hammers to Integrate Language Models and Automated Theorem Provers](https://mlsanity.com/paper/2205.10893/) (2022)
- [Cumulative Reasoning with Large Language Models](https://mlsanity.com/paper/2308.04371/) (2023)
- [From LLM to NMT: Advancing Low-Resource Machine Translation with Claude](https://mlsanity.com/paper/2404.13813/) (2024)
- [A New Era in Software Security: Towards Self-Healing Software via Large Language Models and Formal Verification](https://mlsanity.com/paper/2305.14752/) (2023)
- [Ranking LLM-Generated Loop Invariants for Program Verification](https://mlsanity.com/paper/2310.09342/) (2023)
- [A Static Evaluation of Code Completion by Large Language Models](https://mlsanity.com/paper/2306.03203/) (2023)
- [A Survey on Theorem Provers in Formal Methods](https://mlsanity.com/paper/1912.03028/) (2019)
- [The Refinement Calculus of Reactive Systems Toolset](https://mlsanity.com/paper/1710.08195/) (2017)
- [Differential Hoare Logics and Refinement Calculi for Hybrid Systems with Isabelle/HOL](https://mlsanity.com/paper/1910.13554/) (2019)
- [An Executable Structural Operational Formal Semantics for Python](https://mlsanity.com/paper/2109.03139/) (2021)

## Built on by (most cited first, 2 of 2)

- [MaCTG: Multi-Agent Collaborative Thought Graph for Automatic Programming](https://mlsanity.com/paper/2410.19245/) (2024)
- [Reasoning Under Threat: Symbolic and Neural Techniques for Cybersecurity Verification](https://mlsanity.com/paper/2503.22755/) (2025)

## Abstract (arXiv)

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.