기술 요약: ImProver 2

문제 제기

형식 수학 라이브러리 (예: Lean 의 Mathlib) 의 급속한 확장은 이중적인 도전을 야기했습니다. 이러한 라이브러리의 유지보수성은 이질적인 증명 스타일과 낮은 모듈성으로 인해 위협받고 있으며, 신경 정리 증명기를 위한 훈련 데이터의 품질은 정확하지만 구조적으로 비최적인 증명들로 인해 저하됩니다. 기존 자동 증명 최적화 방법은 이질적이고 휴리스틱하게 정의된 목적 함수, 고품질 최적화 데이터의 부족, 그리고 대규모 모델의 훈련 및 추론에 따른 prohibitive 비용 등 상당한 장애물에 직면해 있습니다. 또한, 이전 연구들은 종종 범용 폐쇄 소스 모델에 의존하거나 토큰 수에만 집중하여 모듈성 및 종속성 관리와 같은 더 넓은 구조적 지표를 다루지 못했습니다.

방법론

저자들은 Lean 4 에서 증명 최적화를 위해 작은 언어 모델 (SLM) 을 반복적으로 자기 개선하도록 설계된 신경 심볼릭 프레임워크인 ImProver 2를 소개합니다. 이 시스템은 다중 구성 요소 파이프라인을 통해 작동합니다.

1. 신경 심볼릭 증강 (발판)

비형식적 추론과 형식적 검증 사이의 간극을 메우기 위해, 이 프레임워크는 모델이 Lean 환경의 풍부한 맥락에 노출되도록 합니다. 이 "발판"($\Psi$) 은 다음을 포함합니다:

• 맥락 슬라이스: 대상 증명에서 직접 참조되는 관련 정의, 정리, 보조 정리들을 메타데이터와 함께 직렬화한 것.
• 상태 체인 (CoS): 각 전술 단계 전후의 목표 상태에 대한 명시적 추적들을 주석으로 교차 배치하여 증명의 논리적 흐름을 드러내는 것.
• 자동 비형식화: 형식 증명을 고수준 설명의 시퀀스로 변환하여 생성된 증명 단계에 대한 자연어 요약.

2. 최적화 지표

이 시스템은 계산 가능한 함수 $\mu$로 정의된 세 가지 고유한 구조적 목적을 목표로 합니다:

• 길이: 사용된 전술의 수를 최소화하는 것 (증명 "골핑").
• 종속성: 증명에서 명시적으로 언급된 고유한 외부 보조 정리의 수를 최소화하여 자기 완결적인 증명을 장려하는 것.
• 모듈성: have, calc 등을 통해 도입된 독립적인 하부 증명인 "유효하게 생성된 목표 (effective spawned goals)"의 수를 최대화하는 것. 이는 증명 분해 및 유지보수성을 위한 대리 지표 역할을 합니다.

3. 반복적 선호도 최적화 (IRPO) 파이프라인

ImProver 2 는 SLM 을 부트스트랩하기 위해 반복적 훈련 루프를 사용합니다:

1. 생성: 현재 모델 $G_t$가 신경 심볼릭 발판을 활용하여 훈련 세트의 각 정리에 대해 $n$개의 후보 재작성을 생성합니다.
2. 필터링 및 재생: 후보들은 정확성 (Lean 커널 검증) 과 지표 개선도에 따라 점수가 매겨집니다. 재생 버퍼를 사용하여 새로 생성된 데이터와 역사적 데이터를 균형 있게 조정하여 모델 붕괴를 방지하고 점진적인 개선을 보장합니다. 사소하거나 품질이 낮은 문제는 필터링됩니다.
3. 선호도 쌍 구성: 데이터셋은 "승자" (컴파일되고 개선도가 높은 증명) 와 "패자" (실패 또는 개선도가 낮은 증명) 로 분할됩니다. 두 가지 유형의 선호도 쌍이 형성됩니다: 개선 크기에 따라 순서가 매겨진 승자 - 승자 쌍과 승자 - 패자 쌍.
4. 훈련: 모델은 승자 증명에 대한 직접 선호도 최적화 (DPO) 손실과 음의 로그 가능도 (NLL) 손실을 결합한 **반복적 추론 선호도 최적화 (IRPO)**를 사용하여 업데이트됩니다. 이 과정은 수렴하거나 예산이 소진될 때까지 반복됩니다.

주요 기여

