PaperlayerView exact revision on arXiv

Source-linked AI summary

Agentic Verified Optimization of Real-World Software

Zhe Ye, Udaya Ghai, Zhizhen Qin, Dawn Song, Soonho Kong

arXiv:2610.30188v1cs.SEcs.AIcs.LGcs.LOcs.PL

TL;DR

Test-based optimization checks can be exploited and do not guarantee preserved behavior. The paper has agents produce faster implementations with machine-checked equivalence proofs, using Lean and AQUEDUCT-migrated applications; verified rewrites improve 47 of 51 application scenarios and 156 of 189 Verina targets. Application-level gains are smaller than function-level gains, so target selection matters.

  • Problem

    Test-based checks do not guarantee behavior preservation and can reward agents for special-casing tested inputs, while joint implementation and proof search also requires balancing performance with provability.

    Source: §1 · pp. 1–2

  • Method

    The approach searches for faster implementations together with machine-checked equivalence proofs, using the reference as the specification and AQUEDUCT to migrate applications into Lean.

    Source: §1 · p. 2, §4.2 · pp. 7–8

  • Results

    Verified rewrites improve 47 of 51 application scenarios, and agents produce 156 verified improvements among 189 Verina targets.

    Source: §1 · p. 2, §5.1 · p. 10

  • Takeaways & Limitations

    Application-level gains are smaller than function-level gains, so choosing functions according to their share of application runtime matters.

    Source: §7 · p. 14

    The study’s equality criterion excludes opaque effects such as I/O and foreign calls, and can be stronger than callers require, as with floating-point tolerance.

    Source: §3.1 · p. 4

Abstract

from arXiv · show

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.

1 INTRODUCTION

Program optimization must make software faster without changing its behavior, but test-based checks can be exploited and do not guarantee equivalence. This paper pairs faster implementations with machine-checked proofs, evaluates the approach on Lean functions and migrated applications, and finds verified speedups at both levels.

Motivation

  • Test-based acceptance can reward agents for passing tests rather than preserving behavior, whereas equivalence proofs cover every input.The paper cites reward hacking and special-casing tested inputs as observed risks.Source: §1 · p. 1

Approach

  • Agentic verified optimization asks an agent to produce a faster implementation and a machine-checked equivalence proof against the reference implementation.The reference itself supplies the correctness specification, avoiding the need to write a separate specification.Source: §1 · p. 2

Challenge

  • The task couples implementation and proof search: a fast rewrite may be difficult to prove, while an easy-to-prove rewrite may offer little improvement.Agents must balance performance, proof construction, and search effort.Source: §1 · p. 2

Evaluation

  • Lean 4 supports executing and proving the same definitions; AQUEDUCT migrates C, C++, Go, and Rust applications to native Lean and checks ports against their originals.The evaluation uses 189 Verina implementations and migrated applications, measuring individual rewrites and application-level effects.Source: §1 · p. 2

Results

  • On 47 of 51 application scenarios, verified rewrites improve execution, while agents produce 156 verified improvements among 189 Verina targets.Across the migrated repositories, 92 proved rewrites are faster on function-level microbenchmarks; application-level gains are smaller than function-level gains.Source: §1 · p. 2

2 BACKGROUND AND RELATED WORK

Prior optimization and verification approaches face limits in correctness checks, the transformations they can express, proof requirements, and benchmark scope. The paper positions verified optimization against these limitations and describes AQUEDUCT as a way to obtain real-world Lean applications.

Correctness checks

  • Test-based checks can accept optimizations that exploit tests or omit behavior, while an equivalence proof rules out these failures by covering every input.The related-work discussion cites failures involving harness weaknesses, benchmark specialization, and kernel contracts.Source: §2 · p. 3

Expressiveness

  • Predefined passes, rewrite rules, representations, and target languages constrain what verified optimizers can express; agents can instead write new algorithms or data representations directly in Lean.The discussion contrasts fixed transformation spaces with agent-authored rewrites proved equivalent to the reference.Source: §2 · p. 3

Proof and specification

  • Automated equivalence checkers and written specifications limit existing agentic proof workflows, while the reference implementation can serve as the specification without being newly written.The cited examples include restricted checker acceptance and a reported false-acceptance rate, alongside the difficulty of writing specifications.Source: §2 · p. 3

