一句话：提出 Refine4LLM，用精化演算自动引导并验证 LLM 生成代码，在保证正确性的同时提升自动化程度。
以 Copilot 为代表的代码大语言模型降低了编程门槛，但其生成代码缺乏正确性保证，存在幻觉风险，且从规约到代码的端到端过程是不透明、不可控的黑箱，难以取信于用户。传统程序精化能把高层规约语句逐步变换为可执行代码并保持正确性，但相关工具主要面向形式方法专家，缺乏自动化与可扩展性。为此作者提出 Refine4LLM：对规约进行形式精化，借助精化演算自动提示并引导 LLM 交互式生成代码，再验证生成代码满足约束以保证正确性，同时从过程中学习并构建更高级的精化法则以扩展精化演算。在程序精化与 LLM 基准上的实验表明，该方法相较最先进基线能更高效地生成更鲁棒的代码，并减少精化与验证所需时间。
Recently, the rise of code-centric Large Language Models (LLMs) has reshaped the software engineering world with low-barrier tools like Copilot that can easily generate code. However, there is no correctness guarantee for the code generated by LLMs, which suffer from the hallucination problem, and their output is fraught with risks. Besides, the end-to-end process from specification to code through LLMs is a non-transparent and uncontrolled black box. This opacity makes it difficult for users to understand and trust the generated code. Addressing these challenges is both necessary and critical. In contrast, program refinement transforms high-level specification statements into executable code while preserving correctness. Traditional tools for program refinement are primarily designed for formal methods experts and lack automation and extensibility. We apply program refinement to guide LLM and validate the LLM-generated code while transforming refinement into a more accessible and flexible framework. To initiate this vision, we propose Refine4LLM, an approach that aims to:(1) Formally refine the specifications, (2) Automatically prompt and guide the LLM using refinement calculus, (3) Interact with the LLM to generate the code, (4) Verify that the generated code satisfies the constraints, thus guaranteeing its correctness, (5) Learn and build more advanced refinement laws to extend the refinement calculus. We evaluated Refine4LLM against the state-of-the-art baselines on program refinement and LLMs benchmarks. The experiment results show that Refine4LLM can efficiently generate more robust code and reduce the time for refinement and verification.
@article{paperbot3246,
title = {Automated Program Refinement: Guide and Verify Code Large Language Model with Refinement Calculus},
author = {Yufan Cai and Zhe Hou and David Sanan and Xiaokun Luan and Yun Lin and Jun Sun and Jin Song Dong},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {POPL},
year = {2025},
doi = {10.1145/3704905}
}