1. 리팩토링을 위한 자기 개선 SLM: 이 논문은 반복적 선호도 최적화가 특수 연구 라이브러리에서 증명을 최적화하도록 작은 언어 모델 (특히 7B 파라미터 모델) 을 효과적으로 부트스트랩할 수 있음을 보여줍니다. 이를 통해 모델은 훨씬 더 큰 모델들과 경쟁할 수 있게 됩니다.
2. 구조적 최적화 지표: 단순한 길이 감축을 넘어, 저자들은 모듈성과 종속성 지표를 도입하고 평가합니다. 이러한 지표는 라이브러리 유지보수와 관련된 고유한 리팩토링 목표를 타겟팅하기 위해 증명 구조와 라이브러리 맥락을 활용합니다.
3. 신경 심볼릭 증강: 이 프레임워크는 목표 상태 추적, 관련 맥락, 자동 비형식화를 추출하고 통합합니다. 저자들은 이러한 증강이 작고 최첨단 모델 모두의 성능을 크게 향상시켜 유효하고 고가치인 재작성의 발견을 용이하게 함을 보여줍니다.

실험 결과

이 시스템은 7B 파라미터 베이스 모델 (DeepSeek-R1-Distill-Qwen-7B) 을 사용하여 인간이 작성한 연구 수준의 수학 벤치마크인 miniCTX-v2에서 평가되었습니다.

• 규모 대비 성능: 발판을 사용하지 않은 경우, ImProver 2 는 세 가지 지표 (길이, 모듈성, 종속성) 모두에서 훨씬 더 큰 DeepSeek-R1 671B 모델을 능가합니다. 예를 들어, 모듈성에서 ImProver 2 는 평균 0.143의 개선을 달성한 반면, 671B 모델은 0.055의 개선만 보였습니다.
• 최첨단 모델과의 비교: 7B ImProver 2 모델은 길이 및 종속성 지표에서 중급 최첨단 모델 (예: GPT-5-mini) 과 경쟁력을 보입니다. 또한 발판을 사용하지 않은 모든 평가된 시스템 중 모듈성에서 가장 높은 성과를 거두었습니다.
• 발판의 영향: 신경 심볼릭 발판을 추가하면 모든 모델 계열에서 성능이 크게 향상됩니다. 예를 들어, 7B 모델의 길이 개선 점수는 베이스 모델의 0.118에서 발판을 적용한 경우 0.236으로 상승했습니다. GPT-5-high 와 같은 대형 모델조차도 발판을 통해 0.660 에서 0.875 로 상당한 개선을 보였습니다.
• 반복 동역학: 대부분의 성능 향상은 처음 2~3 번의 IRPO 반복 내에서 발생합니다. 이 시스템은 작은 모델들이 연구 수준의 증명 구조를 효과적으로 재구성하는 법을 학습할 수 있음을 보여주지만, 모델이 일반적인 리팩토링 패턴을 흡수함에 따라 성능은 결국 정체됩니다.
• 정확도 트레이드오프: 논문은 최적화와 컴파일 정확도 사이의 트레이드오프를 지적합니다. 최적화된 증명은 종종 더 높은 지표 개선을 제공하지만, 보수적인 재작성보다 약간 낮은 컴파일률을 보일 수 있으며, 이는 구조적 변환의 위험성을 반영합니다.

중요성과 주장

이 논문은 증명 최적화가 단순히 모델 규모에 의존하는 것이 아니라 작업 특화적 전문성과 반복적 자기 개선에 의해 크게 주도된다고 주장합니다. 재생 버퍼가 적용된 선호도 최적화 파이프라인과 신경 심볼릭 발판을 결합함으로써, ImProver 2 는 작고 접근 가능한 모델들이 복잡하고 연구 수준의 증명 구조를 효과적으로 재구성할 수 있음을 입증합니다.

저자들은 그들의 작업이 증명 최적화를 확장 가능하고 학습 가능한 작업으로 확립한다고 주장합니다. 그들은 그들의 접근 방식이 형식 라이브러리 유지보수와 미래 증명기를 위한 훈련 데이터 품질 향상에 대한 중요한 필요성을 해결하며, 거대하고 비싼 최첨단 모델에만 의존하지 않고 증명 리팩토링을 자동화하는 길을 제시한다고 말합니다. 이 작업은 적절한 발판과 훈련을 통해 작은 모델들이 특정 구조적 목표에서 훨씬 더 큰 시스템의 성능을 맞먹거나 능가할 수 있음을 강조합니다.