Benchmark scope

  • Verified code-generation benchmarks check specification satisfaction but do not evaluate implementation speed.The passage lists function-level, verifier, and repository-scale benchmark families.Source: §2 · p. 3

Real-world applications

  • AQUEDUCT migrates applications into native Lean and validates each port with differential testing, fuzzing, and mutation analysis.The motivation is that Lean has few executable real-world applications with deployed callers and workloads.Source: §2 · p. 3

3 AGENTIC VERIFIED OPTIMIZATION

The paper formulates optimization as a search for a faster replacement and an equivalence proof, then extends the task from individual functions to repository-level changes. Agents jointly revise code and proofs, and Lean’s kernel checks rewrites while microbenchmarks and application scenarios measure performance.

3.1 PROBLEM FORMULATION

  • Behavioral equivalence requires the replacement to return the same result on every input, including Lean-expressed effects; opaque effects and weaker-than-equality correctness criteria fall outside this study.The replacement has the same signature and carries a proof of equality to the reference.Source: §3.1 · p. 4
  • Using the executable reference as the specification avoids writing a new specification, which can be difficult and may omit intended behavior.Equality to the reference keeps the correctness obligation fixed as the agent explores faster algorithms.Source: §3.1 · pp. 4–5
  • The objective is to minimize workload execution time subject to Lean accepting an equality proof against the fixed reference.A successful result must also be executable and build with its callers.Source: §3.1 · p. 5

3 AGENTIC VERIFIED OPTIMIZATION

  • Repository-level optimization asks the agent to choose functions within a search budget, prove each replacement equivalent, and reduce application execution time.Microbenchmarks measure individual rewrites; macrobenchmarks compare the integrated repository with the original.Source: §3.1 · p. 5

3.1 PROBLEM FORMULATION

  • For repository optimization, target choice balances runtime share and apparent provability; larger module rewrites can reach representations and control paths unavailable to single-function changes.A module rewrite requires interface equality, while exposing a changed representation in exported types requires a refinement relation.Source: §3.1 · p. 5

3.2 JOINT IMPLEMENTATION AND PROOF SEARCH

  • The longest-increasing-subsequence rewrite replaces exponential recursive search with a table-based algorithm and runs 4,467.871× faster on the 261-input corpus.A lemma relates table queries to the recursive helper across suffixes and possible preceding elements; Gron also reuses character-classification lemmas across rewrites.Source: Figure 2 · p. 6, §3.2 · p. 6
  • Agents revise implementations and proofs together because algorithm changes require linking different intermediate states, and Lean’s errors and goals guide further search.A failed proof does not distinguish an incorrect rewrite from an incomplete proof.Source: §3.2 · p. 6

3.3 ACCEPTANCE AND MEASUREMENT

  • Lean’s kernel checks each equality theorem against the unchanged reference, while microbenchmarks, application scenarios, and vfastp summarize performance at different levels.vfastp is the fraction of targets whose best verified candidate exceeds a specified speedup threshold.Source: §3.3 · p. 7

4 TARGETS FOR VERIFIED OPTIMIZATION

The paper studies verified optimization on standalone functions and complete applications, using Lean references for the former and AQUEDUCT-migrated programs for the latter. AQUEDUCT builds and checks migration tests against the original program before the resulting port becomes an optimization reference.

4 TARGETS FOR VERIFIED OPTIMIZATION

  • AQUEDUCT migrates C, C++, Go, and Rust applications into Lean because repository-level optimization requires complete applications with callers and workloads.The original executable serves as a behavior oracle and performance baseline; the port becomes the reference for optimization.Source: §4 · p. 7, §4.2 · p. 7

4.1 FUNCTIONS FROM VERINA

  • Verina provides 189 standalone Lean 4 reference functions, optimized over their valid inputs without using the suite’s formal specifications.A deterministic generator supplies up to 256 cases per target alongside official tests, and the functions are measured with microbenchmarks.Source: §4.1 · p. 7, Table 1 · p. 9

4.2 APPLICATIONS MIGRATED BY AQUEDUCT

  • AQUEDUCT develops each port and its test corpus together, using three diverse candidate ports and independent test design to expose behavioral differences.Differential execution, coverage, fuzzing, and mutation testing inform selection and repair; migration tests check exit status, output, filesystem effects, and timeouts.Source: §4.2 · pp. 7–8, Figure 3 · p. 8

5 EVALUATION

