기술 요약: Proof-Refactor

문제 정의

대규모 언어 모델(LLM)은 Lean과 같은 시스템을 위한 형식적 증명을 생성하는 데 뛰어난 능력을 보여주었으나, 그 출력물은 성숙한 형식 수학 라이브러리(예: Mathlib)의 특징인 모듈성, 가독성, 유지보수성 및 재사용성이 부족한 경우가 많다. 이러한 결함은 대부분의 증명 생성 파이프라인에 내재된 "컴파일 우선(compile-first)" 목표에서 비롯되며, 이는 구조적 품질보다는 이진적 정확성(binary correctness)에 보상을 주는 경향이 있다. 결과적으로, 에이전트들은 증명을 재사용 가능한 라이브러리 구성 요소로 분리하기보다는, 인라인된 인자(inlined arguments), 문제 특화적인 정의, 그리고 자동화에 대한 과도한 의존성을 가진 단일적(monolithic) 스크립트를 생성하는 경향이 있다.

증명 품질을 개선하기 위한 기존 방식들은 일반적으로 증명 길이를 최소화하는 것과 같은 계산 가능한 최적화 목표에 의존한다. 그러나 길이 기반 메트릭은 의미 있는 리팩토링보다는 "골핑(golfing, 직접 압축)"을 선호하는 경향이 있다. 모듈성과 재사용성 같은 특성들은 신뢰할 수 있는 자동 메트릭으로 환원하기 어려우며, 이는 검증하기 쉬운 것(컴파일)과 기대되는 것(라이브러리 수준의 아티팩트) 사이에 간극을 만든다.

방법론: Proof-Refactor

저자들은 증명 리팩토링을 단일 프록시 메트릭에 대한 엔드 투 엔드 최적화가 아니라, 구조화되고 프로세스에 의해 유도되는 워크플로우로 취급하도록 설계된 에이전트 프레임워크인 Proof-Refactor를 제안한다. 이 프레임워크는 Claude Code와 lean-lsp-mcp(Lean을 위한 Model Context Protocol 서버)를 기반으로 구축되었으며, 리팩토링 작업을 네 가지 순차적인 단계로 분해한다.

핵심 구성 요소

1. lean-lsp-mcp 통합: 시스템은 컨텍스트 검사(파일 구조, 증명 상태, 진단), 선언 검색(로컬, Mathlib 및 타입 패턴), 증명 상호작용(병렬 태틱 시도, 코드 액션)을 위한 도구를 활용한다.
2. 커스텀 extract 태틱: 증명 내의 태틱 블록을 독립적인 정리(theorem)인 "스캐폴드(scaffold)"로 추출하는 특수화된 Lean 태틱이다. 이는 다음 두 가지 경우를 처리한다:
   • 목표를 닫거나(close the goal) 정의적으로 동일한 목표를 남기는 블록.
   • 남은 목표를 남기는 블서, 전방향 블록의 목표로부터 전방향 블록의 목표로 향하는 함의 정리를 생성하는 블록.
   • 사용되지 않는 변수를 자동으로 제거하여 추출된 정리가 최소화되도록 보장한다.
3. 외부 지원: 파이프라인은 외부 모델(실험에서는 특히 Gemini 3.1 Pro)을 호출하기 위해 독립된 컨텍스트 인터페이스를 채택한다. 이는 고수준의 추론(조각 선택, 일반화 가능한 인터페이스 설계)과 저수준의 Lean 상호작용(편집, 검사, 수리)을 분리한다.

4단계 파이프라인

1. 추출(Extraction): 외부 지원이 원래의 증명을 분석하여 추출할 태틱 블록을 제안한다. 에이전트는 lean_extract를 사용하여 이러한 제안을 "스캐폴드"(중간 정리)로 변환하고 이를 파일에 삽입한다.
2. 헬퍼 설계(Helper Design): 에이전트는 유사성에 따라 스캐폴드를 그룹화하고, 외부 지원과 함께 일반화 가능한 헬퍼 선언을 설계한다. 이들은 라이브러리 컨벤션에 부합하는지 확인하기 위해 설계 원칙에 따라 검토된다. 스캐폴드는 임시로 취급되며, 다른 선언이 스캐폴드에 의존하지 않는다.
3. 증명(Proving): 에이전트는 새로운 헬퍼 선언과 원래 증명의 추출된 부분에 있는 sorry 플레이스홀더를 채운다. 원래의 증명 조각들이 논리적 아이디어를 제공하는 경우가 많으며, 에이전트는 일반화된 보조 정리들을 위한 형식적 증명을 구축한다.
4. 증명 수리(Proof Repair): 에이전트는 검증된 새로운 헬퍼 선언을 호출하도록 원래의 증명을 다시 작성한다. 임시 스캐폴드와 추출 래퍼를 제거하여, 새로운 추상화에 의존하는 깨끗하고 모듈화된 증명을 완성한다.

