본 논문은 수학의 형식화 과정에서 중요한 단계인 전제(premise) 검색을 효율적으로 수행하는 새로운 방법을 제시한다. 기존의 자연어 기반 검색 방법은 사용자의 수학적 전문 지식을 요구하고, 형식 언어(예: Lean) 기반 방법은 학습 데이터 부족으로 성능이 저하되는 문제점을 가지고 있다. 본 연구는 Mathlib에서 추출한 데이터를 활용하여 경량화되면서 효과적인 전제 검색 모델을 학습시켰다. 특히, 형식 언어 코퍼스에 특화된 토크나이저를 사용하여 질의(Lean이 제공하는 증명 상태)와 전제를 잠재 공간에 임베딩하고, 미세한 유사도 계산 방법과 재순위 지정 모듈을 적용하여 성능을 향상시켰다. 실험 결과, 제안된 모델은 기존 방법보다 높은 정확도와 낮은 계산 비용을 달성함을 보였다. 개발된 검색 엔진은 공개 소스로 제공된다.
