I’m talking about proof-based advanced math in natural language. This activity has never been “verifiable” until Lean-autoformalization became possible. And I claim that the models were already remarkably good at proof-based advanced math in natural language before Lean-autoformalization became possible.
Indeed, it seems pretty implausible to me to say that the order of events during training / recent history is that first the models become capable of doing Lean-autoformalization of natural-language proofs, and only then the models become good at natural-language proofs, thanks to RLVR-via-autoformalization. Is that what you think? To me, that really seems like the wrong order. Lean-autoformalization of a natural-language proof is hard, and seems to require access to a model that is already very good at natural-language proofs.
Lean-autoformalization is just a particularly strong form of verifiability. I do not think it’s a prerequisite for strong proof skills (and wasn’t used in the papers I linked).
I do think “verifiable” is highly relevant, even if it can be squishier than formally verified. Compare a question like “Is this natural language proof valid?” to “Is this story well written?” Which is easier to train on? If you can create a scoring function for stories that works as reliably as judging the validity of a natural language proof, then I’d predict you could train LLMs to write really good stories.
The pretraining data is the baseline to bootstrap from. From there, it’s a matter of providing training signals for the model to learn from, and verifiable domains provide clean signals. Even if the pretraining data is rather error-ridden, those errors get averaged away in next-token prediction unless they’re systematic.
those errors get averaged away in next-token prediction unless they’re systematic.
Sorry if I’m misunderstanding, but aren’t they always systematic in cases we care about? If you look at (say) people writing papers about the neuroscience of schizophrenia, there are a zillion mutually-incompatible ideas and schools of thought. It’s not the case that everyone is saying “truth plus random noise”, so all you need is enough data and you can average it out to get the true neuroscience of schizophrenia, right?
Compare a question like “Is this natural language proof valid?” to “Is this story well written?” Which is easier to train on? If you can create a scoring function for stories that works as reliably as judging the validity of a natural language proof, then I’d predict you could train LLMs to write really good stories.
Yes this is exactly my point. It is much easier to create an LLM that says whether a natural-language proof is correct, than an LLM that says whether a fiction story is good. And I’m asking the question: Why the difference? You want to say “because math is verifiable”, and I’m drilling into that and saying it doesn’t make sense. What does “math is verifiable” mean to you, and what exactly is the path from “math is verifiable” to “the LLM can say whether a natural-language proof is correct”?
The answer to that question can’t involve RLAIF, because you can’t even start RLAIF until you already have an LLM that says whether a natural-language proof is good. It’s a chicken-and-egg thing.
You CAN say “the LLM can say whether a natural-language proof is correct, including e.g. noticing subtle flaws in a proof’s use of p-adic Hodge theory, because we did RLVR on its ability to do high school contest math problems with right and wrong answers, along with RLVR on algebraic manipulation tasks that we could check with SymPy, etc.” At least, that hypothesis would not have a chicken-and-egg problem. But it strikes me as a very far-fetched answer to the question, that cannot possibly be hitting the nail on the head. Those two kinds of things are very very different! Why would there be such strong transfer from one to the other? I’m open to nonzero transfer, I just expect it to be very indirect and high-level. Whatever the LLM knows about p-adic Hodge theory that enable it to catch mistakes in proofs, it didn’t get that from RLVR on math problems with right and wrong answers. See what I mean?
but aren’t they always systematic in cases we care about?
In unverifiable domains, yes. That’s largely what I interpret “unverifiable” to mean. By “math is verifiable”, I’m describing a property of the domain, not the LLM. A disputed result can, in principle, be decomposed into local steps small enough that any trained mathematician (or automated proof checker) will agree on each step. When mathematicians disagree, the disagreement is traced to a specific step that gets settled. In schizophrenia research, there are no similar resolvable cruxes to surface, so disagreeing camps continue publishing and systematic error builds up without a correcting mechanism.
Verifiability of a domain tends to correlate with the quality of the training data, but it’s not the same thing. Math lends itself to checks that are not LLMs, like answer keys, computer algebra, and Lean. RL against those checks grounds the model in something consistent and correct, and the training pressure also reaches the LLM’s reasoning. Any single right answer can sit on an invalid step, but across broad varieties of problems, RL reinforces valid reasoning. Lean isn’t required for this and likely came later, but it can grade the whole chain, which makes the grounding cleaner. This is why the transfer from right-answer RLVR to proof-checking that Beren describes doesn’t feel that far-fetched to me, and also why I’d predict math reasoning to be repairable even from a contaminated corpus (as in Hastings’ proposed experiment), even one with coherently wrong results. A wrong pocket can survive in math if it’s isolated enough (Mochizuki’s disputed abc proof is perhaps the human version), but the odds of correction scale with its overlap with the rest of mathematics, and whatever matters broadly overlaps a lot. A contaminated psych corpus has very little to repair against. Would you predict differently?
Knowledge of p-adic Hodge theory specifically will mostly come from pretraining. A subtle flaw in a p-adic Hodge theory proof boils down to some simpler step failing, like a theorem applied where its hypotheses don’t hold. Knowing the hypotheses comes from pretraining and/or context, while RLVR trains the habit of checking them. Such rigor is only trainable in domains where something exists to be rigorous against: an external check that can signal wrongness. Math is ideal here. Psych is not.
I’m talking about proof-based advanced math in natural language. This activity has never been “verifiable” until Lean-autoformalization became possible. And I claim that the models were already remarkably good at proof-based advanced math in natural language before Lean-autoformalization became possible.
Indeed, it seems pretty implausible to me to say that the order of events during training / recent history is that first the models become capable of doing Lean-autoformalization of natural-language proofs, and only then the models become good at natural-language proofs, thanks to RLVR-via-autoformalization. Is that what you think? To me, that really seems like the wrong order. Lean-autoformalization of a natural-language proof is hard, and seems to require access to a model that is already very good at natural-language proofs.
Lean-autoformalization is just a particularly strong form of verifiability. I do not think it’s a prerequisite for strong proof skills (and wasn’t used in the papers I linked).
I do think “verifiable” is highly relevant, even if it can be squishier than formally verified. Compare a question like “Is this natural language proof valid?” to “Is this story well written?” Which is easier to train on? If you can create a scoring function for stories that works as reliably as judging the validity of a natural language proof, then I’d predict you could train LLMs to write really good stories.
The pretraining data is the baseline to bootstrap from. From there, it’s a matter of providing training signals for the model to learn from, and verifiable domains provide clean signals. Even if the pretraining data is rather error-ridden, those errors get averaged away in next-token prediction unless they’re systematic.
Sorry if I’m misunderstanding, but aren’t they always systematic in cases we care about? If you look at (say) people writing papers about the neuroscience of schizophrenia, there are a zillion mutually-incompatible ideas and schools of thought. It’s not the case that everyone is saying “truth plus random noise”, so all you need is enough data and you can average it out to get the true neuroscience of schizophrenia, right?
Yes this is exactly my point. It is much easier to create an LLM that says whether a natural-language proof is correct, than an LLM that says whether a fiction story is good. And I’m asking the question: Why the difference? You want to say “because math is verifiable”, and I’m drilling into that and saying it doesn’t make sense. What does “math is verifiable” mean to you, and what exactly is the path from “math is verifiable” to “the LLM can say whether a natural-language proof is correct”?
The answer to that question can’t involve RLAIF, because you can’t even start RLAIF until you already have an LLM that says whether a natural-language proof is good. It’s a chicken-and-egg thing.
You CAN say “the LLM can say whether a natural-language proof is correct, including e.g. noticing subtle flaws in a proof’s use of p-adic Hodge theory, because we did RLVR on its ability to do high school contest math problems with right and wrong answers, along with RLVR on algebraic manipulation tasks that we could check with SymPy, etc.” At least, that hypothesis would not have a chicken-and-egg problem. But it strikes me as a very far-fetched answer to the question, that cannot possibly be hitting the nail on the head. Those two kinds of things are very very different! Why would there be such strong transfer from one to the other? I’m open to nonzero transfer, I just expect it to be very indirect and high-level. Whatever the LLM knows about p-adic Hodge theory that enable it to catch mistakes in proofs, it didn’t get that from RLVR on math problems with right and wrong answers. See what I mean?
In unverifiable domains, yes. That’s largely what I interpret “unverifiable” to mean. By “math is verifiable”, I’m describing a property of the domain, not the LLM. A disputed result can, in principle, be decomposed into local steps small enough that any trained mathematician (or automated proof checker) will agree on each step. When mathematicians disagree, the disagreement is traced to a specific step that gets settled. In schizophrenia research, there are no similar resolvable cruxes to surface, so disagreeing camps continue publishing and systematic error builds up without a correcting mechanism.
Verifiability of a domain tends to correlate with the quality of the training data, but it’s not the same thing. Math lends itself to checks that are not LLMs, like answer keys, computer algebra, and Lean. RL against those checks grounds the model in something consistent and correct, and the training pressure also reaches the LLM’s reasoning. Any single right answer can sit on an invalid step, but across broad varieties of problems, RL reinforces valid reasoning. Lean isn’t required for this and likely came later, but it can grade the whole chain, which makes the grounding cleaner. This is why the transfer from right-answer RLVR to proof-checking that Beren describes doesn’t feel that far-fetched to me, and also why I’d predict math reasoning to be repairable even from a contaminated corpus (as in Hastings’ proposed experiment), even one with coherently wrong results. A wrong pocket can survive in math if it’s isolated enough (Mochizuki’s disputed abc proof is perhaps the human version), but the odds of correction scale with its overlap with the rest of mathematics, and whatever matters broadly overlaps a lot. A contaminated psych corpus has very little to repair against. Would you predict differently?
Knowledge of p-adic Hodge theory specifically will mostly come from pretraining. A subtle flaw in a p-adic Hodge theory proof boils down to some simpler step failing, like a theorem applied where its hypotheses don’t hold. Knowing the hypotheses comes from pretraining and/or context, while RLVR trains the habit of checking them. Such rigor is only trainable in domains where something exists to be rigorous against: an external check that can signal wrongness. Math is ideal here. Psych is not.