본 논문은 대규모 언어 모델(LLM)이 추상적 구조를 구체적인 설정에 적용하여 발생하는 정리를 공식화하는 데 어려움을 겪는 문제를 해결하기 위해, 연구 수준의 수학적 결과를 자동 공식화하는 것을 목표로 구조-인스턴스 정리 자동 공식화(SITA) 프레임워크를 개발했다. SITA는 추상 수학 이론과 Lean 증명 보조 도구에서의 구체적인 적용 사이의 격차를 체계적으로 연결한다. 공식화된 추상 구조는 정의, 가정, 연산 및 정리로 구성된 모듈식 템플릿으로 취급되며, 이는 구체적인 인스턴스 공식화를 위한 재사용 가능한 가이드 역할을 한다. 구체적인 인스턴스가 주어지면, 해당 Lean 정의 및 인스턴스 선언을 생성하고, Lean의 타입클래스 메커니즘을 사용하여 통합하며, 구조적 가정을 확인하여 검증된 정리를 구성한다. 자동화와 형식적 정확성을 보장하기 위해 피드백 기반 개선을 통해 LLM 기반 생성을 통합했다. 최적화 문제 데이터세트에 대한 실험을 통해 SITA가 추상 구조에 기반한 다양한 인스턴스를 효과적으로 공식화함을 입증했다.
