Automated Program Refinement: Guide and Verify Code Large Language Model with(…)
summary
A toolchain called Refine4LLM guides GPT-style code models with refinement calculus, generates code, then checks it with SMT/ATP verification (Z3-like solvers) and feeds counterexamples back to the model or switches refinement laws. It finds and learns learned refinement laws from ~100 example patterns with some human-in-the-loop curation. Demonstrations include catching a hallucinated infinite loop in a naive square‑root, producing provably terminating binary‑search and quicksort variants, and reducing refinement plus verification time versus baselines.
AI-written summary · about
chapters (8)
- 0:00Program refinement and LLM challenges
- 2:12Refinement calculus for correctness
- 5:49Guiding LLMs with formal systems
- 9:04Dynamic refinement from data
- 13:20System workflow and applications
- 15:06Limitations and future work
- 16:13Q&A: Invariants and variants
- 17:36Q&A: Dynamic laws for data
related talks
16mLemur: Integrating Large Language Models in Automated Program Verification
53mSemantics-based program manipulation in the age of LLMs
22mTowards Verified Code Reasoning by LLMs
18mReductive Analysis with Compiler-Guided Large Language Models for Input-Centric Code(…)
01h 02mHow can Machine Learning Help Formal Proving ?
17mRLM: Recursive Language Models for Large Codebases
32mCan We Trust AI-Generated Code?
21mVerMCTS: Synthesizing Multi-Step Programs using a Verifier, a Large Language Model,(…)