기술 요약: LeanSearch v2

문제 정의: 전역 전제 검색

이 논문은 Lean 4 생태계 내 자동 증명에서 중요한 격차를 지적합니다. 기존 도구들은 의미론적 검색(쿼리와 일치하는 개별 선언 찾기) 또는 전제 선택(단일 전술 단계에 유용한 보조정리 예측) 에 뛰어나지만, 전역 전제 검색에서는 실패합니다.

전역 전제 검색은 전체 정리를 증명하는 데 필요한 완전하고 논리적으로 일관된 라이브러리 보조정리 집합을 식별하는 작업으로 정의됩니다. 이는 단일 관련 문서를 찾는 것과 구별되는데, 그 이유는 다음과 같습니다:

1. 비국소성: 필요한 보조정리들은 종종 라이브러리 (Mathlib) 의 먼 모듈에 위치하며 문제 진술과 어휘적 중복을 공유하지 않습니다.
2. 전략적 의존성: 문제와 보조정리 간의 연결은 의미론적이 아니라 구조적이며, 증명 전략의 "논리적 아키텍처"(예: 목표의 재구성을 통해 정리 인터페이스와 일치시킴) 에 의존합니다.
3. 완전성: 세 개 또는 네 개의 보조정리 집합에서 하나의 필수 보조정리가 누락되면 증명이 불완전해지며, 이는 표준 문서 관련성 지표에서 포착되지 않는 실패 모드입니다.

저자들은 효과적인 전역 전제 검색 없이는 AI 증명기들이 기존 지역 보조정리를 재증명하는 데 연산 자원을 낭비하고, 효율적이고 관례적인 증명 생성에 어려움을 겪는다고 주장합니다.

방법론: LeanSearch v2

LeanSearch v2 는 이 과제를 해결하도록 설계된 두 가지 모드의 검색 시스템입니다.

1. 표준 모드 (검색 기저)

표준 모드는 개별 Mathlib 선언을 위한 고성능 검색 엔진으로 기능하며, 추론 모드의 기반이 됩니다.

• 코퍼스 구성: 시스템은 Mathlib 의 모든 선언을 추출하기 위해 정적 분석 도구인 Jixia를 활용합니다. 이는 의존성 그래프를 구축하고 하향식 계층 비형식화를 수행합니다. 이 과정은 각 선언의 이미 비형식화된 의존성 설명을 통합하여 자연어 설명을 생성함으로써, 설명이 불투명한 식별자가 아닌 수학적 개념에 기반하도록 보장합니다.
• 파이프라인: 도메인 특화 미세 조정 없이 오프더셸 모델 (Qwen3-Embedding-8B 및 Qwen3-Reranker-8B) 을 사용하는 2 단계 임베딩–재순위화 파이프라인을 채택합니다.
  • 임베딩: 쿼리와 코퍼스 항목은 선언 종류, 타입 시그니처, 비형식화된 설명을 포함하는 구조화된 패시지 템플릿을 사용하여 인코딩됩니다.
  • 재순위화: 정의와 인스턴스를 특별히 처리하여 기존 시스템에서 관찰된 검색 어려움을 극복하는 종류 인식형 재순위화기가 쿼리 - 후보 쌍에 점수를 매깁니다.

2. 추론 모드 (전역 전제 검색)

추론 모드는 표준 모드를 기반으로 스케치–검색–반성 반복 루프를 통해 전제 집합을 검색합니다.

