본 논문은 자동 형식화(autoformalization), 즉 비형식적인 수학적 명제를 검증 가능한 형식적 표현으로 변환하는 과정에 대한 종합적인 개요를 제공한다. 인공지능, 특히 대규모 언어 모델(LLM)의 발전에 힘입어 자동 형식화 분야는 급속한 성장을 이루었고, 새로운 기회와 독특한 과제를 동시에 안겨주었다. 본 논문에서는 수학적 관점과 LLM 중심 관점 모두에서 최근 자동 형식화의 발전을 살펴보고, 다양한 수학 분야와 난이도 수준에서 자동 형식화의 적용 방식을 조사하며, 데이터 전처리부터 모델 설계 및 평가에 이르는 전 과정을 분석한다. 또한 LLM이 생성한 출력의 검증 가능성을 높이는 데 있어 자동 형식화의 새로운 역할을 탐구하고, LLM의 신뢰성과 추론 능력 향상에 대한 잠재력을 강조한다. 마지막으로, 현재 연구를 지원하는 주요 오픈소스 모델과 데이터셋을 요약하고, 이 분야의 미해결 과제와 유망한 미래 방향을 논의한다.
