Proof-Refactor: 생성된 형식 증명을 모듈형 산출물로 리팩터링하기

대규모 언어 모델 (LLMs)이 형식 증명 (formal proofs) 생성에서 강력한 성능을 보여주었지만, 그 출력물은 성숙한 형식 수학 라이브러리의 증명들에 비해 가독성, 모듈성, 유지보수성 및 재사용성이 떨어지는 경우가 많습니다. 우리는 이러한 격차가 대부분의 증명 생성 파이프라인에 내재된 '컴파일 우선 (compile-first)' 목표에서 부분적으로 기인한다고 주장하며, 이는 라이브러리 품질의 산출물보다는 단일 구조(monolithic) 또는 임시방편적 (ad hoc)인 증명 스크립트를 장려합니다. 기존의 증명 품질 개선 방식은 종종 명시적이고 계산 가능한 최적화 목표에 의존합니다. 그러나 실제로 가장 다루기 쉽고 실험적으로 검증된 목표는 주로 길이에 기반한 것이며, 가독성, 모듈성, 유지보수성 및 재사용성과 같은 고차원적인 품질은 신뢰할 수 있는 자동 지표로 환원하기 어렵습니다. 우리는 단일 대리 지표 (proxy metric)를 대상으로 증명 개선을 최적화하는 대신, 인간의 증명 리팩터링 (proof-refactoring) 워크플로에서 영감을 얻은 프로세스 가이드 접근 방식 (process-guided approach)을 취합니다. 우리는 증명 리팩터링을 네 가지 단계, 즉 후보 증명 파편 추출, 헬퍼 선언 (helper declarations) 설계, 추출 및 설계된 구성 요소의 형식적 증명, 그리고 검증된 구성 요소를 사용한 원래 증명의 수리로 분해하는 에이전트 기반 프레임워크 $\textbf{Proof-Refactor}$를 제안합니다. PutnamBench 및 Putnam2025에서 생성된 Lean 증명에 대해, Proof-Refactor는 강력한 Claude Code 리팩터링 베이스라인 대비 루브릭 기반 리팩터링 점수를 향상시켰으며, 특히 시그니처 품질 (signature quality)과 인간 가독성에서 가장 큰 이득을 보였습니다. 이러한 결과는 프로세스 가이드 리팩터링이 증명 길이를 주요 목표로 다루지 않고도 증명 구조를 개선할 수 있음을 시사합니다.