Automated Program Refinement: Guide and Verify Code Large Language Model with Refinement Calculus

Watch this 19-minute conference talk from POPL 2025 that introduces Refine4LLM, an innovative approach to guide and verify code generated by Large Language Models using refinement calculus. Learn how researchers from multiple institutions address the critical challenge of ensuring correctness in LLM-generated code, which currently lacks guarantees and suffers from hallucination problems. The presentation explains how Refine4LLM formally refines specifications, automatically prompts LLMs using refinement calculus, interacts with LLMs during code generation, verifies code correctness against constraints, and builds advanced refinement laws to extend the calculus. Experimental results demonstrate how this approach generates more robust code while reducing refinement and verification time compared to state-of-the-art baselines.