Lean Refactor: 멀티-객체 리팩토링 에이전트로 증명 길이 70% 압축, 버전 호환성까지 개선

Jialin Lu 팀이 Lean 증명의 길이·컴파일 비용·버전 호환성을 동시에 개선하는 플러그앤플레이 에이전틱 프레임워크 Lean Refactor를 공개했습니다. 사전 구축된 전략 DB에서 멀티-객체 리팩토링 전략을 검색해 frozen LLM을 제어하는 방식으로, 경쟁 벤치마크에서 70% 이상의 토큰 압축과 최대 60%의 컴파일 시간 단축을 달성했습니다. 버전-필터링 검색으로 대상 Lean 버전에 맞춘 압축이 가능하며, 리팩토링된 증명이 향후 Lean 릴리스로의 제로샷 버전 전이에서도 더 강한 성능을 보였다는 점이 흥미로운 포인트입니다. 다만 실험은 특정 LLM과 전략 DB에 의존하므로, 새로운 모델이나 라이브러리 버전에서의 일반화는 추가 검증이 필요합니다.

• #lean
• #proof-refactoring
• #agentic-framework
• #llm
• #version-robust