Verzadigingsgestuurde datasetgeneratie voor wiskundig redeneren van LLM's in het TPTP-ecosysteem
Saturation-Driven Dataset Generation for LLM Mathematical Reasoning in the TPTP Ecosystem
September 8, 2025
Auteurs: Valentin Quesnel, Damien Sileo
cs.AI
Samenvatting
Het gebrek aan hoogwaardige, logisch correcte data vormt een kritieke belemmering voor het bevorderen van het wiskundig redeneervermogen van Large Language Models (LLMs). Ons werk gaat deze uitdaging aan door decennia van onderzoek naar automatisch stellingen bewijzen om te zetten in een schaalbare data-engine. In plaats van te vertrouwen op foutgevoelige LLMs of complexe syntax van bewijsassistenten zoals Lean en Isabelle, maakt ons framework gebruik van de saturatiecapaciteiten van E-prover op de uitgebreide TPTP-axiombibliotheek om een enorme, gegarandeerd valide corpus van stellingen af te leiden. Onze pijplijn is principieel en eenvoudig: saturatie van axioma's, filteren op "interessante" stellingen, en het genereren van taken. Zonder LLMs in de loop elimineren we feitelijke fouten door constructie. Deze puur symbolische data wordt vervolgens omgezet in drie moeilijkheidsgecontroleerde uitdagingen: entailment-verificatie, premisse-selectie en reconstructie van bewijzen. Onze zero-shot experimenten op frontier-modellen onthullen een duidelijke zwakte: de prestaties storten in bij taken die diepgaand, structureel redeneren vereisen. Ons framework biedt zowel het diagnostische instrument om deze kloof te meten als een schaalbare bron van symbolische trainingsdata om deze aan te pakken. We maken de code en data publiekelijk beschikbaar.
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