Natural deduction as a sandbox for capability emergence from RL.

In the inference-scaling paradigm, model output improves with inference cost: reasoning models spend more compute at test time to solve harder problems (https://arxiv.org/abs/2408.03314). For now, most of that improvement comes from recombining knowledge already present in the training data. But once models reach the frontier of what is known, further capability growth will be governed by the scaling laws of creating new knowledge, not learning existing knowledge. Understanding how and when models can do this — behaviourally and mechanistically — is therefore critical for both forecasting capabilities and preparing safety techniques for them.

There are surprisingly few settings where "new knowledge" can be defined in a controlled way. Studies at frontier scale run into a basic confound: the base model has seen essentially all human mathematical writing, so "the model discovered nothing new" and "the model discovered nothing new relative to training data that covers everything" cannot be told apart (https://arxiv.org/abs/2504.13837). Propositional natural deduction is such a setting. It has a perfect verifier, a training distribution we specify completely, and a natural difficulty gradient — rules that can be checked locally versus rules that require tracking open subproofs. Crucially, a small transformer trained from scratch on short synthetic proofs can be proven unable to reach the held-out theorems, so any success cannot be explained by hidden prior exposure.

In this project we use natural deduction as a sandbox for new-knowledge generation. We train a small model from scratch on short synthetic proofs — the analog of textbook drills — hold out nontrivial theorems including exercises from Halbach's Logic Manual, and ask three questions: whether RL against the verifier reaches theorems that no amount of supervised training could (bootstrapping); whether the proofs it discovers are as informative as human-authored training data (data equivalence); and whether feeding each round's discoveries into the next round's training compounds or saturates (compounding). Because the sandbox is fully specified, the role of the verifier, the training distribution, and the iteration structure can each be varied independently — exactly the knobs frontier experiments cann

If we are able to demonstrate and dissect knowledge creation in this setting, this wconstitute a model organism forystem small enough to studymechanistically, in which a model measurably exceeds its training distribution. This would be useful well beyond the immediate result — for interpretability (watching a genuinely new capability form),n (detecting when a model ismoving beyond its training distribution), and for developing mitigation techniques against unwanted emergent capabilities before they appear at scale. This would be a strong paper.

Now that models have reached the frontier of human knowledge, the capabilities that matter for safety will increasingly be discovered by models rather than learned from us. We currently have no testbed for the tools that would detect and control this. Natural deduction provides one: the boundary of what the model can do is known exactly, so we can watch a capability being discovered with full ground truth. This lets us develop and validate detection tools — probes and behavioural signatures of a model moving beyond its training data — and control tools — interventions that stop an unwanted capability from compounding — before they are needed at scale.

Mentees will work collaboratively in small sub-teams to derive theoretical results and design and implement experiments. I expect to spend time co-working together with mentees early on in the project (1-2 weeks), to craft a project plan, help run experiments, and work through the theory.

We will then collaboratively construct a more detailed project plan, and mentees will largely take ownership of the project, including conference submission. We will continue to meet weekly where I will make suggestions about next steps and co-work on bottlenecks when needed.

1. Be able to implement nanoGPT scale models from scratch.

2. Ability to implement basic intepretability techniques.

3. Familiarity with formal logic is not required but is a plus.

4. Ability to implement simple custom RL pipelines.

Anything can work, but I have a mild preference for the Bay area so we can co-work in person and I can provide snacks.