On Verina and migrated applications, agents found faster rewrites with equality proofs, and application-level gains persisted but were smaller than function-level gains. AQUEDUCT ports also recovered more original-program behavior than a single-agent migration baseline.

5 EVALUATION

  • The evaluation withheld workloads from optimization, required full equality, and used repeated paired timing trials on a frozen corpus for Verina.Repository workloads were independently constructed and fixed before optimization; application benchmarks measured integrated rewrites.Source: §5 · p. 9, §5.1 · p. 9, §5.2 · p. 10

5.1 FUNCTION-LEVEL OPTIMIZATION ON VERINA

  • 156 of 189 Verina functions received faster verified implementations; the fastest verified candidates yielded a 1.851× geometric mean speedup and 1.117× median.The gains include 71 functions above 1.25× and 38 above 2× speedup.Source: §5.1 · p. 10

5.2 REPOSITORY-LEVEL OPTIMIZATION ON AQUEDUCT PORTS

  • 1.120× faster across application scenarios, with gains in 47 of 51 scenarios and all 17 repositories by geometric mean, below the 1.864× function-level gain.Integrated rewrites are proved equal to the Lean declarations they replace; application gains are bounded by the share of scenario time spent in rewritten functions.Source: Figure 5 · p. 11, §5.2 · p. 12
  • The 92 proved repository rewrites achieved a 1.864× geometric mean speedup and 1.402× median; their patterns include algorithmic, representation, and evaluation-order changes.Fifteen optimized functions outperformed their matched original operation, compared with 12 migrated declarations.Source: §5.2 · p. 11
  • Across 40 repositories, AQUEDUCT recovered 87.68% of original-supported tests versus 68.17% for the single-agent baseline, a 19.50-point difference.Candidate diversity, generated tests, and repeated repair address outright port failures and rarer behaviors such as boundary inputs and exact diagnostics.Source: §5.2 · p. 12

6 RESEARCH DIRECTIONS

The research directions address certification across language boundaries, proof and implementation search, target selection, workload specialization, and broader equivalence and optimization models. They also propose learning from optimization trajectories and carrying verified optimizations into lower-level representations.

Allocating effort between implementation and proof

  • Future studies could compare whether optimizing before proving, proving after each change, or interleaving both finds useful verified replacements faster under matched budgets.Matched runs with and without proof requirements could test how proofs affect transformations attempted.Source: §6 · p. 12

Reusing proofs across optimizations

  • Comparing fresh proof search with reuse of earlier lemmas could measure effects on proof cost and verified improvements, including transfer across repositories.Maintenance studies could test whether agents adapt prior optimizations and proofs as callers and dependencies change.Source: §6 · p. 12

Selecting targets for application performance

  • Target selection could compare source-inspection choices with profile-informed choices, and local function rewrites with module-level shared-representation rewrites under matched budgets.Measuring application gains and rewrite combinations would expose interactions that isolated microbenchmarks miss.Source: §6 · pp. 12–13

Specializing to a kind of workload

  • Specializing to a described workload could let agents tailor representations and control paths while retaining a machine-checked obligation guarded by a workload predicate.The study withholds evaluation workloads and requires full equality; future work could measure speedup against proof effort and predicate coverage.Source: §6 · p. 13

Learning from optimization trajectories

  • Training on optimization trajectories could teach agents which changes to attempt and when to continue a proof or revise an implementation.Held-out repositories under fixed budgets could test whether this improves verified speedup beyond represented programs.Source: §6 · p. 13

Extending equivalence beyond equality

  • Opaque effects can be modeled so equivalence compares request-and-response behavior, while concurrency requires relations over observable interleavings or traces.When callers need only approximate agreement, a relation such as a relative-error bound can replace equality; the relation must reflect caller observations.Source: §6 · p. 13

Extending the optimization space

  • Verified rewrites could target explicit memory layouts, unboxed representations, or vector instructions, with the trusted boundary moved to the lowering that produces the artifact.Optimizing Lean core-library functions or compiler passes could extend verified optimization to their callers or the compiler itself.Source: §6 · p. 13

Certifying migration

  • Certifying a migrated application end to end would require a proof connecting its source program to its Lean port, which could compose with the optimization proof.Where source models are available, translating Rust to Lean offers a shorter route, with the translation as the trusted step.Source: §6 · pp. 13–14

7 CONCLUSION

