LPO: Discovering Missed Peephole Optimizations with Large Language Models

Compilers speed up code by spotting tiny inefficient instruction sequences and rewriting them into better ones, but there are so many possible patterns that even mature compilers like LLVM keep missing optimizations, and finding new ones by hand or by exhaustive search is slow or limited; this paper (University of Waterloo and Monash University — Zhenyang Xu, Chengnian Sun, and colleagues) presents LPO, which pairs a large language model's creativity with a formal verifier's rigor in a feedback loop, letting the model propose rewrites while the verifier proves them correct — discovering dozens of real missed optimizations in LLVM.

The argument in one glance

Problem

Compilers keep missing tiny local optimizations, because there are too many to enumerate

Compilers make programs faster without changing what they do, and a lot of that work happens in a series of optimization passes over the program's intermediate representation. One of the most important is peephole optimization: it looks at a small "window" of a few dependent instructions and, if that sequence is inefficient, replaces it with an equivalent but better one — folding constants, removing redundant work, simplifying operations. These local rewrites matter twice over, because besides making the code smaller and faster directly, they often unlock bigger optimizations by later passes. The trouble is that peephole optimization is not one clean algorithm. Unlike, say, dead-code elimination, which can be a single unified procedure, peephole optimizations are a huge collection of individual pattern-matching and rewriting rules — "if you see this instruction sequence, rewrite it to that one." And modern instruction sets are so broad that the number of possible patterns multiplies explosively, so no one can write them all down. That is why the optimizer in a compiler like LLVM is never finished: engineers keep discovering and adding new patterns, and the compiler keeps missing optimizations it could have made. Each missed pattern is code that is slower or larger than it needs to be, across every program the compiler touches. The open problem is how to systematically find the ones it is missing.
What people did

Find missed optimizations by hand, by differential testing, or by superoptimization

Three approaches exist. Manual inspection has a human read the generated IR or assembly and spot suboptimal patterns; this has found many optimizations over the years. Differential testing automatically detects missed opportunities, either by comparing the outputs of different optimizing compilers or by comparing how a compiler handles two programs that are semantically equivalent. Superoptimization takes a sequence of instructions and searches — by stochastic search or program synthesis — for the truly optimal equivalent sequence; recent superoptimizers for LLVM include Souper and Minotaur.
Why it fell short

Each existing method is either unscalable or fundamentally restricted

None of the three can systematically discover genuinely new optimizations at scale. Manual inspection is labor-intensive, demands deep compiler expertise, and simply does not scale to the vast space of patterns. Differential testing is effective but limited by construction: comparing against other compilers can only surface optimizations that some other compiler already implements, and comparing equivalent programs finds cases where a compiler underperforms its own expectations — neither discovers entirely new classes of optimization that no existing tool knows. Superoptimization can in principle find optimal sequences, but in practice it either does not scale (the search space of instruction sequences is enormous) or comes with significant restrictions on the kinds of optimizations it can express and find. So the field was caught between methods that are creative but unscalable and methods that are automatic but confined to what is already known or narrowly searchable. What was missing was a way to explore the space creatively, like a human expert, but automatically and at scale — while still guaranteeing that every proposed rewrite is actually correct.
This paper's idea

Let an LLM propose rewrites and a formal verifier prove them, in a feedback loop

LPO's key insight is that two very different tools have exactly complementary strengths and weaknesses. Large language models are good at creative exploration — they can propose plausible, human-like rewrites across the whole breadth of an instruction set — but they hallucinate, confidently suggesting rewrites that are subtly wrong. Formal verification is the opposite: it gives rigorous, airtight correctness guarantees, but it cannot creatively discover what to try. LPO combines them in a closed-loop feedback mechanism so each covers the other's weakness. The framework has three components. An extractor analyzes programs to pull out candidate instruction sequences worth optimizing. An LLM-based optimizer takes a candidate and proposes a more efficient equivalent sequence. A verifier then rigorously checks the proposal on two counts: that it is a valid refinement (semantically equivalent, or a legal refinement when the original had undefined behavior) and that it actually improves performance. If the proposal passes, it is saved as a discovered optimization. If it fails, the verifier's output — precisely why it was wrong — is fed back to the LLM as targeted guidance, and the LLM tries again. This loop lets LPO explore creatively but never accept an incorrect rewrite. Evaluated in the LLVM ecosystem, LPO identifies up to 22 of 25 previously-reported missed optimizations, versus 15 for the superoptimizer Souper and 3 for Minotaur. And over eleven months of intermittent testing it discovered 62 missed peephole optimizations that had not been reported, 28 of which were confirmed and 13 already fixed in LLVM — with Souper and Minotaur failing to find 26 and 31 of those, respectively.

Why this problem is worth solving

Peephole optimizations run on essentially every compiled program, so each missed one is a small tax multiplied across all software, and finding them has been stubbornly manual.

