Generación de Conjuntos de Datos Impulsada por Saturación para el Razonamiento Matemático de Modelos de Lenguaje en el Ecosistema TPTP
Saturation-Driven Dataset Generation for LLM Mathematical Reasoning in the TPTP Ecosystem
September 8, 2025
Autores: Valentin Quesnel, Damien Sileo
cs.AI
Resumen
La escasez de datos de alta calidad y lógicamente sólidos es un cuello de botella crítico para avanzar en el razonamiento matemático de los Modelos de Lenguaje a Gran Escala (LLMs, por sus siglas en inglés). Nuestro trabajo aborda este desafío transformando décadas de investigación en demostración automática de teoremas en un motor de datos escalable. En lugar de depender de LLMs propensos a errores o de sintaxis complejas de asistentes de demostración como Lean e Isabelle, nuestro marco aprovecha las capacidades de saturación de E-prover en la vasta biblioteca de axiomas TPTP para derivar un corpus masivo de teoremas garantizados como válidos. Nuestra canalización es fundamentada y simple: saturar axiomas, filtrar teoremas "interesantes" y generar tareas. Al no incluir LLMs en el proceso, eliminamos errores fácticos por construcción. Estos datos puramente simbólicos se transforman luego en tres desafíos controlados por dificultad: verificación de implicación, selección de premisas y reconstrucción de demostraciones. Nuestros experimentos de cero disparos en modelos de vanguardia revelan una debilidad clara: el rendimiento colapsa en tareas que requieren un razonamiento profundo y estructural. Nuestro marco proporciona tanto la herramienta de diagnóstico para medir esta brecha como una fuente escalable de datos de entrenamiento simbólicos para abordarla. Hacemos público el código y los datos.
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