Proof-Refactor: Refactoring Generated Formal Proofs into Modular Artifacts

Motivation

• Known: 생성된 formal proof는 컴파일 여부(정합성)로만 보상받기 때문에, PutnamBench나 Putnam2025 같은 벤치마크에서 컴파일에는 성공하지만 가독성, 모듈성, 재사용성이 떨어지는 증명이 많이 생성된다는 문제가 알려져 있다.
• Gap: 기존 증명 품질 개선 연구들은 length 기반의 계산 가능한 목표(proof golfing)에 의존하는데, 이는 가독성·모듈성·유지보수성·재사용성 같은 질적 속성을 측정하기 어렵고, 길이 축소만을 지향하다 의미있는 helper declaration 설계를 놓칠 수 있다는 한계가 있다.
• Why: 증명 검증(verification)이 갖는 이진적 피드백만으로는 library-quality의 formal mathematics에 요구되는 구조적 품질을 보장할 수 없으므로, post-generation refactoring은 LLM 기반 정리 증명 생성물의 실질적 활용성과 재사용성을 높이는 데 중요하다.
• Approach: 검증된 증명 (E, p)를 입력으로 받아 동일한 statement S를 유지하면서 새로운 helper declaration 집합 H를 도입한 (E′, p′)로 변환하는 constrained refactoring 문제를 정식화하고, 이를 Claude Code, lean-lsp-mcp, custom lean_extract 도구, 독립 컨텍스트 외부 모델 조력을 결합한 4단계 agentic 파이프라인으로 해결한다.

Achievement

1. Proof-Refactor 프레임워크 제안: 증명 조각 추출(Extraction), helper 설계(Helper Design), 증명(Proving), 수리(Repair)의 4단계로 리팩토링을 분해하는 process-guided agentic 파이프라인을 구축했다.
2. lean_extract 도구 개발: Mathlib의 extract_goal이 지원하지 못하는 비동치 goal 케이스까지 처리 가능한 custom Lean tactic을 만들어 증명 조각을 독립적 theorem(scaffold)으로 추출할 수 있게 했다.
3. LLM-as-a-judge 기반 정량 평가: PutnamBench, Putnam2025의 생성된 Lean 증명에 대해 rubric 기반 리팩토링 점수를 baseline(Claude Code + lean-lsp-mcp + lean4-skills) 대비 향상시켰으며, 특히 signature 품질과 human readability에서 가장 큰 개선을 보였다.

How

• 리팩토링을 (E, p) ⇝refactor (E′, p′) 형태의 constrained transformation으로 정식화하며, E′ = E ∪ H (새 helper declaration 집합)로 제한하고 quality preference Q에 대해 (E′, p′) ≻Q (E, p)를 요구
• lean-lsp-mcp를 context inspection(lean_file_outline, lean_hover_info, lean_goal, lean_diagnostic_messages), declaration search(lean_local_search, lean_leansearch, lean_loogle), proof interaction(lean_multi_attempt, lean_code_actions, lean_run_code) 세 범주로 활용
• custom extract tactic을 통해 tactic block을 독립 theorem으로 변환하는 lean_extract 도구를 lean-lsp-mcp에 통합하여 scaffold를 생성
• Phase 1(Extraction): 외부 모델이 추출 후보를 제안하고 agent가 lean_extract로 scaffold를 만들어 검증
• Phase 2(Helper Design): scaffold를 유사도로 그룹화하고, 외부 모델이 Mathlib 관련 정보와 함께 helper declaration을 설계, agent가 설계 원칙에 따라 검토
• 각 phase는 이전 세션의 context를 상속받지 않는 독립적 Claude Code 세션으로 실행되며, 이전 단계에서 생성된 Lean 파일만 다음 단계로 전달됨

Originality

• 증명 리팩토링을 length 최소화(golfing) 중심이 아니라 helper declaration 추출·일반화·재사용이라는 인간 formalization 관행을 모사한 process-guided 구조로 재정의함
• extract_goal의 한계(비동치 goal 처리 불가, 변수 정리 미흡)를 극복하는 custom lean_extract tactic을 설계함
• 각 phase가 독립적 context를 갖는 세션으로 실행되는 파이프라인 구조와, 고수준 리팩토링 추론(외부 모델)과 저수준 Lean 상호작용(Claude Code agent)을 분리하는 독립 컨텍스트 외부 조력 인터페이스를 도입함
• 리팩토링 문제를 (E, p) ⇝refactor (E′, p′) 형태의 수학적 정식화로 명확히 제시함

Limitation & Further Study

• 평가가 LLM-as-a-judge rubric 점수에 크게 의존하고 있어, 실제 사람 formalizer의 주관적 품질 평가나 장기적 유지보수성 검증이 부족함
• 실험이 PutnamBench와 Putnam2025라는 특정 도메인(경시수학)의 생성된 증명에 한정되어, 일반적인 Mathlib 기여나 산업용 formal verification 코드베이스로의 일반화 가능성이 검증되지 않음
• 4단계 파이프라인이 다수의 Claude Code 세션과 외부 모델 호출을 필요로 하여 계산 비용과 시간 비용이 상당히 클 것으로 예상되나 이에 대한 구체적 비용 분석이 부족함
• 후속 연구로 사람 평가자와의 상관관계 검증, 다양한 라이브러리·언어(Isabelle 등)로의 확장, 자동화된 재사용성 지표 개발이 필요함

Evaluation

총평: proof golfing 중심의 기존 접근과 차별화하여 helper declaration 재사용과 가독성 향상을 목표로 하는 process-guided refactoring이라는 새로운 문제 설정과 실용적 도구(lean_extract)를 제시한 흥미로운 연구이며, 향후 사람 평가와의 일치도 및 더 넓은 도메인으로의 확장 검증이 기대된다.