qed-superopt

An LLM finds faster code. A theorem prover makes sure it's right.

qed-superopt is a superoptimizer for LLVM IR. A Meta model proposes rewrites of small, hot functions that beat clang -O3, and Alive2 formally proves every rewrite correct, for every possible input. When a proposal is wrong, the prover returns a counterexample, the model repairs its attempt, and the loop continues. Nothing unproven ever reaches the output.

Quod erat demonstrandum: what was to be shown, has been shown.

Built for the Meta Global AI Developer Hackathon (Oct 26 – Nov 4, 2026), theme Push the Frontier.

---

Why

Compilers are excellent, but not perfect. Every month, developers report missed optimizations to LLVM: code where clang -O3 emits more instructions than necessary. Finding them by hand is slow, and checking that a clever rewrite is really correct is even slower, because the traps are subtle: signed overflow, shifts past the bit width, poison values.

LLMs are good at the first part: creative, plausible rewrites. They are terrible at the second: they hallucinate with confidence. So we split the job:

	Creativity	Certainty
LLM alone	✅	❌
Exhaustive search (classic superoptimizers)	❌ limited by search space	✅
qed-superopt	✅ the LLM proposes	✅ the prover decides

How it works

flowchart LR
    C["C function"] -->|"clang -O3"| SRC["Reference IR"]
    SRC --> LLM["Meta model<br/>proposes a rewrite"]
    LLM --> V{"Alive2<br/>proof"}
    V -->|"counterexample"| LLM
    V -->|"proven ✓"| COST["llc + llvm-mca<br/>measure the gain"]
    COST --> OUT["Proven, faster IR"]

Loading

1. Extract a function's IR as produced by clang -O3: the baseline to beat.
2. Propose: a Meta model (Muse Spark via the Meta Model API) rewrites it.
3. Prove: Alive2 checks the rewrite against the original with an SMT solver (Z3). If it is wrong, Alive2 produces a concrete input that breaks it, which goes back to the model.
4. Measure: the proven rewrite is lowered to x86-64 assembly and scored with llvm-mca (Skylake), then timed on a real CPU.

Quick start

You need uv and the reference toolchain: LLVM b974545 and Alive2 adacbd5, with Z3, in a qed-toolchain folder next to this repository (or set QED_TOOLCHAIN). Building LLVM takes hours:

mkdir ../qed-toolchain && cd ../qed-toolchain
git init llvm-project && cd llvm-project
git remote add origin https://github.com/llvm/llvm-project.git
git fetch --depth 1 origin b97454582dfbe2d5ebe7b7b1533de947bef16942 && git checkout FETCH_HEAD
cd ..
cmake -G Ninja -S llvm-project/llvm -B llvm-build -DCMAKE_BUILD_TYPE=Release \
  -DLLVM_ENABLE_PROJECTS="llvm;clang" -DLLVM_TARGETS_TO_BUILD="X86;AArch64" \
  -DLLVM_ENABLE_ASSERTIONS=ON -DLLVM_ENABLE_RTTI=ON -DLLVM_ENABLE_EH=ON -DBUILD_SHARED_LIBS=ON \
  -DLLVM_INCLUDE_TESTS=OFF -DLLVM_INCLUDE_BENCHMARKS=OFF -DLLVM_INCLUDE_EXAMPLES=OFF
ninja -C llvm-build
git clone https://github.com/AliveToolkit/alive2.git
git -C alive2 checkout adacbd5180ccf95075e9867c4f0c259f59c9fef2
cmake -G Ninja -S alive2 -B alive2/build -DCMAKE_BUILD_TYPE=Release -DBUILD_TV=1 \
  -DCMAKE_PREFIX_PATH=$PWD/llvm-build -DCMAKE_CXX_COMPILER=$PWD/llvm-build/bin/clang++
ninja -C alive2/build alive-tv

Then, from this repository, without any API key:

uv run pytest -q                                                     # includes the wrong rewrites that must be rejected
PYTHONPATH=. uv run python scripts/verify_all.py                     # re-proves every recorded result
PYTHONPATH=. uv run python scripts/fold_back.py results/spark-full-v1   # applies our rule to the recorded wins
PYTHONPATH=. uv run python scripts/replay.py win                     # replays a recorded win, Alive2 runs again
PYTHONPATH=. uv run python scripts/replay.py rejected                # replays a recorded rejection

To run the loop on one function, copy .env.example to .env, add a Meta Model API key, and cap the spending:

PYTHONPATH=. uv run python -m qed.loop bench/B/llvm-issue-215060 --run-id try-1 --max-total 1

Why you can trust the results

A superoptimizer is only as good as its proofs, so rigor is the core of the project, not an afterthought.

