StepFun-Formalizer: Unlocking the Autoformalization Potential of LLMs through Knowledge-Reasoning Fusion
Created by
Haebom
저자
Yutong Wu, Di Huang, Ruosi Wan, Yue Peng, Shijie Shang, Chenrui Cao, Lei Qi, Rui Zhang, Zidong Du, Jie Yan, Xing Hu
개요
본 논문은 자연어 수학적 명제를 형식 언어로 변환하는 자동 형식화(Autoformalization) 분야에서, 기존 방법들의 낮은 정확도 문제를 해결하기 위해 ThinkingF라는 데이터 합성 및 훈련 파이프라인을 제안합니다. ThinkingF는 형식 언어 도메인 지식과 자연어 문제 이해 및 비형식-형식 정렬 추론 능력이라는 두 가지 핵심 능력 향상에 중점을 둡니다. 대규모 형식 지식 데이터셋과 전문가가 설계한 템플릿을 기반으로 비형식-형식 추론 경로를 생성하는 데이터셋을 구성하고, SFT와 RLVR을 적용하여 두 능력을 융합 및 개선합니다. 결과적으로, 7B 및 32B 모델은 포괄적인 형식 지식과 강력한 비형식-형식 추론 능력을 보이며, 특히 StepFun-Formalizer-32B는 FormalMATH-Lite에서 40.5%, ProverBench에서 26.7%의 SOTA BEq@1 점수를 달성하여 기존의 일반 목적 및 특수 모델들을 능가합니다.
시사점, 한계점
•
시사점:
◦
자동 형식화 분야에서 형식 지식과 추론 능력 향상을 위한 효과적인 데이터 합성 및 훈련 파이프라인을 제시.
◦
대규모 언어 모델을 활용하여 FormalMATH-Lite 및 ProverBench에서 SOTA 성능 달성.
◦
형식 지식과 추론 능력의 융합을 통해 자동 형식화의 정확도 향상 가능성 제시.
•
한계점:
◦
ThinkingF 파이프라인의 일반화 성능 및 다양한 수학 분야에 대한 적용 가능성에 대한 추가적인 연구 필요.
◦
전문가가 설계한 템플릿에 대한 의존도가 높아, 템플릿 설계의 품질이 성능에 큰 영향을 미칠 수 있음.
