DRIFT: 정리 자동 형식화를 위한 분해, 검색, 예시 제시, 그리고 형식화 프레임워크

이 논문은 대규모 언어 모델 (LLM) 이 자연어로 된 수학 명제를 기계가 검증 가능한 형식 언어 (예: Lean 4) 로 변환하는 자동 형식화 (Autoformalization) 작업의 한계를 극복하기 위해 제안된 새로운 프레임워크 DRIFT를 소개합니다.

1. 문제 정의 (Problem)

기존의 검색 증강 생성 (RAG) 기반 자동 형식화 방법론은 다음과 같은 근본적인 한계를 가지고 있습니다:

• 복잡한 쿼리: 자연어 수학 명제는 여러 개념이 밀집되어 있어, 이를 그대로 검색 쿼리로 사용하면 정확한 정의나 보조 정리 (premise) 를 찾기 어렵습니다.
• 문맥 부재: 검색된 형식적 정의 (예: ZMod, IsPrimitiveRoot) 는 모델에게 해당 정의의 **구문적 사용법 (syntax)**과 적용 패턴을 제공하지 못합니다. 이로 인해 모델은 정의는 알지만 이를 올바른 Lean 문법으로 구조화하는 데 실패하거나, 존재하지 않는 객체를 생성하는 할루시네이션을 일으킵니다.
• 단일 쿼리 의존: 기존 방법들은 복잡한 명제를 하나의 덩어리로 취급하여 검색하므로, 수학 정리의 의존성 구조 (dependency structure) 를 반영하지 못합니다.

2. 방법론 (Methodology: DRIFT)

DRIFT (Decompose, Retrieve, Illustrate, Formalize Theorems) 는 네 단계로 구성된 파이프라인을 통해 위 문제를 해결합니다.

① 분해 (Decompose)

• 목표: 복잡한 자연어 명제를 더 작고 다루기 쉬운 "서브-쿼리 (sub-queries)"로 분할합니다.
• 작동 방식: LLM 이 입력된 명제를 분석하여, 각 수학적 개념 (예: "소수 p", "원시근", "곱셈 차수") 에 해당하는 개별적인 자연어 설명과 예측된 Lean 형식 표현을 포함하는 구조화된 서브-쿼리 세트를 생성합니다.
• 효과: 단일 밀집 벡터 검색의 한계를 극복하고, 각 개념별로 정밀한 검색을 가능하게 합니다.

② 검색 (Retrieve)

• 목표: 분해된 각 서브-쿼리에 해당하는 형식 라이브러리 (Mathlib 등) 의 의존성 (premises) 을 찾습니다.
• 작동 방식: 밀집 Passage 검색기 (Dense Passage Retriever, DPR) 를 사용하여 각 서브-쿼리를 인코딩하고, 가장 유사한 형식적 정의나 정리를 검색합니다.
• 특징: 전체 명제가 아닌 개념 단위로 검색함으로써 더 정확한 의존성 매핑을 달성합니다.

③ 예시 제시 (Illustrate)

• 목표: 검색된 정의들의 실제 사용 예시를 제공합니다.
• 작동 방식: 검색된 의존성 (premises) 을 활용하는 실제 정리 (theorems) 를 라이브러리에서 선별합니다. 탐욕 알고리즘 (Greedy algorithm) 을 사용하여 검색된 의존성들을 최대한 많이 커버하는 소수의 예시 정리를 선택합니다.
• 효과: 모델에게 정의의 문법적 사용법 (syntax) 과 적용 패턴을 구체적인 예시 (In-context learning) 로 제공하여 형식화 오류를 줄입니다.

④ 정리 형식화 (Formalize Theorems)

• 목표: 최종 형식 명제를 생성합니다.
• 작동 방식: 원래 명제, 검색된 의존성, 그리고 예시 정리를 모두 컨텍스트로 포함하여 LLM 에게 형식화 작업을 지시합니다.

3. 주요 기여 (Key Contributions)

