기술 요약: Lean 리팩토링

문제 정의

강화 학습 (RL) 을 통해 Lean 에서 형식적 정리 증명에 훈련된 대규모 언어 모델 (LLM) 은 종종 정확하지만 극도로 장황하고, 취약하며, 계산적으로 비용이 많이 드는 증명을 생성합니다. 기존 리팩토링 노력들이 존재하지만, Lean 생태계에 적용될 때 세 가지 근본적인 한계에 직면합니다:

1. 다목적 긴장 관계: Lean 리팩토링은 본질적으로 다목적적입니다. 증명 길이를 최적화하는 것은 종종 컴파일 비용 최소화와 충돌합니다 (예: 더 짧은 증명이 컴파일 시간을 부풀리는 무거운 전술을 호출할 수 있음). 기존 방법들은 이러한 트레이드오프를 균형 있게 조정하거나 추론 시에 보지 못한 사용자 목적에 적응할 수 있는 원칙적인 메커니즘이 부족합니다.
2. 버전 취약성: Lean 과 그 표준 라이브러리인 Mathlib 는 빈번한 API 변경과 정리 이름 변경과 함께 거의 매주 진화합니다. 최첨단 LLM 은 정적인 지식 컷오프를 가지므로, 구식 전술을 환각하거나 현재 도구 체인과의 호환성 문제를 일으킵니다.
3. 데이터 부족: 주류 프로그래밍 언어와 달리 Lean 은 훈련 기반 리팩토링 파이프라인에 필요한 대규모 쌍을 이룬 데이터셋 (노이즈가 있는 코드와 정제된 코드 쌍) 이 부족합니다. 또한, 훈련 기반 접근 방식은 새로운 LLM 릴리스마다 반복적인 미세 조정이 필요하여 모델 교체나 Lean 의 릴리스 주기에 따라 확장되지 못합니다.

방법론: Lean Refactor

저자들은 기존 LLM 을 미세 조정하지 않고 Lean 증명을 리팩토링하도록 설계된 플러그인 및 플레이 방식의 검색 증강 에이전트 프레임워크인 Lean Refactor를 제안합니다. 이 시스템은 지식을 구조화되고 밀집하게 주석된 데이터베이스로 외부화함으로써 리팩토링 논리를 모델에서 분리합니다.

1. 밀집하게 주석된 전략 은행

프레임워크의 핵심은 20 만 개 이상의 장 - 단 증명 쌍에서 정제된 9,237 개의 고유한 리팩토링 전략으로 구성된 선별된 데이터베이스입니다.

• 구조: 각 전략에는 제목, 설명, 전제 조건 ("언제 적용할지"), 단계별 적용 가이드, 그리고 추상적인 전후 예제가 포함됩니다.
• 메타데이터: 중요한 점은 각 전략이 LLM 이 훈련 데이터에서 추론할 수 없는 메타데이터로 주석되어 있다는 것입니다:
  • 컴파일 시간 감소: 전략을 적용했을 때 관찰된 중앙값 상대 속도 향상.
  • 버전 호환성: 리팩토링된 증명이 성공적으로 컴파일되는 검증된 Lean/Mathlib 도구 체인 집합 (예: v4.14.0, v4.16.0, v4.22.0). 이는 여러 버전에서 단축된 증명을 재컴파일하여 결정됩니다.

2. 다목적 검색 및 재순위화

추론 시, 프레임워크는 모델 재훈련 없이 사용자 지정 목적에 적응하는 검색 파이프라인을 사용합니다:

• 가장 짧은 증명: 증명 세그먼트에 대한 의미적 유사성 (코사인 유사도) 을 기반으로 전략을 검색합니다.
• 컴파일 시간 인식: 의미적으로 유사한 후보들의 광범위한 풀을 검색한 다음, 주석된 컴파일 비용 감소 메타데이터를 기반으로 이를 재순위화합니다.
• 버전 특정: 후보 풀을 필터링하여 사용자의 목표 Lean 버전을 포함하는 호환성 메타데이터를 가진 전략만 포함합니다.

3. 에이전트 루프

프레임워크는 다음으로 구성된 모델 중립 에이전트 루프로 이러한 구성 요소를 감쌉니다:

