Génération de jeux de données pilotée par la saturation pour le raisonnement mathématique des LLM dans l'écosystème TPTP
Saturation-Driven Dataset Generation for LLM Mathematical Reasoning in the TPTP Ecosystem
September 8, 2025
papers.authors: Valentin Quesnel, Damien Sileo
cs.AI
papers.abstract
La rareté de données de haute qualité et logiquement solides constitue un goulot d'étranglement critique pour l'amélioration du raisonnement mathématique des modèles de langage de grande taille (LLMs). Notre travail relève ce défi en transformant des décennies de recherche en démonstration automatique de théorèmes en un moteur de données scalable. Plutôt que de s'appuyer sur des LLMs sujets aux erreurs ou sur une syntaxe complexe d'assistants de preuve comme Lean et Isabelle, notre cadre exploite les capacités de saturation de E-prover sur la vaste bibliothèque d'axiomes TPTP pour dériver un corpus massif de théorèmes garantis valides. Notre pipeline est à la fois rigoureux et simple : saturer les axiomes, filtrer les théorèmes "intéressants", et générer des tâches. En excluant les LLMs du processus, nous éliminons les erreurs factuelles par construction. Ces données purement symboliques sont ensuite transformées en trois défis à difficulté contrôlée : vérification d'implication, sélection de prémisses et reconstruction de preuve. Nos expériences en zero-shot sur des modèles de pointe révèlent une faiblesse évidente : les performances s'effondrent sur les tâches nécessitant un raisonnement profond et structurel. Notre cadre fournit à la fois l'outil de diagnostic pour mesurer cet écart et une source scalable de données d'entraînement symboliques pour y remédier. Nous mettons le code et les données à disposition du public.
https://github.com/sileod/reasoning_core
https://hf.co/datasets/reasoning-core/rc1
English
The scarcity of high-quality, logically sound data is a critical bottleneck
for advancing the mathematical reasoning of Large Language Models (LLMs). Our
work confronts this challenge by turning decades of automated theorem proving
research into a scalable data engine. Rather than relying on error-prone LLMs
or complex proof-assistant syntax like Lean and Isabelle, our framework
leverages E-prover's saturation capabilities on the vast TPTP axiom library to
derive a massive, guaranteed-valid corpus of theorems. Our pipeline is
principled and simple: saturate axioms, filter for "interesting" theorems, and
generate tasks. With no LLMs in the loop, we eliminate factual errors by
construction. This purely symbolic data is then transformed into three
difficulty-controlled challenges: entailment verification, premise selection,
and proof reconstruction. Our zero-shot experiments on frontier models reveal a
clear weakness: performance collapses on tasks requiring deep, structural
reasoning. Our framework provides both the diagnostic tool to measure this gap
and a scalable source of symbolic training data to address it. We make the code
and data publicly available.
https://github.com/sileod/reasoning_core
https://hf.co/datasets/reasoning-core/rc1