Source-linked AI summary
Reasoning Core: A Scalable RL Environment for LLM Symbolic Reasoning
Valentin Lacombe, Valentin Quesnel, Damien Sileo
TL;DR
Reasoning Core targets the limited generality of puzzle-focused benchmarks by procedurally generating tasks in foundational symbolic domains. It combines external verification and continuous difficulty control; an initial zero-shot evaluation found its tasks challenging for GPT-5, particularly at higher difficulty.
Problem
Method
Results
Takeaways & Limitations
Reasoning Core is positioned as a resource for future RLVR research on foundational symbolic reasoning.
Source: §5 · p. 4
Abstract
from arXiv · showhide
We introduce Reasoning Core, a new scalable environment for Reinforcement Learning with Verifiable Rewards (RLVR), designed to advance foundational symbolic reasoning in Large Language Models (LLMs). Unlike existing benchmarks that focus on games or isolated puzzles, Reasoning Core procedurally generates problems across core formal domains, including PDDL planning, first-order logic, context-free grammar parsing, causal reasoning, and system equation solving. The environment is built on key design principles of high-generality problem distributions, verification via external tools, and continuous difficulty control, which together provide a virtually infinite supply of novel training instances. Initial zero-shot evaluations with frontier LLMs confirm the difficulty of Reasoning Core's tasks, positioning it as a promising resource to improve the reasoning capabilities of future models.
1 Introduction
Reasoning Core addresses limits in scalable RLVR data and puzzle-focused generators with procedurally generated tasks in foundational symbolic domains.
1 Introduction
- Fixed benchmarks and puzzle-focused generators leave a need for scalable data and tasks probing the expressive generality of foundational reasoning domains.Existing approaches rely on fixed curated benchmarks or finite scraped content, while many generative tasks use constrained rule sets.Source: §1 · p. 1
- Reasoning Core provides procedural environments for PDDL planning, first-order logic with equality, context-free grammar parsing, symbolic induction, and system equation solving.Source: §1 · p. 1
- Specialized external tools verify structured solutions, while offline parallel generation and search support a continuing supply of novel instances.Each generator has a continuous difficulty control for adaptive curricula.Source: §1 · p. 1
2 Related Work
Prior work spans static reasoning benchmarks and procedurally generated environments, while Reasoning Core emphasizes general symbolic domains and verifiable data.
2 Related Work
- Fixed benchmarks are susceptible to contamination and do not evaluate generalization to novel problems of increasing difficulty.Source: §2 · p. 2
- Procedural generation creates dynamic, scalable evaluation environments, but many existing suites focus on games, puzzles, or narrow templates.Source: §2 · p. 2
- Reasoning Core distinguishes itself through expressive domains such as planning and formal logic, which can model a wide range of real-world problems.Source: §2 · p. 2
- Reasoning Core adds verifiable synthetic data targeting generalizable symbolic reasoning skills to the RLVR ecosystem.It interfaces with external solvers for correctness in complex symbolic domains.Source: §2 · p. 2
3 Reasoning Core
Reasoning Core combines foundational symbolic tasks with controlled generation, specialized verification, and scalable production of novel problems.
3 Reasoning Core
- The suite covers PDDL planning, first-order logic, non-linear equation solving, grammar parsing, regex induction, symbolic induction, causal reasoning, and formal mathematics tasks.It also includes retrieval and perception tasks, such as missing-element detection and set intersection.Source: §3 · p. 2
- A continuous difficulty knob adjusts generator factors such as proof depth, equation variables, and PDDL plan length, using stochastic rounding for discrete parameters.This supports adaptive curricula and a virtually infinite supply of novel instances.Source: §3 · p. 2
- The framework uses theorem provers, PDDL planning engines, and symbolic algebra systems to provide objective reward signals and assess structured outputs.The tools also handle problem solvability and solution optimality.Source: §3 · pp. 2–3
- Grammar-based generators and efficient algorithms control both maximum and minimum generation depth to tune problem difficulty.Grammars are used for arithmetic, regex-following, and grammar-understanding tasks.Source: §3 · p. 3
- Search-based and offline parallel generation pipelines rapidly produce diverse problems for continuous RLVR training.Source: §3 · p. 3
4 Results
An initial zero-shot evaluation found Reasoning Core challenging for GPT-5, with higher difficulty producing more failures on most tasks.
4 Results
- GPT-5 with low reasoning effort found all tasks challenging, and hard mode increased failure rates for most tasks.Source: §4 · p. 3
- The evaluation tested easy knob level 0 and hard knob level 5, using 200 samples per task and difficulty.Source: §4 · p. 3
- The difficulty control worked as intended for most tasks, with the hard setting yielding higher failure rates.Source: §4 · p. 3
5 Conclusion
Reasoning Core is a scalable RL environment for fundamental symbolic reasoning, using high-generality tasks, external solvers, continuous difficulty control, and efficient data generation. Initial GPT-5 zero-shot performance underscores the tasks’ demanding nature and positions the environment as a resource for future RLVR research.
5 Conclusion
- Reasoning Core targets fundamental symbolic reasoning with high-generality tasks such as PDDL planning and first-order logic.The library uses external solvers for rigorous verification and continuous difficulty control.Source: §5 · p. 3
- The framework’s continuous difficulty control and efficient data generation provide a tool for developing robust and transferable reasoning skills in LLMs.Source: §5 · pp. 3–4
- Initial zero-shot performance of GPT-5 underscores Reasoning Core’s demanding tasks and positions it as a resource for future RLVR research.The framework combines continuous difficulty control with efficient data generation.Source: §5 · pp. 3–4
A.1 planning
The planning task asks models to produce valid action sequences for goals in randomly generated PDDL-like domains. Its instances vary planning complexity and are checked for both syntactic correctness and semantic validity.
A.1 planning
- Planning instances use randomly constructed PDDL-like domains with objects, actions, preconditions, effects, and specified goals.Models must reason over state transitions to generate valid action sequences.Source: §A.1 · p. 6
- The generator varies domain complexity, object types, fluent arities, and goal configurations to cover diverse planning patterns.Source: §A.1 · p. 6
- Solutions are validated for syntactic correctness and semantic validity against domain constraints.Source: §A.1 · p. 6
- The authors describe this as the first planning-data generator, to their knowledge, using randomly sampled domains rather than existing ones such as BlocksWorld or Sokoban.Source: §A.1 · p. 6
A.2 equation_system
The equation-system task tests solving linear systems and classifying cases without a unique solution. Its generator creates unique-solution systems, then modifies them to produce inconsistent or underdetermined cases.
A.2 equation_system
- The task evaluates solving linear systems and identifying underdetermined or inconsistent cases.Source: §A.2 · p. 6
- The generator starts with a known unique solution and applies random linear combinations to obfuscate the equations.Source: §A.2 · p. 6
- It probabilistically creates inconsistent systems by adding contradictory constraints or underdetermined systems by removing equations.The distribution includes unique-solution, inconsistent, and multiple-solution systems.Source: §A.2 · p. 6
- For a requested variable, the model must return its numerical value or report “No solution” or “Multiple solutions” when no unique value exists.Source: §A.2 · p. 6
A.3 regex_following
The regex task asks models to generate strings accepted by a supplied pattern under full-match semantics. Patterns vary in complexity and use constructs including character classes, quantifiers, alternation, grouping, and predefined character sets.
A.3 regex_following
- The model must generate a string accepted by a supplied regex pattern under full-match semantics.Source: §A.3 · p. 7
- Patterns are generated with varying complexity using character classes, quantifiers, alternation, grouping, and predefined character sets.Source: §A.3 · p. 7
- The examples distinguish strings that match a pattern from ones that do not, and request a valid match for a supplied pattern.Source: §A.3 · p. 7
A.4 regex_induction
Regex induction tests whether models can infer a regular expression that separates positive from negative examples. Problems use procedurally generated target patterns, and scoring rewards perfect classification while favoring concise expressions.
A.4 regex_induction
- Targets are generated with a probabilistic context-free grammar combining character classes, quantifiers, alternation, concatenation, and predefined patterns such as \d and \w.The prompt asks for a regex matching every positive string and no negative strings.Source: §A.4 · p. 7
- Positive strings are sampled from the target regex, while negative strings come from other randomly generated regexes and are filtered to exclude accidental matches.Source: §A.4 · p. 7
- Solutions are rewarded for perfect classification accuracy, with a length penalty applied only at 100% accuracy to prefer concise expressions.Source: §A.4 · p. 7
A.5 arithmetics
This section describes procedurally generated symbolic-reasoning tasks across arithmetic and sequence induction, formal logic, grammar parsing, Bayesian inference, and set operations, with problem structure and complexity varied by generators and outputs evaluated through automated verification. Its arithmetic subsection includes a Set_A prompt asking for the missing string.
A.5 arithmetics; A.6 sequential_induction
- Arithmetic tasks vary expression structure and numeric settings, while sequence induction asks models to infer recursive formulas from generated sequences.Arithmetic generation controls depth, precision, and floating-point probability while rejecting division by zero; sequence formulas range from basic operations to modular arithmetic and unary operators, with degenerate cases and numerical explosion filtered.Source: §A.5 · p. 7, §A.6 · p. 8
A.7 conjecture_entailment; A.8 theorem_premise_selection
- Conjecture entailment tests axiom-subset sufficiency, while premise selection asks models to choose the minimal necessary and sufficient premises for a theorem.The entailment task uses TPTP derivation graphs and perturbed unprovable cases verified with Vampire; premise-selection pools include necessary premises and distractors across mathematical domains.Source: §A.7 · p. 8, §A.8 · p. 9
A.9 proof_reconstruction
- Proof reconstruction requires recovering axiom and parent-clause relationships from shuffled proofs, with every derived clause having exactly two parents.Tasks span mathematical domains, and evaluation combines graph structure with automated validation of individual derivation steps.Source: §A.9 · p. 10
A.10 logic_nli; A.11 evidence_retrieval
- Logic NLI classifies hypotheses as entailed, contradicted, or neither, while evidence retrieval selects the premise statements needed to support a relationship.NLI instances span quantifiers and complex predicates with prover-generated proof metadata; evidence sets are automatically verified and vary in premise count and logical complexity.Source: §A.10 · p. 11, §A.11 · p. 11
A.12 parsability; A.13 parsing
- CFG tasks classify strings as unambiguous, ambiguous, or unparsable, and separately require fully parenthesized parse trees for strings guaranteed to have a unique parse.Generated grammars vary in nonterminals, terminals, and production rules, and include nested structures and Dyck languages.Source: §A.12 · p. 12, §A.13 · p. 12
A.14 bayesian_association
- Bayesian association tasks compute a target’s posterior distribution given observations in generated networks of variables with conditional probability distributions.The tasks require exact inference and reasoning about conditional independence in randomly generated directed acyclic graphs.Source: §A.14 · p. 13
A.15 bayesian_intervention
- Bayesian intervention tasks compute target distributions under both a do-operator intervention and observed evidence, using do-calculus to distinguish interventional from observational queries.Generated directed acyclic graphs have configurable node counts and domain sizes.Source: §A.15 · p. 13
A.16 set_equality; A.17 set_intersection; A.18 set_missing_element
- Set tasks test order-independent set equality, common-element identification, and recovery of a missing item from a shuffled contiguous subsequence across varied data types.Equality difficulty scales with set size and perturbations; intersection allows partial credit via Jaccard similarity, while missing-element sequences span numbers, dates, and letter combinations.Source: §A.16 · p. 14, §A.17 · p. 14, §A.18 · p. 15
A.18 set_missing_element
- Given Set_A = ['bz', 'by', 'ca', 'bw', 'bt', 'cb', 'bv', 'bs', 'bu'], the task is to return its missing string element.Source: §A.18 · p. 15