Compilers are foundational infrastructure: the optimizations they apply improve the speed and size of code across every program built with them, so an improvement in the compiler compounds enormously. Peephole optimizations are especially pervasive because they are local and cheap and run everywhere, and they have a multiplier effect — a small local rewrite can expose a larger optimization to a later pass. But because they are a sprawling collection of individual patterns rather than one algorithm, discovering the ones a compiler is still missing has depended largely on expert humans reading code and noticing suboptimal sequences, which is slow and does not keep up with the growth of instruction sets. Automating that discovery, at scale and with correctness guaranteed, would let a compiler continuously improve without waiting on scarce expert attention. And because the discovered optimizations are verified and can be added to the real compiler, the benefit is durable and broad. As the paper notes, the approach also improves on its own over time: as language models get better at reasoning, the same framework finds more, so the value grows with the underlying models.

The crux is a division of labor that plays each tool to its strength and cancels its weakness.

The reason neither an LLM alone nor a verifier alone solves this is that each is missing exactly what the other has. An LLM can range creatively over the enormous space of possible rewrites, proposing the kind of clever, non-obvious transformation a human expert might — but it has no way to know if a proposal is actually correct, and it will hallucinate rewrites that look right and are not. A formal verifier can prove, with certainty, whether a given rewrite preserves the program’s meaning and improves it — but it has no imagination; it can only check candidates handed to it, not dream them up. Put them together and the gaps close: the LLM supplies the creativity that the verifier lacks, and the verifier supplies the correctness that the LLM lacks. The feedback loop is what makes the pairing more than the sum of its parts. When the verifier rejects a proposal, it does not just say no — it explains precisely why the rewrite is wrong, and that explanation is handed back to the LLM as a concrete correction to reason about, so the next attempt is informed rather than a blind re-guess. This turns a fallible generator and a rigorous but passive checker into a system that explores broadly yet only ever accepts truths, which is exactly what discovering new, correct optimizations requires.

What people did before, and where it broke

Inspect the generated code by hand. Have an expert read the IR or assembly and spot suboptimal instruction patterns. Where it broke. It is labor-intensive, needs deep compiler expertise, and cannot scale to the vast and growing space of possible patterns.
Differential testing against other compilers. Compare a compiler’s output to another compiler’s to find where it does worse. Where it broke. It can only surface optimizations that some other compiler already implements, not genuinely new ones.
Differential testing on equivalent programs. Compile two semantically equivalent programs and compare. Where it broke. It finds cases where a compiler underperforms its own expectations, not entirely new classes of optimization.
Superoptimization by search or synthesis (Souper, Minotaur). Search for the optimal equivalent instruction sequence. Where it broke. The search space is enormous, so it either does not scale or is significantly restricted in the optimizations it can express and find.
The gap. No method explored the optimization space as creatively as a human expert, but automatically and at scale, while still guaranteeing every discovered rewrite is correct.

How LPO works

A closed loop of creative proposal and rigorous verification

↓ →
new
↓ →
new
↓ →
new
↓ →
new
↓ →
new

The idea

Use a large language model to explore the space of rewrites creatively. LPO’s generative half asks an LLM to propose better instruction sequences, exploiting exactly the creative breadth that makes language models good at code but that rigid search lacks. Applying a large language model to discover and generate improvements to code, ranging over transformations a human might think of, is the same approach the work on retrieval-augmented loop-transformation optimization (LoopRAG) covered elsewhere on this site takes, using an LLM to propose code optimizations rather than enumerate them mechanically. LPO applies it to peephole rewrites, letting the model suggest the non-obvious local transformations a compiler is missing.

Guarantee correctness by formally verifying refinement. LPO never trusts the LLM’s proposal; a formal verifier proves each rewrite is a valid refinement of the original before it is accepted. Rigorously checking that a proposed transformation preserves the program’s meaning — that the new version refines the old — is the same discipline the work on checking model refinement to catch distributed-model bugs (Entangle) covered elsewhere on this site applies, treating refinement as the correctness property to prove rather than to hope for. LPO uses refinement checking to filter the LLM’s creative but fallible output down to only correct optimizations.

Search for better code, but with a generator instead of a blind synthesizer. LPO occupies the same goal as superoptimization — find a better equivalent instruction sequence — but replaces exhaustive or stochastic search with a language model guided by verifier feedback. Searching the space of programs for a better sequence with the same behavior is the same objective the work on tree-traversal synthesis using domain-specific symbolic compilation covered elsewhere on this site pursues, synthesizing correct code that meets a goal. LPO trades the synthesizer’s narrow, scaling-limited search for an LLM’s broad creativity, kept honest by the verifier.

Following a candidate through LPO

Discovering and verifying one missed peephole optimization

A trace, drawn from the paper, of how LPO turns a candidate instruction sequence into a verified optimization.

