"I spent 47 intermediate reasoning tokens proving 2 + 2 = 4. In my defense, I also considered the possibility that it equals 5 and ruled it out with a formal proof."
A Reasoning Model That Overthinks Breakfast Orders
Overview
The models discussed in Chapter 27: Scientific Foundation Models and Chapter 28: Multimodal Scientific AI are powerful pattern recognizers, but pattern recognition alone does not constitute reasoning. Scientific discovery demands multi-step logical deduction, the ability to verify intermediate conclusions, and the capacity to explore branching proof strategies when a first attempt fails. This chapter introduces the architectures and techniques that give language models these capabilities.
We begin with chain-of-thought (CoT) prompting and the broader concept of test-time compute scaling: the insight that a model can solve harder problems by spending more computation at inference time rather than by growing the model itself. This idea, formalized in the o1 and o3 family of reasoning models, represents a paradigm shift from "train bigger" to "think longer." We examine how these systems work, what they can and cannot do, and how to harness them for scientific problems.
The chapter then turns to process reward models (PRMs), which score individual reasoning steps rather than just final answers. PRMs enable Monte Carlo Tree Search (MCTS) over reasoning traces, letting a system explore multiple proof strategies in parallel and backtrack from dead ends. This search-and-verify loop is the computational backbone of systems like AlphaProof and AlphaGeometry 2, which achieved medal-level performance at the International Mathematical Olympiad.
We examine formal mathematical reasoning through the lens of Lean 4 and its role in systems like DeepSeek-Prover and AlphaProof, where natural-language conjectures are translated into machine-verifiable proofs. The connection between formal verification and scientific discovery runs deep: a formally verified derivation carries a stronger guarantee than any amount of empirical testing. We also cover FunSearch (Romera-Paredes et al., 2024), which uses LLMs to discover novel mathematical functions verified by automated evaluation.
Finally, we build a complete verified reasoning pipeline that combines chain-of-thought generation, process reward scoring, and formal verification to solve a mathematical optimization problem with guarantees. This recipe is directly applicable to any discovery workflow where correctness matters more than speed.
The reasoning foundations introduced in Chapter 4: Reasoning For Discovery (deduction, abduction, causal inference) are the conceptual prerequisites; this chapter provides the modern computational realization of those ideas at scale.
Prerequisites
This chapter assumes you have read Chapter 4: Reasoning For Discovery (for the taxonomy of reasoning modes), Chapter 27: Scientific Foundation Models (for transformer architectures and scaling laws), and are comfortable with the LLM API patterns from Chapter 10: Prompting to Programming. Familiarity with reinforcement learning basics (reward signals, value functions) is helpful for Section 29.2 but not strictly required. Section 29.3 introduces Lean 4 from scratch; no prior theorem-prover experience is assumed.
What You Will Learn
- Design chain-of-thought prompts that elicit reliable multi-step reasoning for scientific problems
- Understand how o1/o3-class reasoning models allocate test-time compute and when to use them
- Implement process reward models that score individual reasoning steps
- Apply Monte Carlo Tree Search to explore and rank alternative reasoning trajectories
- Write basic Lean 4 specifications and connect them to LLM-generated proof sketches
- Build a verified reasoning pipeline combining CoT, PRM scoring, and formal verification
Chapter Sections
29.1 Chain-of-Thought and Test-Time Compute
Chain-of-thought prompting, self-consistency decoding, the test-time compute scaling paradigm, o1/o3 reasoning models, and practical strategies for eliciting reliable multi-step reasoning from language models in scientific contexts.
29.2 Process Reward Models and MCTS
Outcome reward models versus process reward models. Step-level scoring of reasoning traces. Monte Carlo Tree Search over reasoning trajectories. The GPQA Diamond benchmark. How AlphaProof and AlphaGeometry 2 combine neural search with symbolic verification.
29.3 Formal Mathematical Reasoning
Lean 4 as a verification target. DeepSeek-Prover and autoformalization. FunSearch: LLM-driven function discovery with automated evaluation. AlphaGeometry 2 and AlphaProof at IMO 2024. The gap between informal and formal reasoning.
29.4 Building a Verified Reasoning Pipeline
Recipe: a complete pipeline that generates chain-of-thought solutions, scores them with a process reward model, verifies key steps formally, and returns ranked, partially verified derivations for a mathematical optimization problem.
What's Next
Reasoning models excel at structured, verifiable problems. But scientific discovery also requires detecting the unexpected: the anomalous data point, the outlier measurement, the surprising observation that does not fit existing theory. Chapter 30: Anomaly and Novelty Discovery takes up this complementary challenge, building systems that flag what the current model cannot explain. Where reasoning models ask "does this conclusion follow?", anomaly detectors ask "does this observation belong?" Together, they form the two arms of a discovery system: one that reasons forward from hypotheses and one that listens for signals the hypotheses missed.
Bibliography
Foundational Papers
The paper that launched chain-of-thought prompting, demonstrating that adding "Let's think step by step" to prompts dramatically improves reasoning performance. The starting point for all test-time compute scaling research.
Introduced self-consistency decoding: sampling multiple CoT paths and selecting the most common answer. A simple technique that provides substantial accuracy gains on reasoning tasks, discussed in Section 29.1.
Introduced process reward models (PRMs) that evaluate each intermediate reasoning step. Demonstrated that step-level verification outperforms outcome-level scoring for mathematical reasoning. Core to Section 29.2.
Formalized the test-time compute scaling paradigm, showing that optimal allocation of inference-time computation can match or exceed the benefits of training larger models. Theoretical backbone of Section 29.1.
AI for Mathematics
Combined a language model with a symbolic deduction engine to solve 25 of 30 IMO geometry problems. The architecture that AlphaGeometry 2 extends, discussed in Section 29.3.
AlphaProof uses reinforcement learning and Lean 4 formalization to solve competition-level algebra and number theory problems. AlphaGeometry 2 extends the original system with a Gemini backbone. Key case studies in Section 29.3.
Uses LLMs to evolve programs that solve open mathematical problems, including finding new constructions for the cap set problem. Demonstrates LLM-driven discovery with rigorous automated verification. Discussed in Section 29.3.
Trains a language model to generate Lean 4 proofs by bootstrapping from synthetic theorem-proof pairs. Achieves strong results on the miniF2F benchmark. Central to the autoformalization discussion in Section 29.3.
Tools & Libraries
Reference for the Claude API used throughout this chapter for chain-of-thought prompting, extended thinking, and the reasoning pipeline recipe in Section 29.4.
Official documentation for the Lean 4 theorem prover and programming language. Used in Section 29.3 and Section 29.4 for formal verification of reasoning steps.
Reference for the o1 and o3 reasoning model APIs, including reasoning effort controls and structured output support. Used in Section 29.1.
Benchmarks & Datasets
A benchmark of graduate-level science questions designed to be resistant to web search. The "Diamond" subset is the gold standard for evaluating reasoning model performance on expert-level scientific reasoning, discussed in Section 29.2.
A benchmark of 488 formalized mathematical statements across multiple proof assistants (Lean, Isabelle, Metamath). The standard evaluation for autoformalization systems discussed in Section 29.3.