The paper formulates verified optimization as finding a faster implementation with a proof of equivalence to an existing program, and reports proved improvements in standalone functions and migrated applications. Application gains are smaller than function-level gains, so target selection matters.

7 CONCLUSION

  • Agents produce verified optimizations in both standalone Lean functions and applications migrated by AQUEDUCT.Rewrites include eliminating intermediate structures and reordering computation.Source: §7 · p. 14
  • Application-level gains are smaller than function-level gains, and four scenarios do not improve, so a locally faster function may not speed up its application.Target selection should account for each function’s share of application runtime.Source: §7 · p. 14
  • The formulation and findings support studying how agents coordinate implementation and proof search to improve application performance with machine-checked correctness.Source: §7 · p. 14

A CORRECTNESS CHECKS

The acceptance protocol checks that a rewrite is proved against an unchanged reference, executable, and integrated into a building repository. Its scope is limited to functions whose effects are expressed inside Lean.

A CORRECTNESS CHECKS

  • The protocol covers pure functions and Lean computations such as Id, StateM, and Except, but excludes opaque effects such as IO and foreign calls.For covered functions, equality applies to every input without a bound on input size or recursion depth.Source: A CORRECTNESS CHECKS · p. 21
  • The build check preserves every existing declaration byte-identically and verifies that the repository builds with the replacement and its proof.A separate integration check registers the theorem as a @[csimp] replacement so compiled callers use the rewrite.Source: A CORRECTNESS CHECKS · p. 21
  • Proofs and auxiliary declarations may use only propext, Quot.sound, and Classical.choice, with sorryAx forbidden.Source: A CORRECTNESS CHECKS · p. 21
  • The rewrite and computational dependencies must be executable, without partial or unsafe definitions or @[implemented_by] and @[extern] substitutions.They use the task’s fixed library and runtime.Source: A CORRECTNESS CHECKS · p. 21
  • The proof must be checked by Lean’s kernel and cannot use native_decide to discharge a proof step.The checker also rejects agent-introduced typeclass instances that would change equality’s interpretation; accepted implementations are compiled and timed with fixed tools.Source: A CORRECTNESS CHECKS · p. 21

B MIGRATION PIPELINE AND RESULTS

AQUEDUCT migrates applications through candidate generation, test design, comparison, selection, and repair, with consistent interface-comparison rules throughout. Its generated tests reveal behavioral differences that benchmark tests miss, and the ports recover more original-supported behavior than a single-agent baseline.

B MIGRATION PIPELINE AND RESULTS

  • AQUEDUCT generates candidates, designs tests for uncovered behavior and disagreements, compares ports with the original, selects a candidate, and coordinates repair.Coverage and mutation feedback guide further test generation; hidden tests and signals derived from them remain inaccessible to agents.Source: B MIGRATION PIPELINE AND RESULTS · p. 21
  • The same comparison rule applies during migration and hidden evaluation, while unstable behavior is excluded or handled by a declared rule.This keeps required behavior consistent across candidate selection, repair, and evaluation.Source: B MIGRATION PIPELINE AND RESULTS · p. 21
  • Across 40 repositories, AQUEDUCT ports recover 87.68% of original-supported tests versus 68.17% for the single-agent baseline.The ports pass 16,345 of 18,642 original-supported tests, compared with 12,709 for the baseline.Source: B MIGRATION PIPELINE AND RESULTS · p. 21
  • The mutation audit injects deterministic source-level faults after the test suites are frozen and counts only mutants that compile.A mutant is killed only if a test passing on the original fails on the mutant; the test-design agents generated 33,671 behavioral tests.Source: B MIGRATION PIPELINE AND RESULTS · p. 22
  • On 36 compiled mutants across 9 repositories, generated tests kill 28 (77.8%) versus 17 (47.2%) for ProgramBench tests, with the generated suite catching 12 of 13 mutants caught by only one suite.The table compares both suites on the same mutants.Source: B MIGRATION PIPELINE AND RESULTS · p. 22, Table 3 · p. 22
  • At the program boundary, surviving mutants identify behaviors the corpus executes but does not yet constrain, making them targets for further test generation.The full audit population is reported in Table 4.Source: B MIGRATION PIPELINE AND RESULTS · p. 22, Table 4 · p. 22

C MIGRATION ABLATIONS