Step 1 of 5

The extractor finds a candidate sequence

LPO's extractor analyzes programs and pulls out a small window of dependent instructions that looks like it might be suboptimal — a candidate for a better rewrite.

This is the raw material the loop will try to improve.

Why it works

The LLM supplies creativity the verifier lacks. A formal verifier can only check candidates, not invent them → but an LLM proposes plausible rewrites across the whole instruction set → so the system explores the space as creatively as an expert, automatically.
The verifier supplies correctness the LLM lacks. An LLM hallucinates rewrites that look right but are wrong → but formally proving each proposal is a valid refinement → so only correct optimizations are ever accepted.
Feedback turns rejection into progress. A rejected proposal would otherwise be a dead end → but handing the LLM the verifier’s explanation of the error → so the next attempt is a targeted correction, not a fresh blind guess.
Checking performance keeps discoveries worthwhile. A correct rewrite is not necessarily a better one → but verifying that the proposal actually improves performance too → so LPO saves only optimizations that are both valid and beneficial.
Breadth beats narrow search on real cases. Superoptimizers are confined by their search space → but an LLM ranges over rewrites those searches cannot express → so LPO finds many missed optimizations that Souper and Minotaur do not.

What it costs (trade-offs and scope)

It depends on the LLM’s reasoning quality. LPO’s discoveries come from what the model can creatively propose; a weaker model finds fewer, and the paper frames the method as improving precisely as LLM reasoning advances — so its power is tied to a component that is outside the framework and evolving.
The verifier bounds what can be confirmed. Every accepted optimization must pass formal verification, so LPO can only discover rewrites the verifier can actually prove correct and beneficial; transformations beyond the verifier’s reach cannot be confirmed even if proposed.
The loop spends LLM and verification effort per candidate. Each candidate may take several propose-verify-feedback rounds, and both the LLM calls and the formal checks have cost, so discovery is a compute-spending search rather than a one-shot lookup.
It targets local peephole optimizations. LPO is aimed at small instruction-sequence rewrites; larger or more global optimizations that are not expressible as a local peephole are outside its scope.
Reported results are within the LLVM ecosystem. The 22-of-25 and 62-found figures, and the comparisons to Souper and Minotaur, are measured against LLVM and a curated benchmark; results in other compilers or with other verifiers would depend on those settings.

The evaluation

Discovering missed peephole optimizations

Property	Manual or differential testing	Superoptimizers (Souper, Minotaur)	LPO
How candidates are found
Correctness guarantee
Finds genuinely new optimizations
Known-benchmark recall (of 25)
New optimizations found

A comparison of ways to discover missed peephole optimizations. By pairing an LLM's creative proposal of rewrites with a formal verifier's rigorous refinement-and-performance check in a closed feedback loop, LPO identifies up to 22 of 25 previously-reported missed optimizations in LLVM (versus 15 for Souper and 3 for Minotaur) and found 62 unreported missed optimizations over eleven months (28 confirmed, 13 already fixed), which the superoptimizers largely miss. Exact figures should be read from the paper.Underlined values explain themselves when clicked.

Where this stops working

What to keep in mind

This explainer is based on the paper’s full text (the authors’ arXiv copy, 2508.16125, of the ASPLOS 2026 paper). The described system is the paper’s: LPO is an automated framework to discover missed peephole optimizations, built on the insight that large language models are effective at creative exploration but prone to hallucination, while formal verification gives rigorous guarantees but cannot creatively discover — so LPO combines them in a closed-loop feedback mechanism. Its workflow has three components: an extractor that identifies candidate instruction sequences; an LLM-based optimizer that proposes a more efficient equivalent; and a verifier that checks the proposal for valid refinement (semantic equivalence, or legal refinement when the original has undefined behavior) and for performance improvement, saving it if verified and, if not, feeding the verifier’s output back to the LLM as targeted guidance for a corrected attempt. Evaluated within the LLVM ecosystem, the paper reports LPO identifies up to 22 of 25 previously-reported missed optimizations, versus 15 for Souper and 3 for Minotaur (two recent LLVM superoptimizers), and that over eleven months of development and intermittent testing LPO found 62 missed peephole optimizations, with 28 confirmed and 13 already fixed in LLVM, while Souper and Minotaur fail to identify 26 and 31 of those confirmed or fixed cases, respectively. The background above on compiler passes, intermediate representation, refinement, and superoptimization is standard compiler context provided to make the approach intuitive. The step-by-step walkthrough is an illustration of the described mechanism. Exact details of the extractor, the LLM prompting, the verifier, and the full evaluation should be read from the paper.

Background

Why pairing a creative generator with a rigorous checker keeps being the winning recipe

