본 논문은 AI 기반 형식적 수학 추론 분야의 발전과 그 응용 분야 중 하나인 형식적 검증에 초점을 맞추고 있다. GPT-4를 활용하여 Coq, Lean4, Dafny, ACSL, TLA+ 등 5가지 형식 명세 언어에 대한 18,000개의 고품질 instruction-response 쌍을 생성하고, DeepSeek-R1을 포함한 10개의 오픈소스 LLM을 대상으로 평가하였다. 또한, 7~8B 규모의 소형 모델들을 fine-tuning하여 DeepSeek-R1-671B와 유사한 성능을 달성하였으며, 형식적 데이터를 이용한 fine-tuning이 수학, 추론, 코딩 능력 향상에도 기여함을 확인하였다. Fine-tuning된 모델들은 Hugging Face에 공개되었다.