The ablations show that every component improves recovery relative to the single-agent baseline, while a fixed phased pipeline performs worse. Candidate diversity and the two testing signals make substantial contributions, and iterative repair outperforms a fixed sequence.

C MIGRATION ABLATIONS

  • The ablations compare one repair round, removal of coverage guidance, removal of mutation feedback, the best single migration strategy, a single-agent baseline, and a fixed phased pipeline.Source: C MIGRATION ABLATIONS · pp. 22–23
  • 87.68% recovery for the full pipeline exceeds 68.17% for a single agent, every component ablation falls between them, and the fixed phased pipeline falls below the single agent.Figure 6 compares the full pipeline with four component ablations and two baselines.Source: Figure 6 · p. 23, C MIGRATION ABLATIONS · p. 23
  • The fixed phased pipeline recovers less than the single-agent baseline despite using the same tools, while iterative repair lets agents revisit earlier decisions when later evidence reveals missed behavior.The result suggests allowing agents freedom in how they work while keeping acceptance criteria and checks rigorous.Source: C MIGRATION ABLATIONS · p. 23
  • Candidate diversity provides the largest gain: the best single migration strategy reaches 72.96% recovery, and no one strategy dominates across repositories.Because repair rarely changes a port’s overall structure, useful structural diversity must be present among initial candidates.Source: C MIGRATION ABLATIONS · p. 23
  • Removing coverage guidance costs 9.80 points and removing mutation feedback costs 10.05 points, exceeding the 8.46-point loss from limiting repair to one round.Coverage steers tests toward unexercised behavior, while mutation feedback strengthens checks on behavior the corpus already reaches.Source: C MIGRATION ABLATIONS · p. 23

D.1 LONGEST INCREASING SUBSEQUENCE

The LIS rewrite is proved equivalent for every input list by relating its table query to the recursive helper. Across 261 evaluation inputs, it achieves a 4,467.871× speedup.

D.1 LONGEST INCREASING SUBSEQUENCE

  • The proof covers every integer list and every optional preceding element, showing the computed table query matches the recursive helper’s length.Source: §D.1 · p. 23
  • 4,467.871× speedup: median time per corpus pass falls from 1.424 seconds to 318.653 microseconds across 261 inputs.Source: §D.1 · p. 24

D.2 MIGRATION AT SCALE: 7ZIP

The 7zip port recovers 554 of 883 original-supported tests, while its generated behavioral-test results and remaining open obligations make the migration gap measurable.

D.2 MIGRATION AT SCALE: 7ZIP

  • 62.74% of 883 original-supported tests are recovered by the final port, compared with 28.77% for the baseline.Source: §D.2 · p. 24
  • At the final checkpoint, the port passes 541 of 579 generated behavioral tests, with 938 behavioral obligations still open when the budget is exhausted.The remaining open obligations account for the gap between generated-corpus pass rate and hidden-set recovery.Source: §D.2 · pp. 24–25

D.3 OPTIMIZATION CASE STUDIES

Five proved rewrites illustrate algorithmic, representation, and evaluation-order improvements in migrated code. In each case, equality proofs establish that the rewrite preserves behavior on every input.

D.3 OPTIMIZATION CASE STUDIES

  • Cheat findConsolidated’s direct reverse search is 5.46× faster than migrated Lean and 20.36× faster than the matched Go operation.It avoids building the consolidated sheet list before searching.Source: §D.3 · p. 25
  • Cheat consolidatedSheets’ reverse traversal with a hash set is 1.46× faster than migrated Lean and 6.65× faster than the matched Go operation.It preserves last-title-wins semantics while avoiding repeated filtering and reallocation.Source: §D.3 · p. 25
  • Gron validIdentifier’s allocation-free check is 1.96× faster than migrated Lean and 2.10× faster than Go.The proof reuses lemmas for character-classification replacements.Source: §D.3 · p. 25
  • Cheat filterSheets’ one-time tag normalization is 5.45× faster than migrated Lean and 2.01× faster than the matched Go operation.Output checksums agree across all three implementations.Source: §D.3 · p. 25
  • Code Minimap pow10’s zero-exponent fast path is 9.29× faster within Lean and 1.37× faster than the Rust original on a microbenchmark including zero.Source: §D.3 · p. 25
  • All five rewrites remove common migrated-code patterns, and their equality proofs guarantee behavior is preserved on every input.Source: §D.3 · p. 25

Related papers

Loading 2610.30188v1…