So that’s my theory: it’s about pretraining data quality, not verifiability.
These seem highly entangled to me rather than a dichotomy to choose from. Verifiability is what allows for high-quality training data in many situations, especially once you get beyond scraping the internet and into the realm of synthetic data. It also allows for clean attribution of the reward signal in an RL environment.
Math has some of the cleanest verifiability of any domain, especially with tools like Lean, which is far more robust than LLMs judging themselves. Not only do you have an external oracle for a correct answer, the entire chain of inferences leading to it can be adjudicated.
You may be interested in: DeepSeek-R1: Incentivizing Reasoning Capability in LLMs via Reinforcement Learning
Abstract: General reasoning represents a long-standing and formidable challenge in artificial intelligence. Recent breakthroughs, exemplified by large language models (LLMs) and chain-of-thought prompting, have achieved considerable success on foundational reasoning tasks. However, this success is heavily contingent upon extensive human-annotated demonstrations, and models’ capabilities are still insufficient for more complex problems. Here we show that the reasoning abilities of LLMs can be incentivized through pure reinforcement learning (RL), obviating the need for human-labeled reasoning trajectories. The proposed RL framework facilitates the emergent development of advanced reasoning patterns, such as self-reflection, verification, and dynamic strategy adaptation. Consequently, the trained model achieves superior performance on verifiable tasks such as mathematics, coding competitions, and STEM fields, surpassing its counterparts trained via conventional supervised learning on human demonstrations. Moreover, the emergent reasoning patterns exhibited by these large-scale models can be systematically harnessed to guide and enhance the reasoning capabilities of smaller models.
See also: Training Verifiers to Solve Math Word Problems
We show that, compared to a finetuning baseline, the use of verifiers results in approximately the same performance boost as a 30x model size increase, and that verifiers scale significantly better with increased data.
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.