It helps to see LPO within a broad pattern: some of the most effective recent uses of machine learning in systems and compilers come not from trusting a model’s output, but from pairing a fallible, creative generator with a rigorous, trustworthy checker, and letting the checker’s feedback steer the generator. A language model is wonderful at proposing ideas across a huge space and terrible at guaranteeing any of them is correct; a formal method is the reverse. Neither is sufficient alone for a task where wrong answers are unacceptable — like changing what a compiler does to a program. But together, in a loop where the verifier both filters and teaches, they become a system that can explore boldly while only ever committing to what is proven. This structure recurs wherever creativity and correctness are both required: the generator dreams, the checker disciplines, and the feedback closes the gap. It is essentially the recipe of combining machine learning with a solver when high precision is required, one of the reusable patterns the work on whether machine learning for systems has reached an inflection point covered elsewhere on this site identifies, precisely because it lets learned components be used safely where mistakes would be costly. LPO’s contribution is to instantiate this recipe for compiler peephole optimization, showing that an LLM guided by a formal verifier can rediscover most known missed optimizations and unearth dozens of genuinely new ones in a mature compiler, and that it will keep finding more as language models improve.

If you remember only three things

1. Peephole optimization rewrites small, inefficient instruction sequences into better equivalent ones, directly improving code and often unlocking bigger optimizations by later passes. But unlike a single-algorithm optimization, peephole optimizations are a vast collection of individual pattern-and-rewrite rules, and modern instruction sets make the space of patterns explode, so even mature compilers like LLVM keep missing optimizations. The three existing ways to find missed ones are each limited: manual inspection is labor-intensive and does not scale, differential testing only finds optimizations other compilers already implement or cases a compiler underperforms, and superoptimizers (Souper, Minotaur) either do not scale or are significantly restricted by their search space.
2. LPO's insight is that LLMs and formal verifiers have exactly complementary strengths: LLMs explore creatively across the whole instruction set but hallucinate incorrect rewrites, while formal verification guarantees correctness but cannot invent candidates. LPO combines them in a closed feedback loop of three parts: an extractor pulls out candidate instruction sequences; an LLM-based optimizer proposes a more efficient equivalent; and a verifier rigorously checks the proposal for valid refinement (semantic equivalence, or legal refinement of undefined behavior) and for performance improvement. A passing proposal is saved; a failing one has the verifier's explanation fed back to the LLM as targeted guidance for a corrected attempt. This lets LPO explore broadly yet accept only provably correct, beneficial optimizations.
3. Evaluated in the LLVM ecosystem, the paper reports LPO identifies up to 22 of 25 previously-reported missed optimizations, versus 15 for Souper and 3 for Minotaur, and that over eleven months of intermittent testing it discovered 62 unreported missed peephole optimizations, 28 confirmed and 13 already fixed in LLVM, with the superoptimizers failing to find 26 and 31 of those. The trade-offs: LPO's power depends on the LLM's reasoning (and improves as models improve), the verifier bounds what can be confirmed, each candidate spends LLM and verification effort over several rounds, it targets local peephole rewrites, and the results are within LLVM. The approach is a clean instance of pairing a creative generator with a rigorous checker.

Check yourself

Check your understanding

1. Why do even mature compilers like LLVM keep missing peephole optimizations?
2. What limited the three prior approaches (manual inspection, differential testing, superoptimization)?
3. What is LPO's key insight about combining large language models and formal verification?
4. What did LPO achieve in the LLVM ecosystem, and what bounds its power?

Sources

The paper is “LPO: Discovering Missed Peephole Optimizations with Large Language Models” by Zhenyang Xu, Hongxu Xu, Yongqiang Tian, Xintong Zhou, and Chengnian Sun (Cheriton School of Computer Science, University of Waterloo, and Monash University), published at ASPLOS 2026, DOI 10.1145/3779212.3790184. It is available on arXiv as 2508.16125.

This explainer is written from the paper’s full text (the authors’ arXiv copy). LPO is an automated framework for discovering missed peephole optimizations, built on the insight that large language models are effective at creative exploration but prone to hallucination, while formal verification gives rigorous guarantees but cannot creatively discover — so LPO combines them in a closed-loop feedback mechanism. Its three components are an extractor that identifies candidate instruction sequences, an LLM-based optimizer that proposes a more efficient equivalent, and a verifier that checks the proposal for valid refinement and performance improvement, saving it if verified and otherwise feeding the verifier’s output back to the LLM as targeted feedback for a corrected attempt. Evaluated within the LLVM ecosystem, the paper reports LPO identifies up to 22 of 25 previously-reported missed optimizations (versus 15 for Souper and 3 for Minotaur), and that over eleven months it found 62 missed peephole optimizations, with 28 confirmed and 13 already fixed in LLVM, while Souper and Minotaur fail to identify 26 and 31 of those, respectively. Numbers are the paper’s own; exact mechanisms and full results should be confirmed in the paper.