1. 새로운 프레임워크 제안: DRIFT 는 자연어 명제를 분해하고 검색된 의존성을 예시 정리로 문맥화하는 최초의 체계적인 접근법입니다. 이는 형식 정의와 문법적 사용법 사이의 격차를 해소합니다.
2. 성능 기록 갱신: ProofNet(내부 분포) 과 ConNF(외부 분포) 벤치마크에서 기존 최첨단 (SOTA) 방법론인 RAutoformalizer (RAuto) 와 제로샷 (Zero-shot) 베이스라인을 능가하는 성능을 기록했습니다.
3. 적응형 검색의 중요성 규명: 검색의 효과는 모델의 사전 지식 (parametric knowledge) 과 명제의 복잡성 사이의 간격에 크게 의존함을 분석을 통해 증명했습니다. 이는 모델의 능력에 맞춘 적응형 검색 전략의 필요성을 시사합니다.

4. 실험 결과 (Results)

실험은 ProofNet, MiniF2F-test, ConNF 세 가지 벤치마크에서 수행되었으며, GPT-4.1, DeepSeek-V3.1, Goedel-V2-8B 등 다양한 모델을 사용했습니다.

• 검색 성능 (Dependency Retrieval):
  • ProofNet 에서 DRIFT 는 베이스라인 (단일 쿼리) 대비 F1 점수를 약 2 배 가까이 향상시켰습니다 (13.77% → 27.68% 등).
  • 분해 (Decompose) 모듈이 검색의 정밀도 (Precision) 와 재현율 (Recall) 을 모두 크게 개선했습니다.
• 형식화 정확도 (Formalization Correctness):
  • ProofNet: GPT-4.1 기준 BEq+@10 점수가 19.25% (DPR) 에서 **21.93% (DRIFT)**로 향상되었습니다.
  • ConNF (외부 분포): DRIFT 는 극적인 개선을 보였습니다. GPT-4.1 의 BEq+@10 점수가 20.08% (DPR) 에서 **62.33% (DRIFT)*로 급증하여, 불완전한 오라클 (Oracle) 설정을 능가하기도 했습니다. 이는 예시 제시 (Illustrate) 모듈이 새로운 도메인에서의 문법적 구조 학습에 결정적 역할을 했음을 시사합니다.
  • MiniF2F-test: 의존성이 적은 간단한 문제에서는 검색이 오히려 방해가 될 수 있어 성능 향상이 제한적이었으나, DRIFT 는 여전히 경쟁력 있는 성능을 유지했습니다.
• Ablation Study:
  • '예시 제시 (Illustrate)' 모듈을 제거하면 BEq+ 점수가 크게 하락하여, 정의뿐만 아니라 사용 예시가 형식화 정확도에 필수적임을 입증했습니다.
  • '분해 (Decompose)' 모듈을 제거하면 검색된 의존성이 더 다양해지지만, 예시 정리가 이를 안내해주지 않으면 성능이 저하될 수 있음을 보여주었습니다.

5. 의의 및 결론 (Significance)

DRIFT 는 자동 형식화 분야에서 다음과 같은 중요한 통찰을 제공합니다:

• 구조적 접근의 필요성: 수학 명제를 단순한 텍스트가 아닌, 개념들의 집합으로 분해하여 처리해야 정확한 형식화가 가능합니다.
• 문맥의 중요성: 형식적 정의만 제공하는 것은 불충분하며, 실제 사용 예시 (Exemplars) 를 통해 문법과 논리 구조를 학습시켜야 합니다.
• 적응형 전략: 모델의 내부 지식과 외부 검색 정보의 균형을 맞추는 적응형 전략이 향후 연구의 핵심 방향임을 강조합니다.

이 연구는 LLM 이 복잡한 수학 정리를 형식화할 때 발생할 수 있는 문법적 오류와 논리적 불일치를 줄이고, 특히 외부 분포 (Out-of-Distribution) 데이터에 대한 일반화 능력을 크게 향상시킴으로써 자동 증명 시스템의 실용성을 높이는 데 기여합니다.