Reasoning Core: Teaching Language Models to Think Through Procedural Symbolic Data

Paper: 2603.02208 Authors: Valentin Lacombe, Valentin Quesnel, Damien Sileo Categories: cs.CL

The Gap

Language models trained on web text learn patterns but struggle with formal reasoning. Prior work tried synthetic data—GSM8K-style math problems, simple logic puzzles, code exercises—but these approaches hit a wall. They either use fixed templates (so models memorize patterns instead of learning reasoning) or generate from narrow distributions (so the data doesn’t cover the reasoning space models need). Projects like DeepMind’s FunSearch and OpenAI’s process supervision showed that verifiable reasoning data helps, but nobody built a unified, scalable generator that spans multiple formal domains with continuous difficulty control and built-in verification.

Problem: LMs reason poorly on formal tasks
   |
   v
Assumption: Verifiable symbolic data during pre-training can teach reasoning
   |
   v
Method: Procedural generator across 5 domains + external solvers + difficulty knobs
   |
   v
Evidence: Pre-training mix improves reasoning, preserves language quality
   |
   v
Conclusion: Scalable symbolic data generation is viable for reasoning-enhanced LMs

The Increment

One sentence: Before, you trained on web text and hoped reasoning emerged; now, you can inject verifiable symbolic reasoning tasks directly into pre-training at scale.

Core Mechanism

Reasoning Core is a procedural generator that creates problems across five formal domains: PDDL planning (move blocks in randomized worlds), first-order logic with equality (prove theorems), context-free grammar tasks (parse or generate strings), causal reasoning (infer from Bayesian networks), and equation systems (solve for variables). Each domain has a randomization engine that samples problem instances, a difficulty parameter you can dial up or down, and an external solver (off-the-shelf tools like Fast Downward for PDDL, Z3 for logic) that both verifies correctness and optionally produces step-by-step reasoning traces.

The data flow is simple: you specify a domain, difficulty level, and whether you want reasoning traces. The generator samples a random problem instance, calls the solver to get the solution and optionally the derivation steps, then formats everything as text. The output is a training example with input (problem statement), output (solution), and optionally intermediate steps (the solver’s reasoning chain). You can generate millions of examples, mix them into your pre-training corpus, and the model learns from ground-truth reasoning instead of just pattern-matching web text.

   Domain Spec + Difficulty
          |
          v
   [ Randomization Engine ]
          |
          v
   Problem Instance -----> [ External Solver ]
          |                       |
          v                       v
   Problem Text            Solution + Trace
          |                       |
          +-------+-------+-------+
                  |
                  v
          Training Example
       (input, output, steps)

Think of Reasoning Core as a flight simulator for formal reasoning. A pilot doesn’t learn by reading flight manuals alone—they need hours in a simulator that generates diverse, realistic scenarios with verifiable outcomes. Here, the randomization engine is the scenario generator (weather conditions, aircraft failures), the difficulty knob is the training progression (start with clear skies, advance to storms), the external solver is the physics engine that enforces real-world constraints, and the reasoning traces are the instructor’s commentary showing correct decision sequences. The model is the trainee pilot, and pre-training is flight school. Instead of hoping the pilot figures out aerodynamics from reading Wikipedia, you put them in the simulator from day one.

Key Concepts

• Procedural generation with verification: Most synthetic data generators use templates—fill-in-the-blank patterns that produce superficially varied but structurally identical problems. Reasoning Core instead uses randomization engines that sample from the actual problem space (random graph structures for planning, random formulas for logic). Each generated problem is then verified by an external solver, so you know the answer is correct and the problem is solvable. This is like the difference between a multiple-choice test with shuffled options (template) versus generating entirely new math problems and checking them with a calculator (procedural + verification). The former teaches pattern recognition; the latter teaches problem-solving.

• Continuous difficulty control: Traditional datasets have discrete difficulty levels or none at all. Reasoning Core lets you dial a continuous parameter—for PDDL, it’s the number of objects and goal complexity; for logic, it’s formula depth and quantifier nesting. This enables curriculum learning: start the model on easy problems during early pre-training, gradually increase difficulty as it improves. Imagine teaching a child arithmetic: you don’t jump from 2+2 to calculus. You increase problem complexity as their skills develop. The difficulty knob automates this progression.

• Solver-derived reasoning traces: When you solve a logic problem by hand, you write intermediate steps: “assume X, apply rule Y, derive Z.” Most training data lacks this. Reasoning Core optionally includes the solver’s derivation—the actual proof steps, planning actions, or equation manipulations. This is like showing your work in math class. The model learns not just what the answer is, but how to get there. During pre-training, this means the model sees correct reasoning chains from the start, not just final answers. During RL fine-tuning, these traces become verifiable reward signals: did the model follow valid reasoning steps?