주요 기여

• 프로세스 유도형 리팩토링: 본 논문은 단순한 길이 감소보다 중간 증명 구성 요소의 식별, 일반화 및 재사용을 우선시하는 워크플로우를 도입한다.
• 분리된 아키텍처: 고수준 리팩토링 추론(외부 모델을 통한)과 저수준 Lean 상호작용(Claude Code 에이전트를 통한)을 분리함으로써, 하나의 컨텍스트에 상충하는 작업(도구 사용 vs. 추상적 설계)이 과부하되는 것을 방지한다.
• 커스텀 툴링: extract 태틱의 구현과 lean-lsp-mcp와의 통합은 단일적 증명을 구조화된 아티팩트로 변환하는 강력한 메커니즘을 제공한다.
• 평가 프로토콜: 저자들은 길이 메트릭에만 의존하는 대신 구조, 시그니처 품질, 태틱 품질, 재사용성 및 인간 가독성을 점수화하는 루브릭 기반 평가 시스템을 제안한다.

실험 결과

프레임워크는 PutnamBench(96개 문제)와 Putnam2025(12개 문제)의 생성된 Lean 증명을 대상으로, Proof-Refactor를 강력한 베이스라인인 (Claude Code와 lean4:refactor를 포함한 lean4-skills)와 비교 평가하였다.

• 품질 개선: Proof-Refactor는 평균 품질 점수에서 상당한 이득을 달성했다: PutnamBench에서 +0.45, Putnam2025에서 +0.31.
• 세부 메트릭: 가장 큰 개선은 시그니처 품질(PutnamBench에서 +0.68)과 인간 가독성(PutbankBench에서 +0.50)에서 관찰되었다. 구조와 재사용성 또한 일관된 개선을 보였다.
• 길이 vs. 품질: 길이에 최적화된 베이스라인과 달리, Proof-Refactor는 골핑(golfing)을 우선시하지 않았다. Putnam2025에서 베이스라인에 비해 오히려 더 낮은 단어 감소율(-3.8 퍼센트 포인트)을 보였음에도 불구하고 더 높은 품질 점수를 기록했다. 이는 프레임워크가 단순히 압축하는 것이 아니라 재사용 가능한 헬퍼를 중심으로 증명을 성공적으로 재구성했음을 나타낸다.
• 사례 연구 (Putnam 1968 B6): 대표적인 사례로, 베이스라인은 원래의 증명 구조를 단순히 번역한 매우 특화된 보조 정리를 생성했다. 반면, Proof-Refactor는 수학적 핵심을 추상화하는 두 개의 일반적인 보조 정리(Rat.exists_mem_open_not_mem_compact 및 tendsto_of_mem_ball_one_div_succ)를 추출하여, 메인 증명을 훨씬 더 간결하고 라이브러리 스타일와 일치하도록 만들었다.
• 절제 연구(Ablation Study): 외부 지원을 제거했을 때 평균 개선 수치가 음수(-0.55)가 되었으며, 시그니처 품질(-0.98)과 인간 가독성(-1.17)이 크게 하락했다. 이는 고수준 설계와 도구 중심 상호작용을 분리하는 것이 성공에 결정적임을 확인시켜 준다.

의의 및 주장

본 논문은 프로세스 유도형 리팩토링이 증명 품질을 높이기 위한 메트릭 기반 최적화의 실행 가능한 대안임을 주장한다. 증명 조각을 추출하고 일반화된 선언으로 변환하는 데 집중함으로써, Proof-Refactor는 비록 원래보다 짧지 않더라도 더 읽기 쉽고, 모듈화되며, 기존 수학적 인프라와 통합된 아티팩트를 생성할 수 있다.

저자들은 이 접근 방식이 증명 검사(컴파일)의 이진 피드백과 라이브러리 수준의 수학에서 기대되는 광범위한 품질 사이의 불일치를 해결한다고 강조한다. 이들은 자신들의 작업을 증명 생성을 대체하는 것이 아니라, 생성된 증명을 성숙한 형식 라이브러리의 표준으로 격상시키기 위한 필수적인 후처리 단계로 포지셔닝한다. 저자들은 현재 범위가 단일 파일 리팩토링으로 제한되어 있으며, 아직 멀티 파일 프로젝트 재구성이나 기존 라이브러리 선언의 편집은 다루지 못한다는 한계점을 인정하고 있다.