Verified self-play for code optimization
I'm working with Professor Gabriel Poesia to extend Token Games to verified self-play for code optimization. Models propose and challenge optimizations in real LLVM code. An improvement only counts if alive2 proves it correct and paired timing shows it beating LLVM's -O3 on real hardware.
- Role
- Graduate researcher, with Professor Gabriel Poesia
- Timeline
- September 2026 — ongoing
- Stack
- C++, LLVM API, Python, alive2, native timing, llvm-mca
- Status
- LLVM experiments; extending the work to PyTorch
The problem
A model can make code shorter without making it faster, and it can pass every test while introducing undefined behavior. If we're going to reward models for finding optimizations, the reward has to mean something. I wanted to know whether formal verification and real timing could make self-play useful on code people actually run.
What I built
I built the duel harness and a C++ slicer using the LLVM API to process 69 MB of IR from ten production codebases, including re2, SQLite, Brotli and zstd. The loop runs differential tests, checks rewrites with alive2, and measures them with paired native timing against -O3. Interleaving the timings brought run-to-run noise below 0.7%.
I tested single models, alternating duels, ensembles, and a proposer that has to bring a verified solution before asking another model to solve its puzzle. The comparisons use equal model-call budgets, so a game has to earn its extra machinery.
Results
After replacing instruction count with real timing, I found and formally verified two re2 fragments that ran 14–16% faster than -O3 on my Mac. They remove a redundant overflow check in inlined vector growth. The reduced pattern was still missed by LLVM trunk when I checked it on September 30; an upstream issue is drafted, but hasn't been filed.
The evaluation was as much of the work as the search. Models found rewrites that improved the instruction-count proxy while making the generated machine code worse. Tests alone also missed undefined behavior. Those are exactly the cases where a reward would teach the wrong lesson.
On the latest 50 fresh fragments, the duel found three correct speedups, matching the best single model and the ensemble. The proof requirement kept every accepted result correct. I'm now extending the work to PyTorch and looking for tasks where interaction between models helps them find more.
What I'd do differently
The biggest lesson was that the evaluator shapes what the model learns to do. Formal verification and real timing made the search useful, because the models could no longer win by shortening code that ran more slowly. I'd keep that discipline as the tasks get larger. The re2 results are fragment-level speedups; the next step is to see what survives in a full program.