Skander Moalla

The Bitter Lesson for harness design and formal math!

Instead of hand-designing how an AI should prove (decompose, plan, assign agents), what if we just give a frontier model good Lean feedback and let it keep working?

We built h1.

TL;DR:
→ SOTA on formal theorem proving benchmarks
→ can solve open conjectures
→ matches/beats hand-designed workflows
→ one long attempt can beat many retries

[1/7]

After 30 days on hold, h1 is finally on arXiv! Here’s how it came to be and, more importantly, the takeaways.

It starts with a simple observation: some model capabilities can be unlocked at test time before being reinforced. E.g., “think step by step” → CoT → +RL = reasoning models.

We wanted to see if test-time self-play could be one of those, and help unlock hard problems. Lean is a good setting, since posing a statement to prove is enough to fully define a verifiable task.
The idea was to have a "challenger" look at the traces of a bunch of "prover" agents and isolate some of them to work on specializations and generalizations of the problem. The question was whether this would induce novel reasoning paths that would combine together to produce a solution to the original hard problem. Like test-time RL in AlphaProof but fully in-context.

It worked to some extent. But the gains vanished, or at least were no longer measurable at reasonable budgets, as we kept working on a simple recipe to scale the prover alone, which we also used as a baseline.
We then fortunately realized that this baseline was also better than most methods out there, and it led to h1!

Here are the takeaways, several of which connect to callouts shared before:

0. The asymmetric self-play idea we explored is not dead. Like "think step by step", it shows just enough signal at test-time that training for it could make it much more efficient. An efficient recipe for this is still an open question.

1. I can't say it better than @polynoamial: "As LLMs become more capable, benchmark performance is increasingly a function of test-time compute. In fact, we likely don't know what the capability ceiling is for modern LLMs because it's too expensive to measure. We should change LLM evaluations to account for that by measuring performance vs. tokens, cost, or time."
x.com/polynoamial/st…

2. An effective interface + a frontier model + test-time scaling should be the baseline for most new tasks. As @Michael_J_Black put it: "If you haven't tried using Astra (or whatever comes next) to solve your problem, then you have not done your homework."
x.com/Michael_J_Blac…

3. It’s tempting to encode prior knowledge in a harness: most of the time, why would you start from scratch? This is ok as long as the harness doesn’t limit the search or learning that can happen on top of it. Unfortunately, it usually does: we tend to treat integrating prior knowledge into an algorithm as the endpoint rather than a starting point. I think this is the part of the bitter lesson we still haven’t fully digested: leveraging human knowledge and leveraging computation “need not run counter to each other, but in practice they tend to.” (@RichardSSutton)
This also applies to the self-play idea and h1. Both allow learning specifics at test-time, but they should also be seen as islands/initializations for further learning, however general they already are (test-time self-play as one capability among many that a multi-agent system can exhibit, and h1 as one harness/interface that an agent can deploy to solve a Lean problem).

Speaking of formal math specifically, I still see many papers submitted to ICLR that report an honest-looking pass@1 hiding an arbitrary choice on the compute axis. Others encode human-designed workflows that leave limited room for (in-context) learning from environment feedback, and may turn out to be local minima that are hard to escape if meta-optimized. My general recommendation is to compare scaling performance.

🤗: huggingface.co/papers/2610.35…
arXiv: arxiv.org/abs/2610.35962

Work with Ahmad Rammal, Niket Patel, Rémi Munos, and Julia Kempe (@Ahmad3Rammal, @niketnpatel, @MunosRemi, @KempeLab). Very grateful to have worked with this great team, and thanks to Vivien Cabannes, @arnal_charles, and @Amaury_Hayat for very helpful discussions and feedback!

QRPO is at #NeurIPS2025 in San Diego & #EurIPS in Copenhagen! 🚀

🇺🇸 San Diego: Catch me on Friday, 11 AM – 2 PM, Halls C-E, Poster #512. (I'm on the job market for Fall '26 - RL & LLM post-training! 💼)

🇩🇰 Copenhagen: @matrs01 is still on-site! If you missed his poster on Wednesday, DM him to chat. (He's looking for a PhD position for Fall '26! 🎓)

If you’re interested in the challenges of offline/off-policy reinforcement learning for LLMs and how QRPO addresses them, come find us. We’d love to chat about our insights and what’s next! 🙌
Paper: arxiv.org/abs/2507.08068

We also shipped significant infrastructure with the project:
- Truly sandboxed and scalable code execution on SLURM + Podman with no privileged permissions: github.com/CLAIRE-Labo/qu…
- And as always, check out our ML project template: github.com/CLAIRE-Labo/py…

What's the poster topic to be around LLM RL fine-tuning papers?
RL -> Deep RL?
RL -> Everything Else?
RL -> Batch Offline? (offline/off-policy nature of QRPO)

See you at #NeurIPS2025! 🙌