Генерация наборов данных на основе насыщения для математических рассуждений в крупных языковых моделях в экосистеме TPTP
Saturation-Driven Dataset Generation for LLM Mathematical Reasoning in the TPTP Ecosystem
September 8, 2025
Авторы: Valentin Quesnel, Damien Sileo
cs.AI
Аннотация
Недостаток высококачественных, логически стройных данных является критическим препятствием для развития математических способностей крупных языковых моделей (LLM). Наша работа решает эту проблему, превращая десятилетия исследований в области автоматического доказательства теорем в масштабируемый механизм генерации данных. Вместо того чтобы полагаться на подверженные ошибкам LLM или сложный синтаксис систем доказательств, таких как Lean и Isabelle, наш фреймворк использует возможности насыщения E-prover на обширной библиотеке аксиом TPTP для создания огромного, гарантированно корректного корпуса теорем. Наш процесс структурирован и прост: насыщение аксиом, фильтрация "интересных" теорем и генерация задач. Без участия LLM в цикле мы исключаем фактические ошибки на этапе построения. Эти чисто символические данные затем преобразуются в три задачи с контролируемой сложностью: проверка следования, выбор предпосылок и восстановление доказательства. Наши эксперименты с нулевым обучением на передовых моделях выявили явную слабость: производительность резко падает на задачах, требующих глубокого, структурного рассуждения. Наш фреймворк предоставляет как инструмент для диагностики этого разрыва, так и масштабируемый источник символических обучающих данных для его устранения. Мы делаем код и данные общедоступными.
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