Lean 리팩터: 에이전트 전략 탐색을 통한 다목적 제어 가능 증명 최적화

연구진은 고정된 LLM과 정제된 전략 데이터베이스를 활용해 Lean 증명을 리팩터링하는 플러그앤플레이 프레임워크 ‘Lean Refactor’를 제안했다.

이 시스템은 증명 길이 단축, 컴파일 비용 감소, 그리고 Lean·Mathlib 버전 간 강건성 향상을 목표로 한다.

실험에서 Lean Refactor는 높은 압축 효과, 더 빠른 컴파일, 그리고 버전 간 전이 성능 개선을 보였다.

이 접근은 모델과 Lean이 바뀔 때마다 반복 재학습이 필요 없는 실용적 형식 검증 병목 해소 방안이다.