Our "Bitter Lesson Paper" - h1 - is finally out on arXiv.
arxiv.org/abs/2610.35962
Here is an excellent account by @SkanderMoalla on how this research came about. TL;DR:
- we tried to study a (slightly) fancy idea to scale at test time (asymmetric self-play)
- each time we carefully tried to adjust and simplify baseline harnesses we washed out our initial gains
- we ended up with h1: a simple baseline formal proving harness that is SOTA (and solved 4 extra Erdos problems) - plus some valuable lessons learned.
(Of course, this was all done way before a lot of recent mathAI happenings; alas, we were > 30 days on hold on arXiv.)
arxiv.org/abs/2610.35962
Here is an excellent account by @SkanderMoalla on how this research came about. TL;DR:
- we tried to study a (slightly) fancy idea to scale at test time (asymmetric self-play)
- each time we carefully tried to adjust and simplify baseline harnesses we washed out our initial gains
- we ended up with h1: a simple baseline formal proving harness that is SOTA (and solved 4 extra Erdos problems) - plus some valuable lessons learned.
(Of course, this was all done way before a lot of recent mathAI happenings; alas, we were > 30 days on hold on arXiv.)
arxiv.org h1: A Taste of the Bitter Lesson in Automated Theorem Proving While progress in informal mathematics has come largely from scaling the chain-of-thought and agentic reasoning of frontier language models, formal theorem proving has increasingly relied on... After 30 days on hold, h1 is finally on arXiv! Here’s how it came to be and, more importantly, the takeaways.View quoted post on X
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!