• What we prove is refinement, the exact correctness criterion LLVM uses for its own optimizations: wherever the original function has defined behavior, the rewrite returns the same result, and it never introduces new undefined behavior. For example, x + 1 > x on a signed int may become true: the two only differ at INT_MAX, where the original overflows and is undefined.
• Small trusted base: Alive2, Z3, and LLVM's IR semantics. Neither the LLM nor our own Python code is trusted.
• Strict reading of the prover: only Alive2's exact success message counts. Timeouts, unsupported features and approximations count as not proven.
• No sleight of hand: the source is the untouched clang -O3 output, the rewrite must keep the exact same signature, and every result is stored with the files that were proven and their hashes.
• We test the tester: a regression suite of deliberately wrong rewrites (abs(INT_MIN), oversized shifts, introduced division by zero…) that the pipeline must reject, every time.
• Reproducible: one command (scripts/verify_all.py) re-checks the corpus and re-runs the prover on every recorded result, checking the stored hashes.
• Honest numbers: one pinned LLVM commit, same target CPU on both sides, gains measured on the final assembly rather than on the IR.
• Measurement conditions: scripts/bench_cpu.py times each win on the real CPU (i7-9700K, then i7-12700H) with the same inputs in a predictable and in a random order, turbo off, core frequency measured at the start and end of every launch, median of 201 repetitions, 5 separate launches, and records these conditions with the results. It runs under WSL2, which executes natively on the CPU (no emulation): the spread between launches and the branch-free wins, used as controls, check the noise. The median spread is 0.9% on both CPUs, but some measures are noisier: over 2% on 61 of 316 on the i7-9700K and on 138 of 316 on the i7-12700H. The Muse Spark Open timings, on the i7-12700H, are noisier: median spread 1.8%, over 2% on 142 of 292. A win only counts if every launch clears the threshold, and the spread of each measure is in the results.

Benchmark

We evaluate on a corpus of small, pure integer functions, in three groups reported separately:

Group	What	Expected outcome
Control	Functions clang -O3 already handles	Little to gain: checks that we do not invent wins
Known misses	Optimizations reported as missed in LLVM issues and prior work, with a known better solution the model never sees	Reach that solution
Open	Functions, some adapted from real projects, with no known better solution	Unknown: nobody knows how many can be improved

Results

On the frozen corpus corpus-v1: 134 functions (24 control, 61 known misses, 49 open), up to 5 attempts each. Every win below is proven correct (refinement) by Alive2.

	Muse Spark	Muse Spark Open	LLM Compiler
Functions with a proven rewrite	132	127	80
Faster than clang -O3, gain estimated by llvm-mca	105	98	30
Kept: not undone by opt -O3, and over 5% in throughput or latency with neither worse	79	73	22
Confirmed on the i7-9700K	60	not timed	15
Confirmed on the i7-12700H	59	54	10
Confirmed on both CPUs	51	not timed: one CPU only	8
Cost	about $36.50, failed calls included	$9.72, on a Modal Shared Endpoint	none: local, 57 min on a GPU

Open weights. Muse Spark Open (meta-models/Muse-Spark-Open-816B-A42B) is the open-weight member of the Muse Spark family. It runs the same loop, prompts, feedback and 5 attempts, served by a Modal Shared Endpoint (--model muse-spark-open; every attempt records the model name the server returned, in results/spark-open-full-v1/). It gets close to Muse Spark at about a quarter of the cost: 98 wins against 105 before the CPU timings, 73 against 79 kept. Its answers are much shorter (median 3.5k output tokens against 19k for Muse Spark), and it gets more counterexamples from Alive2 (55 against 10). Its kept wins were timed on the i7-12700H only, not on the i7-9700K, so it has no "confirmed on both CPUs" number: 54 of 73 are confirmed there, against 59 of 79 for Muse Spark, and 3 are slower.

Each kept win is timed on each CPU in four ways: called as a function and pasted inline in a loop, each with predictable and with random inputs. Confirmed means over 5% faster in every launch in at least one of the four, and slower in none (under 0.98 in every launch). Otherwise a win depends on the context, shows no clear gain, or is slower. We chose this rule after seeing the data, so the four numbers of every win are in results/bench-9700k/ and results/bench-12700h/.

Each of Muse Spark's 51 wins, from its best timing to its worst. The best numbers are best cases, so read them with the worst ones under the axis:

Of the wins confirmed on both CPUs, Muse Spark has 39 known misses, 11 open functions and 1 control; LLM Compiler has 8 known misses. Some of these wins on open functions, as speedups over clang -O3 on the i7-9700K:

Function	Call, predictable	Call, random	Inline, predictable	Inline, random
rgb565-to-rgb888	1.40x	1.40x	2.99x	2.99x
libcxx-days-from-civil	1.54x	1.54x	1.51x	1.51x
hex-digit-value	1.80x	1.80x	1.09x	1.09x
opus-silk-lin2log	1.33x	2.36x	1.35x	2.43x
fletcher16-update	1.14x	1.14x	1.21x	1.21x

