Intel / article

Agentic Verified Optimization of Real-World Software

Source: arxiv.org
Author: Zhe Ye, Udaya Ghai, Zhizhen Qin, Dawn Song, Soonho Kong
Date: Published Oct 23, 2026

Why it matters

Tests can be gamed by coding agents, so equivalence checks based on them are weak. Having the agent deliver a Lean proof that the optimized code matches the original uses the existing implementation as the spec.

Key takeaways · AI-distilled

The task is posed at function and repository levels in Lean 4, where programs can both run and be reasoned about, so an optimized rewrite comes with a machine-checked equivalence proof instead of relying on tests the could exploit.
Because few real-world applications are written in Lean, the authors built Aqueduct, an agentic framework that ports C, C++, Go and Rust programs into native Lean and validates each port by differential testing against the original.
On the 189 reference implementations in Verina, agents produced faster proved rewrites for 156, including algorithmic changes such as replacing exponential recursion with dynamic programming.
On 17 migrated applications, 92 proved rewrites sped up 47 of 51 application scenarios. These gains were smaller than at the function level, so the authors identify choosing which functions to optimize as an important problem.

Terms in this piece · Glossary

AI agent — An AI system that doesn't just answer once but works toward a goal in a loop — taking actions, reading the results, and deciding what to do next.
eval — A repeatable test for AI quality — a set of tasks plus scoring — used the way software teams use test suites, because model output is too variable to judge by eyeballing.

Read the source arxiv.org