# qed-superopt - **Event:** [Meta Global AI Developer Hackathon](https://cerebralvalley.ai/e/meta-ai-developer-hackathon) - **When:** Oct 26, 12:00 PM – Nov 4, 9:00 PM (EST) - **Where:** Online - **Team:** [Jules Reynaud](https://cerebralvalley.ai/u/julesreyn), [Benoit THOMAS](https://cerebralvalley.ai/u/defzefjzf) - **GitHub:** https://github.com/benoithms/qed-superopt - **Demo video:** https://youtu.be/q5jdGRf9M10 - **Gallery:** https://cerebralvalley.ai/e/meta-ai-developer-hackathon/hackathon/gallery - **Page:** https://cerebralvalley.ai/e/meta-ai-developer-hackathon/hackathon/gallery/3687 Compilers are excellent, but not perfect: even at clang -O3, their maximum optimization level, they still miss faster ways to compute the same thing, and finding these missed optimizations by hand is slow expert work. An AI model can propose faster versions, but a compiler cannot accept a rewrite on trust: a single wrong one silently breaks every program built with it. qed-superopt removes the need for trust. It lets an AI optimize code past clang -O3, and it accepts nothing without a mathematical proof. Muse Spark invents a faster version of a function. Alive2, a formal verifier, checks it for every possible input. If the rewrite is wrong, the model gets the exact input that breaks it and tries again. Whatever comes out is proven correct, not just tested. And it works. On a frozen benchmark of 134 functions, Muse Spark produced a proven rewrite for 132. 51 of them are confirmed faster on two real CPUs. For 39 of those, experts already knew a better solution existed: the AI reached a faster result without ever seeing it. In our best example, a date function adapted from libc++, it removed 9 of 35 instructions and ran up to 1.54x faster, on its first attempt, for 14 cents. Meta's open-weight model does it too. Muse Spark Open, served on a Modal Shared Endpoint, ran the same loop on the same benchmark: a proven rewrite for 127 functions, and 54 confirmed faster on a real CPU (timed on one CPU so far), for 9.72 dollars. The whole Muse Spark run cost about 36 dollars, roughly 70 cents per confirmed win. That changes the economics of compiler work: hunting for missed optimizations is usually slow expert labor, and here it ran across a whole benchmark in days. The payoff compounds, because the compiler stack behind Chrome, Android, PlayStation games and Rust programs only has to learn a pattern once for every program that contains it to benefit. We have already reported our first findings to LLVM, issues 237771 and 237772. The idea is simple: let the model be creative, and let a proof decide. We have started taking it from isolated functions to real programs: our first whole-program tests, on PNG decoding and on SQLite, found proven rewrites in real code but no reliable speedup of the whole program yet, so the next step is to give the model larger code to rewrite, not just small functions. Everything can be checked. One command proves all 1,252 recorded proofs again, and we publish what did not hold, along with the limits, in the README and the video. We built the propose, prove and repair loop, the prompts, the corpus and the measurements during the hackathon. We use LLVM, Alive2, Z3 and Meta's models as they are. ## More from Meta Global AI Developer Hackathon - [Vinayak](https://cerebralvalley.ai/e/meta-ai-developer-hackathon/hackathon/gallery/3684) - [PentCloud](https://cerebralvalley.ai/e/meta-ai-developer-hackathon/hackathon/gallery/3685) - [Astodev](https://cerebralvalley.ai/e/meta-ai-developer-hackathon/hackathon/gallery/3686) - [Medicaid_auto](https://cerebralvalley.ai/e/meta-ai-developer-hackathon/hackathon/gallery/3688) - [AutoFTE](https://cerebralvalley.ai/e/meta-ai-developer-hackathon/hackathon/gallery/3689) - [DYTL](https://cerebralvalley.ai/e/meta-ai-developer-hackathon/hackathon/gallery/3690) --- Markdown version of https://cerebralvalley.ai/e/meta-ai-developer-hackathon/hackathon/gallery/3687. Site index for agents: https://cerebralvalley.ai/llms.txt · full text: https://cerebralvalley.ai/llms-full.txt