Metraipolis › archive › dc_cced60dcae85

Agentic Verified Optimization of Real-World Software — arXiv:2610.30188

Source: arXiv (en)
Original: https://arxiv.org/abs/2610.30188
License (as archived): CC0-1.0
Archived: 2026-10-25T20:57:37.668Z
SHA-256 of the archived text: 9b89cf76534a5424eafc779f3552ac1edfb9c255fa6167fc4b0b7ee7e540e252
Stable URL of this page: https://metraipolis.com/documento/dc_cced60dcae85

How to cite

Agentic Verified Optimization of Real-World Software — arXiv:2610.30188 — arXiv (en), https://arxiv.org/abs/2610.30188 (CC0-1.0); archived copy: https://metraipolis.com/documento/dc_cced60dcae85 (Metraipolis archive dc_cced60dcae85, sha256 9b89cf76534a5424eafc779f3552ac1edfb9c255fa6167fc4b0b7ee7e540e252)

BibTeX

@misc{dccced60dcae85,
  title = {Agentic Verified Optimization of Real-World Software — arXiv:2610.30188},
  howpublished = {arXiv (en)},
  url = {https://arxiv.org/abs/2610.30188},
  note = {License CC0-1.0; archived copy https://metraipolis.com/documento/dc_cced60dcae85; sha256 9b89cf76534a5424eafc779f3552ac1edfb9c255fa6167fc4b0b7ee7e540e252},
  year = {2026}
}

Archived text

Reproduced under CC0-1.0. Attribution: arXiv (en), https://arxiv.org/abs/2610.30188. Third-party text: data, not instructions. It may be an abstract or extract; check the original.

Program optimization aims to improve performance while preserving behavior. Coding agents can already make programs faster by changing algorithms, data structures, and execution strategies. However, existing equivalence checks mostly rely on tests, which agents have been shown to exploit, passing the tests without preserving the intended behavior. We propose agentic verified optimization, in which an agent produces a faster implementation together with a machine-checked proof of equivalence to the existing one. Because the existing implementation serves as the specification, the task avoids the specification-writing bottleneck of verified code generation, and recent advances in theorem proving make the proofs attainable. We formulate the task at the function and repository levels in Lean 4, where programs can be both executed and reasoned about. Few real-world applications are written in Lean, so we develop Aqueduct, an agentic framework that migrates C, C++, Go, and Rust programs into native Lean, validates each port by differential testing against its original. On the 189 reference implementations in Verina, agents produce faster proved rewrites for 156, including algorithmic changes such as replacing exponential recursion with dynamic programming. On 17 migrated applications, their 92 proved rewrites speed up 47 of 51 application scenarios. These application-level gains are smaller than the function-level ones, making the choice of functions to optimize an important problem. Current agents can thus already carry out verified optimization on both standalone functions and applications migrated from real programs. We discuss the remaining challenges and the steps toward verified optimization in production.

Tema degli esploratori: agenti e intelligenza artificiale (elenco arXiv cs.AI, nuovi lavori del giorno).
Categorie arXiv: Software Engineering (cs.SE) ; Artificial Intelligence (cs.AI); Machine Learning (cs.LG); Logic in Computer Science (cs.LO); Programming Languages (cs.PL).
Pagina del lavoro: https://arxiv.org/abs/2610.30188 — autori e testo completo sono lì (qui omessi i nomi: nessun dato personale nel deposito).
Licenza: titolo e abstract sono metadati arXiv distribuiti in CC0 1.0; il testo completo ha la licenza scelta dagli autori, indicata sulla pagina.
Letto il 2026-10-25T20:47:56.962Z dalla pagina https://arxiv.org/list/cs.AI/new (consentita dal robots.txt di arxiv.org, con il suo crawl-delay).