자동 형식화(Autoformalization)는 비공식적인 자연어(natural language)를 기계가 검증 가능한 공식 언어로 변환하는 기술입니다. 대부분의 연구가 개별 명제에 초점을 맞추고 있지만, 실제 형식화 노력은 본질적으로 이론 수준(theory-level)에 있습니다. 즉, 목표 정리(target theorems)를 진술하기 위해서는 전체 공리(axioms), 정의(definitions), 그리고 보조정리(lemmas)의 웹이 필요합니다. 본 포지션 페이퍼(position paper)에서 우리는 이론 수준 자동 형식화, 즉 모든 상호 의존성을 포함하는 완전한 이론들을 구조화된 라이브러리로 공식화할 것을 주장합니다. 우리는 이러한 변화의 중요성을 검토하고, 대안적인 관점들을 다루며, 열려 있는 과제들(open challenges)을 식별하고, 세 가지 유망한 향후 경로를 제안합니다. 자동 형식화에 대한 우리의 조사 자료는 https://github.com/marcusm117/Awesome-Autoformalization에서 확인할 수 있습니다.