TLDR: A new framework generates high-quality, logically sound mathematical reasoning datasets for LLMs by leveraging automated theorem provers and the TPTP axiom library. It creates three types of difficulty-controlled tasks (entailment verification, premise selection, and proof reconstruction) without LLMs in the loop, ensuring validity. Experiments show current LLMs struggle with multi-step, structural reasoning, highlighting the need for this scalable data source to improve their mathematical capabilities.
Large Language Models (LLMs) have shown remarkable progress in many areas, but their ability to perform rigorous, multi-step mathematical reasoning remains a significant challenge. A core reason for this limitation is the scarcity of high-quality, logically sound training data. Unlike other domains rich with vast amounts of text or images, formalized mathematical proofs are expensive and difficult to create at scale.
Addressing this critical data bottleneck, a new research paper titled “Saturation-Driven Dataset Generation for LLM Mathematical Reasoning in the TPTP Ecosystem” by Valentin Quesnel and Damien Sileo introduces an innovative framework. This framework transforms decades of automated theorem proving research into a scalable engine for generating massive, guaranteed-valid datasets of mathematical theorems.
A Novel Approach to Data Generation
The key innovation of this framework is its complete independence from LLMs during data generation. Instead of relying on error-prone LLMs or complex proof-assistant syntaxes like Lean or Isabelle, the system leverages the saturation capabilities of E-prover on the extensive TPTP axiom library. This purely symbolic approach ensures that every generated theorem is mathematically valid by construction, eliminating factual errors from the outset.
The pipeline is straightforward yet powerful: it saturates axioms (exhaustively derives logical consequences), filters for “interesting” theorems using a system called AGInTRater, and then generates various reasoning tasks. The process is fully deterministic and reproducible, capable of producing an unlimited supply of tasks with controllable difficulty.
Three Facets of Logical Reasoning
The framework deconstructs the theorem-proving process into three distinct, difficulty-controlled challenges, each designed to probe different aspects of an LLM’s logical reasoning:
- Conjecture Entailment Verification: This is a true/false task that tests a model’s ability to verify deductive conclusions. Models are given context axioms, a specific set of premises (which can be perturbed with distractors), and a theorem, then asked if the premises entail the theorem.
- Minimal Premise Selection: This task requires LLMs to identify the smallest necessary set of hypotheses from a larger pool, including distractors, that are sufficient to prove a given theorem. This tests their ability to filter noise and pinpoint crucial information.
- Proof Graph Reconstruction: The most complex task, this challenges models to reconstruct the hierarchical structure of a complete proof. Given a shuffled list of clauses from a proof, the LLM must identify the parent-child relationships to rebuild the original derivation graph.
The difficulty of these tasks can be precisely controlled by adjusting parameters such as proof depth (the number of steps in a proof) and the number of distractors or perturbations introduced.
Experiments and Key Findings
The researchers conducted zero-shot experiments on frontier models, including gpt-5-nano, gpt-5-mini, and gpt-5, using a benchmark of 3,000 problems across diverse mathematical domains like Algebra, Set Theory, and Topology. The results revealed clear weaknesses in current LLMs:
- Performance consistently degraded as logical complexity increased across all tasks and models, confirming that multi-step inference is a significant bottleneck.
- While larger models generally outperformed smaller ones, even the state-of-the-art gpt-5 model struggled immensely with the Proof Reconstruction task. This suggests that simply scaling models is not enough to unlock robust, hierarchical planning abilities, indicating a fundamental deficit in structural reasoning.
The framework provides both a diagnostic tool to measure this reasoning gap and a scalable source of symbolic training data to address it. The code and data are publicly available for further research and development. You can find more details in the full paper here.
Also Read:
- RIMO: A New Benchmark Exposes AI’s Mathematical Reasoning Gap
- Unlocking Complex Proofs: BFS-Prover-V2 Advances AI in Formal Mathematics
Future Directions
This work opens exciting avenues for future research, including fine-tuning LLMs with these generated datasets to test if symbolic reasoning skills can transfer to natural language mathematical problems. The team also plans to implement iterative saturation loops to generate even more complex problems and extend the framework to support full first-order logic, further increasing the expressiveness of the tasks.