Framework Shift

Before (mainstream approach):        After (this paper):

  Web Text Corpus                     Web Text + Symbolic Data
        |                                      |
        v                                      v
  [ Pre-training ]                    [ Pre-training ]
        |                                      |
        v                                      v
  General LM                          Reasoning-Enhanced LM
        |                                      |
        v                                      v
  Fine-tune on reasoning tasks        Fine-tune on reasoning tasks
   (hope it works)                     (already has foundation)

  Data: Fixed, unverified             Data: Generated, verified
  Reasoning: Emergent (maybe)         Reasoning: Explicit training
  Curriculum: None                    Curriculum: Difficulty control

From hoping reasoning emerges from web text to explicitly training it with verifiable symbolic data from the start, the core shift is making reasoning a first-class training objective rather than an accidental byproduct.

Expert Assessment

Problem choice: This is a real gap. The field has known for years that LMs struggle with formal reasoning, and recent work (chain-of-thought, process supervision, AlphaProof) confirms that verifiable reasoning data helps. But nobody built a unified, scalable generator before. The timing is right—models are big enough to benefit from this data, and the infrastructure (external solvers, curriculum learning) is mature. This sits squarely in the “reasoning for LMs” trajectory that’s been heating up since GPT-3.

Method maturity: This is engineering more than insight. The core idea—use procedural generation + external solvers—is straightforward. The contribution is execution: building a clean interface across five diverse domains, making it scalable, and showing it works. There’s no deep algorithmic novelty, but that’s fine. Sometimes the field needs good infrastructure. The difficulty control and reasoning traces are nice touches, but not groundbreaking. A simpler approach might just generate problems without traces and rely on RL, but the authors’ choice to include supervised traces from the start is defensible.

Experimental integrity: The experiments are solid but not exhaustive. They show pre-training mix improves reasoning on held-out symbolic tasks and doesn’t hurt language modeling. Good. They also show GPT-4 struggles on these tasks, which validates difficulty. But I’d want to see more: ablations on trace vs no-trace, curriculum vs random difficulty, and transfer to non-symbolic reasoning (does PDDL training help with real-world planning?). The baselines are fair—they compare to standard pre-training—but there’s no comparison to other synthetic data generators like those used in Minerva or WizardLM. The numbers look reasonable, no obvious red flags, but the evaluation is narrow.

Writing quality: The paper is clear and well-organized, but the related work section is thin. They mention FunSearch and process supervision but don’t deeply engage with the synthetic data generation literature (e.g., Textbooks Are All You Need, Self-Instruct). The method section is good, but the results section could use more analysis—why does mixing symbolic data preserve language quality? What’s the optimal mix ratio? The discussion of limitations is honest (they acknowledge transfer to real-world reasoning is unclear), which I appreciate. If they rewrote the related work to position this more carefully against prior synthetic data efforts, the paper would be stronger.

Verdict: weak accept — Solid infrastructure contribution with clear experiments, but lacks deep insight or comprehensive evaluation to be a strong accept.

Takeaways

If you’re building training data for reasoning-heavy models, steal these ideas:

1. Pair generation with verification: Don’t just generate synthetic problems—verify them with external tools. This ensures correctness and lets you filter out unsolvable or trivial instances. Use Z3 for logic, SAT solvers for constraints, symbolic math libraries for equations. The verification step is what separates useful synthetic data from noise.

2. Continuous difficulty as a hyperparameter: Instead of fixed easy/medium/hard buckets, parameterize problem complexity (graph size, formula depth, constraint count) and treat it as a curriculum knob. Start low during early training, ramp up as loss decreases. This is applicable beyond symbolic reasoning—imagine difficulty-controlled code generation (function complexity) or reading comprehension (passage length, inference depth).

3. Reasoning traces as intermediate supervision: If your domain has a solver or verifier that produces step-by-step derivations, include them in training data. This gives the model explicit examples of valid reasoning chains, not just input-output pairs. Even if you’re doing RL later, having supervised traces early helps bootstrap. This applies to any task where you can programmatically generate correct reasoning steps: proofs, derivations, planning sequences, debugging traces.

The broader lesson: verifiable synthetic data is underutilized. Most projects generate text and hope it’s useful. If your domain has formal structure, exploit it—generate problems, verify solutions, control difficulty, include reasoning steps. This paper shows it’s feasible at scale.