딥러닝과 형식 수학의 융합으로 형식 검증 연구가 활발히 진행되고 있으며, 특히 자연어 설명을 기계 검증 가능한 표현으로 변환하는 자동 형식화가 중요한 과제로 부각되고 있습니다. 기존 방법들은 맥락 인식 부족, 라이브러리 의존성 검색의 정확도 및 재현율 저하, 대규모 데이터셋 활용의 어려움 등의 문제점을 안고 있습니다. 본 연구에서는 DDR (Direct Dependency Retrieval) 기반의 새로운 검색 증강 프레임워크를 제안합니다. DDR은 자연어 수학적 설명에서 직접 후보 라이브러리 의존성을 생성하고, 효율적인 접미사 배열 검사를 통해 형식 라이브러리 내 존재 여부를 확인합니다. DDR 모델을 통해 구축된 50만 개 이상의 데이터셋으로 훈련한 결과, 기존 SOTA 방법들을 능가하는 정확도와 재현율을 달성했습니다. DDR 기반 자동 형식화기는 기존의 선택 기반 RAG 방법론을 사용하는 모델보다 일관된 성능 우위를 보였습니다.
