StepFun-Formalizer: 지식-추론 융합을 통해 LLM의 자동 형식화 잠재력 개방
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
초록
자동 형식화(autoformalization)는 자연어로 표현된 수학적 명제를 형식 언어로 변환하는 것을 목표로 합니다. 대형 언어 모델(LLM)이 이 분야의 발전을 가속화했지만, 기존 방법들은 여전히 낮은 정확도 문제를 안고 있습니다. 우리는 효과적인 자동 형식화를 위해 두 가지 핵심 능력을 식별했습니다: 형식 언어 도메인 지식에 대한 포괄적인 숙달, 그리고 자연어 문제 이해와 비형식-형식 정렬을 위한 추론 능력입니다. 전자가 없으면 모델은 올바른 형식 객체를 식별할 수 없으며, 후자가 없으면 실제 세계의 맥락을 해석하고 이를 정확히 형식 표현으로 매핑하는 데 어려움을 겪습니다. 이러한 격차를 해결하기 위해 우리는 두 가지 능력을 모두 향상시키는 데이터 합성 및 학습 파이프라인인 ThinkingF를 소개합니다. 먼저, 형식 지식이 풍부한 대규모 예제를 정제하고 선별하여 구성한 데이터셋과, 전문가가 설계한 템플릿에 따라 비형식-형식 추론 궤적을 생성한 데이터셋을 구축합니다. 그런 다음 이 데이터셋을 활용해 SFT(지도 미세 조정)와 RLVR(강화 학습 기반 검증 및 개선)을 적용하여 두 능력을 더욱 융합하고 정제합니다. 그 결과, 7B와 32B 모델은 포괄적인 형식 지식과 강력한 비형식-형식 추론 능력을 모두 보여줍니다. 특히, StepFun-Formalizer-32B는 FormalMATH-Lite에서 40.5%, ProverBench에서 26.7%의 SOTA BEq@1 점수를 달성하며, 모든 기존의 범용 및 특화 모델을 능가했습니다.
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.