Comment Permalink
7836
17
I appreciate the info on LLM training and will edit that footnote.
My claim is that, if we want to understand how LLMs can construct correct natural-language proofs that involve abstruse mathematical objects like the de Rham cohomology group, a big part of the answer is that that approximately every time anyone has ever written down anything about the de Rham cohomology group, that thing they wrote has been true. So the LLM emerges from pretraining with an tendency to say true things, and only true things, about the de Rham cohomology group, and the same applies to everything else in advanced math. This is very very different from most other topics, like anxiety or middle school classroom discipline. Of course, a tendency to say true things and only true things about the de Rham cohomology group isn’t enough, and I’m certainly not questioning the importance of post-training for surfacing that tendency at the appropriate times, and honing it, etc.
Basically, I think you’re being insufficiently curious about the part where you said “this transfers quite well to proof-based arguments also”. It seems to me that AIME problems and computer algebra etc. are really quite different from properly using the de Rham cohomology group in a natural-language proof. I know far less than you about LLM training, but I’d be a bit surprised if LLM training today involves even one RLVR task that requires proper use of the de Rham cohomology group, much less many of them, or if they do I’d be surprised if that were critical as opposed to merely helpful. So I don’t think we would see “transfer to proof-based arguments” if there wasn’t already a whole preexisting edifice of correct proof-based arguments involving the de Rham cohomology group along with everything else, latent in the base model, and post-training merely needs to dredge up that edifice, rather than build it piece-by-piece. There’s just not enough bits to build it piece-by-piece, plus I don’t even know how that would work. (
40
Just piggybacking on Beren's comment; I agree that you severely underestimated the amount of effort that goes into explicit optimization on math capabilities. In particular, I would actually put odds at like 85% that LLM training today involves several RLVR tasks that require proper use of the de Rham cohomology group.
However, your broader point totally stands; there's no way to do stuff with RLVR unless pass rate is nonzero, so the initial performance on such problems has to come from somewhere nontrivial. Most effort towards producing RLVR "environments"...
223
This is an interesting point! I am legitimately unsure here. I think this could have some effect in that there is less 'noise' in the training data (probably midtraining) math data than otherwise (although certainly people write incorrect or confusing math on the internet!). I think this is a broader point in that most information the models read on the internet is likely correct in that it is basic and undebated. I.e. very few people are writing that the capital of France is Berlin, that water is made of argon and copper, and that the battle of Hastings was fought in 1754 etc. LLMs are also very resilient to 'noise' in that because they see just so many variants of the same information that the occasional crazy statement in pretraining just doesn't perturb their world model much. Definitely though in pretraining you would obviously expect areas where human discussion is just a mountain of slop to produce slop in return (there is also an interesting experiment lurking here where we train LLMs on increasing proportions of synthetic 'false math' data and see to what extent they can still generalise real math correctly).
I do think you underestimate the extent to which people have explicitly optimised the mid-training and RLVR data for exactly this kind of higher math. Together the labs are paying billions of dollars to PhD students and human experts precisely for questions, solutions, reasoning traces etc on graduate level math. I don't know enough to say for sure that this includes de Rham but I would not be surprised at all if there is good amount produced and directly trained on there. Similarly, it is actually quite easy to run Lean autoformalization if you have a list of existing questions and proofs which you can extract from e.g. math textbooks or grad students then you can directly setup and RLVR environment to just successfully formalise the known proof target starting from some basic premises. You don't even need answers here as long as you can programmatic
Follow-up to: “LLMs are (still) mostly powered by imitative learning, not RL”
[Edited a bit since publishing, see changelog at the bottom.]
A common take I’ve been hearing is: “LLMs are especially good at math (compared to how good they are at other things)[1] because math is easy to verify”. But that story doesn’t make much sense to me.
My main complaint is that, for advanced math, the verifier is an LLM.[2] So really, the phrase “math is easy to verify” amounts to “LLMs are very good at judging math arguments”. But that’s begging the question! Why are pretrained LLMs so much better at judging math arguments than judging, say, fiction writing? We still need an answer.
So here’s a different theory, in the framework of my earlier post “LLMs are (still) mostly powered by imitative learning, not RL”:
LLMs are especially good at math because almost everything in the math literature is correct. Read a random sentence in a random math paper in the research math literature, and you can be >99% confident that the sentence is true. So if LLMs do what they do best—imitative learning—then in the limit, they’re going to be almost always making correct deductions in their mathematical reasoning. They just need a little sprinkling of curated mid-training data and/or RL to hone their metacognitive strategies and so on.
So that’s my theory: it’s about pretraining data quality, not verifiability.[3] Now let’s apply that theory to other areas.
What about code? Well, for almost all the code that you’ll find on the internet, it compiles and runs and basically does what you’d expect it to do. So if LLMs do what they do best—imitative learning—then in the limit, they’re going to be almost always writing code that compiles and runs and basically does what you’d expect it to do. But code on the internet is also often ugly, buggy, inefficient, etc. So companies need to solve that problem with curated mid-training data and/or RL. This is a bigger challenge for code than it is for math, but companies have spent the past few years pouring a ton of effort into it, and they’ve made impressive progress.
What about other fields? In many fields, the research literature is kinda a dumpster fire. There’s plenty of true and valuable stuff, stirred into a sea of such falsehoods and confused ideas that reading them will make you stupider. So if LLMs do what they do best—imitative learning—then in the limit, they’re going to spit out tons of confused nonsense with occasional insights, with no labels on which is which. Just like the humans. You might reply: “Perhaps this problem is fixable via curated mid-training data and/or RL?” Maybe. But if so, I think we should expect it to be much more of a challenge than it has been for code, let alone math.
How does this theory bear on the “LLM Recursive Self-Improvement” debate?
Well…
I shall leave readers to reach their own conclusions.
Likewise,
How does this theory bear on the “LLM Automated Alignment Research” debate?
Same idea here. Again, readers may judge for themselves.
CHANGELOG:
A few hours after publishing, I changed the first few paragraphs, in order to: (1) acknowledge that RLVR on math questions with right answers is a thing (whoops I forgot, that’s embarrassing); (2) delete the claim that companies don’t do much RL-on-math, which was a vague memory that an expert in the comments section (Beren) has confirmed is false, whoops; (3) fix my incorrect description of the IMO paper. Thanks various people for pushback, especially Thane Ruthenis, Shreyas Sharma, and Beren in the comments, and singularvessel on X.
Next day (Sept 19): Moved some words from footnote 1 into the main text, to make sure people don’t miss it.
Oct 9: Added another sentence into Footnote 1, with more evidence against RLVR-via-autoformalization being an important part of how LLMs got good at math proofs.
I’m not comparing LLMs to human mathematicians in this post; I have opinions but that’s a separate debate.
In the case of RL-for-math, there’s RLVR on questions with right and wrong answers (e.g. the AIME dataset + more examples in Beren’s comment), but for more advanced proof-based challenges, the RL is mostly-or-entirely “RLAIF” (RL from AI Feedback), not “RLVR” (RL with Verifiable Rewards).
(The latter would have to involve some mechanical checker, like the Lean formal verifier, in the RL loop. Beren says that companies are doing that today, but I think that LLMs were already clearly especially good at proof-based advanced math (compared to how good they are at other things) before autoformalization-in-the-loop RLVR would have been feasible.)
(Indeed, it seems very far-fetched to me to think that you could build a Lean-autoformalizer of natural language proofs unless you already had access to a model that was pretty damn good at natural language proofs. So an RLVR-centric explanation of LLM math proof capabilities seems wrong to me on chicken-and-egg grounds.)
(ADDED OCT 9: also, ex-OpenAI post-training engineer Will DePue says: “…these results aren't using formal methods aggressively…”, in a discussion of the Navier–Stokes & October 6th proofs.)
Another place that “verifiability” matters is at inference time: the LLM might notice errors in its own chain-of-thought, or there can be more complicated scaffolds as in this paper about the International Math Olympiad. Same thing: the judge is an LLM.
Of course, “verifiability” is relevant to how humans wound up with such a high-quality math literature. So verifiability-of-math is indirectly related to LLM math competence. Just not directly.