• 계획자: 검색된 전략에 기반하여 리팩토링 작업을 구체적인 단계로 분해합니다.
• 리팩토러: 더 짧은 증명을 생성하기 위해 계획을 실행합니다.
• 디버거: 폐쇄 루프 (최대 $D$라운드) 에서 컴파일러 피드백을 사용하여 오류를 수정합니다.
• 백본 중립성: 계획자, 리팩토러, 디버거는 모든 고정된 최첨단 LLM (예: Gemini, Claude, GPT 시리즈) 으로 인스턴스화될 수 있어, 재훈련 없이 모델 간에 시스템을 이전할 수 있습니다.

주요 기여

1. 데이터셋 공개: 저자들은 현재까지 가장 큰 Lean 리팩토링 데이터셋을 공개합니다. 이는 20 만 개 이상의 장 - 단 증명 쌍과 9 천 개의 리팩토링 전략으로 구성되며, 각각 컴파일 비용과 버전 호환성으로 주석되어 있습니다.
2. 성능: Lean Refactor 는 경쟁 벤치마크 (miniF2F, PutnamBench) 에서 70% 이상의 토큰 수준 압축을 달성하고, 연구용 저장소 (Analysis, FLT, PhysLean) 에서는 20% 이상을 달성합니다. 또한 경쟁 벤치마크에서 컴파일 시간을 최대 **60%**까지 감소시킵니다.
3. 제어 가능성 및 견고성: 이 시스템은 모델 가중치가 아닌 검색 규칙을 통해 다목적 제어 (길이 대 속도 대 호환성) 를 지원합니다. 리팩토링된 증명은 리팩토링되지 않은 대응물 및 이전 최적화 방법보다 향후 Lean 릴리스에 대한 제로샷 버전 이전이 더 강력하게 나타납니다.
4. 모델 중립성: 이 프레임워크는 다양한 LLM 백본 (Gemini 3 Flash, Claude Haiku 4.5) 에서 성능을 향상시키며, 동일한 전략 검색 도구를 제공받더라도 Claude Code 와 같은 범용 코딩 에이전트보다 우수한 성과를 냅니다.

실험 결과

• 길이 감소: 경쟁 벤치마크에서 Lean Refactor 는 이전 최첨단인 ProofOptimizer 를 능가하여 miniF2F 에서 88.40%, PutnamBench 에서 70.38% 의 감소를 달성했습니다 (ProofOptimizer 는 57.20%). 연구 수준의 증명에서는 평균 20~33% 의 감소를 달성하여 절단 기준선보다 훨씬 우수한 성과를 보였습니다.
• 컴파일 시간: 컴파일 비용 메타데이터에 기반하여 전략을 재순위화함으로써, 이 프레임워크는 PutnamBench 에서 표준 검색 접근 방식의 37.11% 대비 **42.62%**의 상대적 컴파일 시간 감소를 달성합니다.
• 버전 호환성: 특정 Lean 버전 (예: v4.16.0) 을 대상으로 할 때, 버전 필터링된 검색은 필터링되지 않은 검색보다 일관되게 더 나은 길이 감소를 제공합니다. 리팩토링된 증명은 ProofOptimizer 나 원래의 장황한 증명보다 더 많은 향후 Lean 릴리스 (최대 v4.29.0) 에서 타입 체킹 능력을 유지합니다.
• 의존성 감소: 리팩토링된 증명은 42~67% 의 사례에서 외부 및 프로젝트 내 의존성을 감소시켜, 무거운 라이브러리 정리로 단순히 이전하는 것이 아니라 진정한 논리적 단순화를 나타냅니다.

중요성

이 논문은 Lean Refactor 가 형식적 수학 라이브러리 유지 관리의 중요한 병목 현상, 즉 증명의 간결성과 컴파일 효율성 사이의 긴장 관계, 그리고 급격히 진화하는 도구 체인 전반에 걸친 코드의 취약성을 해결한다고 주장합니다. 리팩토링 지식을 메타데이터가 풍부한 전략 은행으로 외부화함으로써, 이 프레임워크는 값비싼 모델 미세 조정 없이 제어 가능한 다목적 최적화를 가능하게 합니다. 이 접근 방식은 Lean/Mathlib 버전 드리프트에 대해 시스템이 견고하게 유지되도록 하고, 새로운 LLM 백본에 즉시 적응할 수 있게 하여, 더 유지 가능하고 버전 내성을 갖춘 형식적 증명의 기초를 마련합니다.