StepFun-Formalizer: Раскрытие потенциала автоформализации языковых моделей через интеграцию знаний и логических рассуждений
StepFun-Formalizer: Unlocking the Autoformalization Potential of LLMs through Knowledge-Reasoning Fusion
August 6, 2025
Авторы: Yutong Wu, Di Huang, Ruosi Wan, Yue Peng, Shijie Shang, Chenrui Cao, Lei Qi, Rui Zhang, Zidong Du, Jie Yan, Xing Hu
cs.AI
Аннотация
Автоформализация направлена на перевод математических утверждений, выраженных на естественном языке, в формальный язык. Хотя крупные языковые модели (LLM) ускорили прогресс в этой области, существующие методы по-прежнему страдают от низкой точности. Мы выделяем два ключевых навыка для эффективной автоформализации: глубокое владение знаниями в области формального языка и способность к рассуждению, включающую понимание задач на естественном языке и их точное сопоставление с формальными выражениями. Без первого навыка модель не может идентифицировать правильные формальные объекты; без второго она испытывает трудности с интерпретацией реальных контекстов и их точным отображением в формальные выражения. Для устранения этих пробелов мы представляем ThinkingF — конвейер синтеза данных и обучения, который улучшает оба навыка. Сначала мы создаем два набора данных: один путем дистилляции и отбора крупномасштабных примеров, богатых формальными знаниями, а другой — путем генерации траекторий рассуждений от неформального к формальному, руководствуясь шаблонами, разработанными экспертами. Затем мы применяем SFT и RLVR с этими наборами данных для дальнейшего объединения и уточнения двух навыков. Полученные модели на 7B и 32B параметров демонстрируют как глубокие знания в области формального языка, так и сильные способности к рассуждению от неформального к формальному. Примечательно, что модель StepFun-Formalizer-32B достигает рекордных показателей BEq@1: 40,5% на FormalMATH-Lite и 26,7% на ProverBench, превосходя все предыдущие универсальные и специализированные модели.
English
Autoformalization aims to translate natural-language mathematical statements
into a formal language. While LLMs have accelerated progress in this area,
existing methods still suffer from low accuracy. We identify two key abilities
for effective autoformalization: comprehensive mastery of formal-language
domain knowledge, and reasoning capability of natural language problem
understanding and informal-formal alignment. Without the former, a model cannot
identify the correct formal objects; without the latter, it struggles to
interpret real-world contexts and map them precisely into formal expressions.
To address these gaps, we introduce ThinkingF, a data synthesis and training
pipeline that improves both abilities. First, we construct two datasets: one by
distilling and selecting large-scale examples rich in formal knowledge, and
another by generating informal-to-formal reasoning trajectories guided by
expert-designed templates. We then apply SFT and RLVR with these datasets to
further fuse and refine the two abilities. The resulting 7B and 32B models
exhibit both comprehensive formal knowledge and strong informal-to-formal
reasoning. Notably, StepFun-Formalizer-32B achieves SOTA BEq@1 scores of 40.5%
on FormalMATH-Lite and 26.7% on ProverBench, surpassing all prior
general-purpose and specialized models.