• 스케치 생성: 정리 진술을 받으면 생성기 (Claude Sonnet 4.5) 가 단계별 증명 개요를 제안하며, 정리를 하위 쿼리로 분해합니다. 이는 코드를 작성하는 것이 아니라 수학적 이동과 검색 의도를 정의합니다.
• 검색 및 필터링: 각 하위 쿼리는 표준 모드로 전송됩니다. 필터 모델 (Kimi K2 Instruct) 은 상위 후보를 심사하며, 특정 단계에 검색된 보조정리가 genuinely 유용하지 않은 경우 빈 집합을 명시적으로 허용합니다.
• 실현 가능성 판단 및 반성: 판사 모델이 필터링된 결과를 검사합니다.
  • 보조정리 집합이 증명 전략을 지원하면 루프가 종료됩니다.
  • 집합이 불충분한 경우 (예: 전제 누락 또는 유효하지 않은 경로 제안), 판사는 구조화된 피드백을 스케치 수정기에 제공하여 증명 개요를 수정하고 루프로 다시 진입시킵니다.
• 집계: 최종 출력은 하위 쿼리 간 순위 할인 규칙을 사용하여 집계되어 지원 보조정리의 통합 목록을 형성합니다.

주요 기여

1. 작업 공식화: 이 논문은 단일 문서가 아닌 논리적으로 일관된 전제 집합의 복원을 요구하는 고유한 과제로서 전역 전제 검색을 공식적으로 정의합니다.
2. 벤치마크: 전문가가 선별한 두 가지 벤치마크가 소개됩니다.
   • MathlibQR: 표준 모드 평가를 위한 200 개의 선언과 946 개의 단일 쿼리 검색용 쿼리.
   • MathlibMPR: 전역 전제 검색 (추론 모드) 평가를 위해 병합된 풀 리퀘스트에서 가져온 69 개의 정리와 전문가가 주석한 전제 그룹 (정리당 1~8 개).
3. 시스템 성능: LeanSearch v2 는 도메인 특화 미세 조정 없이 최첨단 결과를 달성합니다.
   • 표준 모드: MathlibQR 에서 nDCG@10 을 0.62로 달성하여 차기 최우수 시스템 (0.53) 을 능가합니다.
   • 추론 모드: MathlibMPR 에서 상위 10 개 후보 내에서 **46.1%**의 실제 전제 그룹을 복원하여, 추론 검색 베이스라인 (38.0%) 과 전제 선택 시스템 (9.3%) 을 크게 능가합니다.
4. 하류 검증: 고정된 증명기 루프를 사용한 통제 실험에서, 다른 검색기를 LeanSearch v2 추론 모드로 교체한 결과 증명 성공률이 **20%**로 증가했습니다 (차기 최우수 시스템은 16%, 검색 없음은 4%). 이는 검색 품질이 직접적으로 증명 생성으로 전파됨을 입증합니다.

중요성과 주장

이 논문은 Lean 전제 검색 문제에 추론–검색 기술을 적용한 최초의 작업으로 이 작업을 위치시킵니다. 저자들은 강력한 에이전트 시스템이 반복적인 쿼리 재형성이나 지역 증명을 통해 약한 검색을 때때로 보상할 수 있지만, 단순히 컴파일되는 증명과 효율적이고 관례적인 증명 사이의 격차는 근본적으로 기존 라이브러리 결과를 식별하고 재사용하는 데 달려 있다고 주장합니다.

중요성은 검색을 형식 수학의 진보를 위한 별도의 축으로 확립하는 데 있습니다. 검색 기저를 증명 생성 루프에서 분리함으로써 시스템은 검색 전략의 독립적인 개선을 가능하게 합니다. 저자들은 방법론이 설계상 언어 중립적이지만, 현재 평가는 Lean 4/Mathlib 에만 국한되며, 이러한 시스템이 복잡한 저장소 수준 작업에서 고도로 능력 있는 에이전트 아키텍처 내에서 어떻게 작동하는지는 향후 탐구의 열린 영역이라고 지적합니다.

이 논문은 계층 비형식화 코퍼스, 종류 인식형 검색 파이프라인, 그리고 반복적 스케치–검색–반성 루프의 결합이 현대 형식 증명에 필요한 산발적이고 비국소적인 보조정리를 찾는 과제를 위한 견고한 해결책을 제공한다고 결론지었습니다.