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