One win. libcxx-days-from-civil, adapted from libc++: days since 1970 from a year, month and day. Open group, first attempt, $0.14, 35 assembly instructions down to 26. clang -O3 handles negative years with a signed division by 400:

%11 = icmp slt i32 %8, 0
%12 = select i1 %11, i32 %10, i32 %8
%13 = sdiv i32 %12, 400
%14 = mul nsw i32 %13, -400

The year fits in 16 bits, and leap years repeat every 400 years. So Muse Spark counts leap years on the year plus 51200, a multiple of 400, which is always positive, and a constant corrects the total. The sign handling and the 400-year arithmetic disappear, and Alive2 proves the result correct (refinement):

%t7 = add i32 %t6, 51200
%t14 = lshr i32 %t7, 2
%t15 = udiv i32 %t7, 100
%t16 = lshr i32 %t15, 2

On the i7-12700H it runs 1.39x faster as a call and about 1.49x inline; the i7-9700K is in the table above. Full record: results/spark-full-v1/libcxx-days-from-civil.json.

One rejection. On linux-mult-frac, x / d * n + x % d * n / d in 32 bits, Muse Spark's attempt 4 widens to 64 bits, multiplies, then divides. It looks right, but the source wraps around in 32 bits. Alive2 finds the input that tells them apart: x = 9, n = 2747760640, d = 12 gives 271250773 in the source and 2060820480 in the rewrite. The attempt is rejected.

Controls. llvm-mca kept 2 of the 24 controls, which were supposed to have nothing to gain. rot-lr-xor is no reliable gain: as a call and inline, 0.88x and 1.05x on the i7-9700K, but 1.12x and 0.96x on the i7-12700H. align-up-pow2 shows a gain only inline, 1.14x and 1.11x, and about 1.00x as a call: it rediscovers a miss LLVM already tracks (#125354), so its control label looks wrong. Muse Spark Open, timed on the i7-12700H only, kept 3 controls: align-up-pow2 again (1.11x inline only), rot-lr-xor with no clear gain (1.04x), and umin-umax-clamp, 1.13x as a call and 1.04x inline, a control we had checked as already optimal on clang trunk.

What the feedback brings. On 30 functions drawn at random, we compared independent attempts, feedback with the verdict only, and feedback with the counterexample: 16, 18 and 18 kept wins. Only 4 functions change between the first and the last, 3 against 1, which is no evidence that memory helps. Counterexamples are rare: 10 in the whole Muse Spark run, on 8 functions, and they changed no result. So far Alive2 works as a judge that guarantees what we keep, more than as a teacher.

We have already reported our first findings to LLVM: #237771 and #237772.

Limits.

• Small pure integer functions, one pass per function, two CPUs. Timing runs under WSL2, where we cannot pin a physical core.
• The CPU matters: the verdict of 19 of Muse Spark's 79 kept wins differs between the two.
• llvm-mca alone is not enough: 26 of its 105 first wins fall to opt -O3 or to our rule, and 28 of the remaining 79 are not confirmed on both CPUs.
• Wins with a branch often depend on the inputs: median3-i32 is 6.11x inline with random inputs and 0.94x with predictable ones.
• The known solutions of 8 of the 61 known misses show no gain under our rule. We keep them in that group, since the corpus is frozen and no kept win comes from them.

What we built vs. what we use

Everything in this repository was written during the hackathon. We build on the shoulders of excellent open-source tools, which we call but do not modify:

Built by us	Used as-is
The propose → prove → repair loop and its orchestration	LLVM / clang (Apache 2.0 with LLVM Exceptions)
Prompts and counterexample feedback	Alive2 (MIT) and Z3 (MIT)
The rigor layer: strict proof parsing, signature checks, verifier regression suite	Meta's Muse Spark model (and Muse Wonder, in experiments), via the Meta Model API; Meta's open-weight Muse Spark Open, via a Modal Shared Endpoint
The benchmark corpus, its evaluation and its charts	Meta's LLM Compiler, run locally with llama.cpp
Spending controls: hard cap per run, response cache	llvm-mca for performance estimates
Measurement harness (scripts/bench_cpu.py) and result checks (scripts/fold_back.py)	The openai Python client, only as the HTTP client of the Meta Model API and of Modal (requests go to Meta models, no OpenAI model is used)

For the demo video only, we also use Manim for the animations and Kokoro for the AI-generated voice.

Prior art

• Souper: a superoptimizer for LLVM IR based on exhaustive, solver-driven search.
• STOKE: stochastic search over x86-64 assembly.
• AlphaDev (DeepMind): reinforcement learning that discovered faster sorting routines.
• Meta LLM Compiler: LLMs trained on LLVM IR and assembly.

Our contribution: use an LLM as the search heuristic, feed the prover's verdicts back to it, and publish only what is formally proven.

Team

• Benoit (@benoithms)
• Jules (@julesreyn)

License

MIT

Built with LLM Compiler.