The authors formulate optimization in Lean 4, a language in which programs can both execute and serve as objects of mathematical proof.
Coding agents produce faster software with machine-checked proofs of equivalence
The authors demonstrate verified optimization in Lean 4 on 189 reference functions and 17 applications migrated from other programming languages.
Big Tech
Zhe Ye · Udaya Ghai · Zhizhen Qin · Dawn Song · Soonho Kong
University of California, Berkeley · Amazon Web Services
Research Digest··2 min read
Ye and colleagues ask coding agents to deliver two things together: a faster implementation and a machine-checked proof that it preserves the reference implementation’s behavior.
§