Source-linked AI summary
Reasoning Core: A Scalable Procedural Data Generation Suite for Symbolic Pre-training and Post-Training
Valentin Lacombe, Valentin Quesnel, Damien Sileo
TL;DR
Existing procedural symbolic-data generators often lack the distributional breadth needed to build reasoning capabilities at scale. Reasoning Core addresses this gap with procedurally generated, solver-verified tasks across foundational formal domains, using difficulty control and a shared training interface. Mixing its data into training improves downstream reasoning while preserving or slightly improving language modeling quality, though large-scale RLVR validation remains future work.
Problem
Existing procedural generators often rely on fixed puzzles or templates and lack the distributional breadth needed to build new reasoning primitives at scale.
Method
Reasoning Core procedurally generates solver-verified symbolic tasks across foundational formal domains, with continuous difficulty control, optional reasoning traces, and a verifiable reward interface.
Results
Mixing Reasoning Core data into pre-training and instruction-tuning consistently improves downstream reasoning while preserving or slightly improving language modeling quality.
Takeaways & Limitations
The suite provides scalable, high-generality symbolic data for training and evaluation across formal reasoning domains.
Takeaways & Limitations
The paper does not report RLVR training results because rigorous validation requires massive rollouts, careful multi-task mixing, and sophisticated curriculum balancing.
Abstract
from arXiv · showhide
Training on verifiable symbolic data is a promising way to expand the reasoning frontier of language models beyond what standard pre-training corpora provide. Yet existing procedural generators often rely on fixed puzzles or templates and do not deliver the distributional breadth needed at scale. We introduce Reasoning Core, a scalable suite that procedurally generates verifiable symbolic reasoning data across core formal domains: PDDL planning over randomized domains, first-order logic with equality, context-free grammar parsing and generation, causal reasoning over random Bayesian networks, and systems of equations. Each task is paired with an external solver for rigorous verification and admits continuous difficulty control for curriculum design. Examples can optionally include solver-derived reasoning traces, enabling supervised training from the earliest pre-training stages, and the same interface provides verifiable reward functions for reinforcement learning. Our experiments show that mixing Reasoning Core data into pre-training improves downstream reasoning while preserving, or slightly improving, language modeling quality. Zero-shot evaluations confirm these tasks challenge frontier models such as GPT-5. The code and data are publicly available under the MIT license.
1 Introduction
Reasoning Core addresses the limited distributional breadth of existing procedural symbolic-data generators with verifiable, high-generality tasks spanning foundational formal domains. Its unified infrastructure supports scalable generation for training, while experiments report improved reasoning and preserved or slightly improved language modeling quality.
- Motivation: Existing procedural generators often use narrow templates or fixed puzzles that lack the distributional breadth needed to instill new reasoning primitives at scale.The paper contrasts fixed PDDL domains, narrow Dyck-language training, and post-training suites that prioritize task count over within-task generality.
- Contribution: Reasoning Core procedurally generates verifiable symbolic data across PDDL planning, first-order logic, context-free grammars, causal reasoning, and equation solving.The suite targets randomized or otherwise expressive formal domains rather than fixed scenarios.
- Contribution: Each generator uses external-solver verification and continuous difficulty control, yielding effectively unbounded novel instances for curriculum design.The interface exposes training-ready examples and verifiable reward functions for pre-training, instruction-tuning, and reinforcement learning.
- Results: Reasoning Core data improves downstream reasoning while preserving, or slightly improving, language modeling quality.The introduction reports this pattern for pre-training experiments.
2 Related Work
Related work includes LLM-generated synthetic data, procedurally generated environments, and procedural formal-data pre-training. Reasoning Core differs by emphasizing broad distributional generality in foundational symbolic domains while combining solver verification and reasoning traces.
- LLM-generated synthetic data: LLM-based synthetic-data methods target mathematics, theorem proving, coding, and instruction tuning but incur high inference costs and limited distributional breadth.Reasoning Core instead uses purely procedural generation for scalable, verifiable data.
- Procedurally generated environments: Procedurally generated environments address static-dataset limitations through dynamic, scalable tasks, with Reasoning Gym offering broad puzzle and game coverage.The comparison frames Reasoning Gym and Reasoning Core as complementary suites.
- Procedurally generated environments: Reasoning Core prioritizes distributional generality in core formal domains, sampling arbitrary STRIPS problems rather than fixed planning instances.This design contrasts with individual puzzle or game tasks such as Sokoban and Hanoi towers.
- Pre-training on procedural data: Prior procedural pre-training work largely relies on simple formal languages such as Dyck grammars, whereas Reasoning Core covers full context-free grammars and additional symbolic domains.The paper positions this broader coverage as compatible with both pre-training and post-training.
- Pre-training on procedural data: Reasoning Core equips symbolic pre-training data with external solver verifiers and rich reasoning traces intended to support reliable correctness and early chain-of-thought behaviors.The paper presents this combination as distinct from prior procedural formal-data efforts.
3 Reasoning Core
Reasoning Core is a procedurally generated suite targeting foundational formal reasoning domains with broad distributions, continuous difficulty control, external solver verification, and scalable generation infrastructure.
- Task coverage: Reasoning Core targets fundamental formal capacities across planning, logic, equations, grammars, causal reasoning, and related symbolic tasks.The suite includes PDDL planning over randomized domains, first-order logic with equality, non-linear equation systems, context-free grammars, causal reasoning over Bayesian networks, and additional formal tasks.
- Difficulty control: A continuous difficulty knob adjusts factors such as proof depth, variable count, and plan length, supporting fine-grained curricula.Discrete hyperparameters use stochastic rounding, enabling adaptive curricula tailored to model performance.
- Verification: External theorem provers, planning engines, and symbolic algebra systems provide objective verification and unambiguous reward signals.The integrated tools include Vampire/E, FastDownward, and Sympy.
- Grammar-based generation: The generation framework supports expressive, auditable grammars with synchronized output channels, context-sensitive state propagation, and structural controls for derivation trees.A bushiness factor encourages lateral expansion, while state propagation tracks variable scopes and loop invariants for procedural code generation.
- Data production: Scalable production uses difficulty-aware timeouts, process cleanup, batch balancing, and parallel workers to manage variable generator and solver runtimes.The pipeline coordinates single-threaded workers with file locks and scales across CPU cores.
- Reasoning traces: Optional reasoning traces record solver proofs or exact recursive derivations, providing training signals for supervised reasoning behaviors.TPTP proofs are reformatted when available, while arithmetic traces log intermediate steps using exact fractional arithmetic.
4 Experiments
Experiments mix Reasoning Core data into pre-training and instruction-tuning datasets, evaluate reasoning and language modeling, and find consistent reasoning gains without language-modeling degradation; RLVR training is left for future work.
- Data and setup: The experiments release 10M pre-training examples totaling 5B tokens and 1M post-training examples totaling 1B tokens.Pre-training difficulty is concentrated at level 0, while post-training samples levels 0, 3, and 5 uniformly.
- Zero-shot evaluation: GPT-5 finds all Reasoning Core tasks challenging, with higher failure rates in hard mode for most tasks.The zero-shot evaluation uses easy level 0 and hard level 5, with 200 samples per task and difficulty.
- Data and setup: Models are trained by adding r×0.5B Reasoning Core tokens to 0.5B-token natural-language corpora across pre-training and instruction-tuning settings.The tested mixing ratios are r ∈ {0, 0.1, 0.3, 0.5, 1.0}; reasoning traces are included for 50% of available examples.
- Supervised training results: Reasoning Core mixing consistently improves PlatinumBench answer NLL across FineWeb, Dolci, and SYNTH training corpora.Answer NLL is used as a continuous reasoning metric that is less noisy than accuracy for small models.
- Supervised training results: At r=0.5, adding half as many Reasoning Core tokens as the original corpus is identified as the apparent mixing sweet spot.This ratio yields one-third symbolic tokens in the combined training mixture.
- Supervised training results: Additional symbolic tokens improve reasoning without degrading language modeling, while slightly reducing validation loss on general natural-language data.The trade-off is increased total token count, with procedurally generated data described as having negligible marginal cost.
- Scope: The study does not report RLVR training results because large-scale validation requires substantially larger compute budgets and careful multi-task balancing.Although the tasks expose verifiable reward functions, large-scale RL validation is scoped to future work.
5 Conclusion
The conclusion presents Reasoning Core as a broadly distributed, solver-verified symbolic data suite whose mixtures improve downstream reasoning while preserving or slightly improving language modeling, while RL and non-symbolic transfer remain future work.
- Conclusion: Reasoning Core combines broad formal-domain coverage, external solver verification, and continuous difficulty control for scalable symbolic training data.The interface supports both pre-training and instruction-tuning, while exposing verifiable reward functions for reinforcement learning.
- Conclusion: Mixing Reasoning Core data consistently improves downstream reasoning while preserving, or slightly improving, language modeling quality.The conclusion reports this pattern across both pre-training and instruction-tuning experiments.
- Conclusion: Zero-shot evaluations show that Reasoning Core tasks challenge frontier models such as GPT-5.The conclusion frames these evaluations as evidence of task difficulty rather than as RLVR training results.
- Conclusion: Large-scale reinforcement-learning validation and transfer to non-symbolic domains are left for future work.The suite exposes verifiable reward functions, but the conclusion explicitly defers these investigations.
Limitations
Reasoning Core’s evidence is limited by formal-domain scope, small experimental scale, absent RLVR training results, and the possibility of residual generator or verification errors.
- Scope: Transfer from formal symbolic tasks to less formal domains has not been empirically validated.Potential applications include legal reasoning, scientific hypothesis evaluation, agentic tool ordering, and structured argumentation.
- Scale: Experiments use models under 100M parameters trained on 0.5B tokens, while zero-shot evaluations do not constitute a full training study.Whether observed benefits and trade-offs hold at larger model and data scales remains open.
- Absence of RLVR Experiments: The paper reports no RLVR training curves because broad-distribution tasks require massive rollouts, multi-task mixing, and sophisticated curriculum balancing for rigorous evaluation.Small-budget RLVR experiments could underestimate the intended utility of these environments.
- Verification: Despite solver checks, LLM review, human adjudication, and code auditing, subtle generator, solver, or specification mismatches may leave a small fraction of instances erroneous.The verification pipeline is therefore not infallible.
Broader Impact
Reasoning Core supports scalable symbolic pre-training by generating virtually unlimited procedural data across formal domains. Its reconstructible, re-validatable design also addresses licensing, contamination, and reproducibility concerns.
- Broader Impact: Procedural formal structures can be injected during pre-training or mid-training to develop foundational reasoning capabilities before post-training.The paper frames this as a scalable path toward neurosymbolic AI.
- Broader Impact: Reasoning Core generates procedurally novel, reconstructible instances whose correctness can be deterministically re-evaluated with provided scoring interfaces.External solvers handle complex verification while keeping the generation code concise and inspectable.
- Broader Impact: Fully procedural data reduces licensing ambiguities and copyright risks associated with web-scraped or proprietary-model-distilled datasets.Procedural novelty also avoids benchmark contamination concerns and supports reproducible datasets.
A Task descriptions 3
The suite covers symbolic arithmetic, induction, Bayesian inference, code and text transformations, grammar tasks, regex tasks, evidence retrieval, planning, and graph reasoning. Tasks vary in generation procedures, representations, scoring rules, and difficulty controls.
- Arithmetic and Induction: Arithmetic tasks evaluate sampled expression trees or simplify grammar-generated symbolic expressions, with difficulty controlled by depth, precision, variables, and numeric range.Sequential induction infers recurrence relations from integer sequence prefixes while filtering degenerate sequences.
- Evidence Retrieval: Evidence retrieval selects minimal premise subsets that entail or contradict a hypothesis, verified by testing whether removing each premise invalidates the proof.This ablation criterion ensures included premises are necessary to the verified proof.
- Planning: Planning generates valid sequential plans from randomly generated STRIPS domains and instances, with deterministic lexicographic action ordering and length-penalized scoring.Reasoning traces track state changes and remaining goals.
- Graph Reasoning: Graph tasks include shortest-path search across diverse topologies and text formats, degree-centrality identification with ties, cycle-node detection, and graph-isomorphism classification.Outputs include BFS traces, sorted node lists, or binary decisions depending on the task.
- Causal Reasoning: Bayesian association computes observational posteriors, whereas Bayesian intervention applies graph surgery before propagating the resulting distribution.Both use random Bayesian networks and Jensen–Shannon divergence scoring.
- Code and Text Transformations: Code execution predicts synthetic Python output across grammar-generated construct complexities, while diff tasks generate or apply unified patches from stochastically mutated file histories.Diff scoring uses character-level similarity.
- Grammar and Regex: Grammar tasks classify parsability, produce parse trees, or identify valid continuations using sampled or curated context-free grammars and exact Earley parsing.Parsing retains only unambiguous parses, and continuation scoring uses token-set overlap with partial credit.
- Grammar and Regex: Regex following generates strings matching stochastic regular expressions, while regex induction handles arbitrary combinations of quantifiers, negation, and predicates.The supplied task description states that these combinations define the distribution’s breadth.