Lean Refactor: Agentic Strategy Search를 통한 증명 최적화

왜 중요한가

Lean/Mathlib의 잦은 업데이트 주기 속에서 LLM의 지식 cutoff이 현실과 동떨어진 경우가 많다. Lean Refactor는 전략 은행을 이용한 inference-time retrieval으로 다중 목표를 조정하고 버전 호환성을 유지하며 재학습 없이도 성능을 달성한다.

핵심 기여

전략 은행의 대형 코퍼스 공개

200K 장-단문 증명쌍과 9,237개 고유 전략으로 구성된 전략 은행을 구축하고, 각 전략에 컴파일 시간 감소 및 버전 호환성 메타데이터를 부여한다.

다객체 최적화 및 버전 호환성 보장

Proof 길이, 컴파일 시간, Lean/Mathlib 버전 간의 trade-off를 inference-time에 제어하는 다목적 검색 및 재정렬을 제공한다.

LLM-agnostic, 훈련 없이 운용

프런티어 LLM에 의존하지 않고 strategy bank를 조회해 refactoring을 수행하는 플러그-앤-플레이 에이전트 루프를 제시한다.

핵심 아이디어 이해하기

[단계 1] 문제 정의: Lean 증명은 길이와 컴파일 비용, 버전 호환성이라는 상충 가능한 다중 목표를 가진다. 단일 축으로 최적화하는 기존 접근은 이 상호작용을 놓치기 쉽다. [단계 2] 해결 원리: 전략 은행에 densely annotated한 refactoring 패턴을 저장하고, inference 시점에 목표를 재구성해 다목적 최적화를 추진한다. [단계 3] 기대 효과: 버전 간 전이성과 컴파일 시간 개선을 동시에 달성하고, LLM의 지식 cutoff에 의한 한계를 은행 메타데이터로 보완한다.

방법론

단락 1: Dense 전략 은행과 버전-aware 메타데이터의 구성 원리. 전략은 제목/설명/When to Apply/적용 가이드/예시/감소 정도로 구성되며, 컴파일 시간 감소와 버전 호환성 메타데이터가 포함된다. 단락 2: Multi-Objective Retrieval 설계. 쿼리-전략 매핑에서 코사인 유사도와 컴파일-비용 감소를 결합한 재정렬/필터링으로 목표를 달성한다. 단락 3: Plug-and-Play 에이전트 루프. Retrieval-Planer-Refactorer-Debugger의 순환으로 증명을 점진적으로 축약하고, 컴파일 실패 시 국소적 수정을 거친다.

주요 결과

경쟁 벤치마크에서 Proof 길이 압축은 최대 70% 이상, miniF2F/PutnamBench/Putnam2025에서 우수한 성능을 보인다. 연구 벤치마크에서도 평균 20% 이상 압축이 관찰되며, 여러 벤치에서 버전 호환성 유지 및 zero-shot 전이 성능 향상을 확인했다. 컴파일 시간 측면에서 평균 최대 60%의 감소를 보고하지만, 일부 케이스에서 버전 간 불일치로 상대 컴파일 시간이 증가하는 현상도 관찰되었다. 버전 필터링 Retrieval은 특정 Lean 버전으로의 전이에서 일관된 이점을 제공한다.

실무 활용

전략 은행을 통한 인퍼런스 시점의 다목적 최적화로 Lean 증명 유지보수와 버전 관리에 실용적 이점을 제공한다.

Lean/Mathlib 버전 간의 자동 리팩토링 파이프라인 지원
대회 문제/연구 수준 증명의 간략화 및 검증 속도 향상
Verifiable code generation 및 PDE 같은 수학-검증 도메인에서의 증명 품질 향상

코드 공개 여부: 미확인

키워드

LeanMathlibretrieval-augmentedmulti-objectiveversion-robustcompressionverification

용어 해설

검색 기반 보강(Retrieval-Augmented): — 정보를 필요로 하는 문제에 대해 외부 지식을 검색해 보충하는 기법으로, LLM의 응답 정확도와 효율성을 높이고 도메인 버전에 대한 민감도를 낮춘다.
버전 관리(Versioning): — Lean/Mathlib의 잦은 릴리스에 따른 API/명의 변경으로 생기는 호환성 문제를 다루는 용어로, 버전-구성 메타데이터를 활용한 안정화 전략을 의미한다.
전략 은행(Strategy Bank): — 다중 목표 최적화에 사용할 refactoring 전략의 모음과 각 전략의 실행 시점, 버전 호환성 등 메타데이터를 포함한 데이터베이스.

Lean Refactor: Agentic Strategy Search를 통한 증명 최적화

왜 중요한가

핵심 기여

핵심 아이디어 이해하기

방법론

주요 결과

실무 활용

키워드

용어 해설

관련 토론

댓글

관련 기사

AI가 생성한 코드의 완벽한 정확성을 보장하는 형식 검증과 Lean

LLM과 Lean으로 MILP 재정식화를 검증하는 FLARE

왜 중요한가

핵심 기여

핵심 아이디어 이해하기

방법론

주요 결과

실무 활용

키워드

관련 토론

댓글

관련 기사

AI가 생성한 코드의 완벽한 정확성을 보장하는 형식 검증과 Lean

LLM과 Lean으로 MILP 재정식화를 검증하는 FLARE