Sättigungsgesteuerte Datensatzgenerierung für mathematisches Reasoning von LLMs im TPTP-Ökosystem
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
Die Knappheit von hochwertigen, logisch fundierten Daten stellt ein entscheidendes Hindernis für die Weiterentwicklung des mathematischen Denkens von Large Language Models (LLMs) dar. Unsere Arbeit begegnet dieser Herausforderung, indem sie jahrzehntelange Forschung im Bereich des automatischen Theorembeweisens in eine skalierbare Datenmaschine umwandelt. Anstatt sich auf fehleranfällige LLMs oder komplexe Syntax von Beweisassistenten wie Lean und Isabelle zu verlassen, nutzt unser Framework die Sättigungsfähigkeiten des E-Provers auf der umfangreichen TPTP-Axiombibliothek, um einen umfangreichen, garantiert gültigen Korpus von Theoremen abzuleiten. Unsere Pipeline ist prinzipientreu und einfach: Axiome sättigen, nach „interessanten“ Theoremen filtern und Aufgaben generieren. Da keine LLMs im Prozess involviert sind, eliminieren wir faktische Fehler durch Konstruktion. Diese rein symbolischen Daten werden dann in drei schwierigkeitskontrollierte Herausforderungen transformiert: Verifikation von Implikationen, Prämissenauswahl und Beweisrekonstruktion. Unsere Zero-Shot-Experimente mit führenden Modellen zeigen eine deutliche Schwäche: Die Leistung bricht bei Aufgaben ein, die tiefes, strukturelles Denken erfordern. Unser Framework bietet sowohl das Diagnosewerkzeug, um diese Lücke zu messen, als auch eine skalierbare Quelle symbolischer Trainingsdaten, um sie zu schließen. Wir stellen den Code und die Daten öffentlich zur Verfügung.
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