기술적 요약: 에이전트형 정리 증명기가 작동하는 이유

문제 제기

최근 검색, 탐색, 증명 보조 도구 검증기를 대규모 언어 모델 (LLM) 과 결합한 에이전트형 정리 증명기들은 검증된 수학적 증명을 생성하는 데 경험적 성공을 거두었습니다. 그러나 기존 이론적 프레임워크는 이러한 성공을 설명하는 데 어려움을 겪고 있습니다. 고전적 증명 이론은 증명의 '존재성'을 다루는 반면, 복잡성 이론은 '최악의 경우' 난이도를 다룹니다. 둘 다 실제에서 마주치는 특정 편향된 정리 분포 (예: 라이브러리 정리, 벤치마크 계열) 에 대해 고정된 연산 예산 내에서 특정 알고리즘이 높은 확률로 성공하는 이유를 적절히 설명하지 못합니다.

본 논문은 다음과 같은 질문에 답합니다: 특정 에이전트 증명기가 지정된 정리 인스턴스 스트림에서 고정된 예산 내에서 검증자가 수용하는 증명을 생성할 확률은 얼마인가? 저자들은 이러한 '통계적 증명 가능성 (statistical provability)'을 이해하는 것이 검증 피드백, 분해와 같은 구성 요소들이 고전적 결정 불가능성이나 최악의 경우 하한과 모순되지 않으면서 성능을 향상시키는 이유를 설명하는 데 필수적이라고 주장합니다.

방법론

1. 도달 가능성 MDP 로의 형식화

저자들은 형식적 증명 탐색을 결정론적 동역학을 가진 **유한 시간 범위 도달 가능성 마르코프 의사결정 과정 (MDP)**으로 모델링합니다:

• 상태 ($X$): 현재 증명 의무 (예: Lean 의 열린 목표 목록) 와 검증기 피드백.
• 행동 ($A$): 전술, 추론 규칙, 또는 검색 명령과 같은 증명기 이동.
• 전이 ($F$): 결정론적 검증기 업데이트 맵 $F: X \times A \to X$. 유효하지 않은 행동은 실패 상태로 매핑되고, 유효한 행동은 새로운 증명 상태로 전이됩니다.
• 목표 ($G$): 해결된 상태의 집합 (빈 목표 목록).

이 형식화는 검증기의 운영 의미론을 전이 커널로 취급합니다. 저자들은 신뢰할 수 있는 상태 추상화 하에서 최적 MDP 성공 확률이 동일한 예산 내의 일반적 구문적 증명 가능성과 정확히 일치함을 증명하여, 통계적 분석을 가능하게 하면서도 논리적 무결성을 유지합니다.

2. 통계적 증명 가능성 정의

핵심 지표는 **통계적 증명 가능성 ($SP^\pi_B(q_0)$)**으로, 초기 정리 분포 $q_0$와 증명기의 내부 무작위성을 평균낸 $B$번의 검증기 호출 내에서 검증된 증명에 도달할 증명기 정책 $\pi$의 확률로 정의됩니다. 이는 최적 성공 확률 $SP^*_B(q_0)$와 대비됩니다.

저자들은 또한 **평균 절단된 증명 길이 ($Len^\pi_B(q_0)$)**를 추적합니다. 이는 성공 또는 예산 소진 전의 검증기 호출 수의 기댓값으로 정의됩니다. 이 지표는 그들의 경계에서 중요한 해석 가능성 핸들 역할을 합니다.

3. 학습 파이프라인 분석

본 논문은 현재 실무와 정렬된 파이프라인을 분석합니다:

1. 오프라인 행동 - 가치 회귀: 훈련 분포에서 검증기 기반 롤아웃 (시뮬레이션된 증명) 을 통해 깊이별 행동 - 가치 함수 ($Q^*_t$) 학습.
2. 탐욕적 테스트 시간 증명: 학습된 점수를 사용하여 테스트 시간에 최선의 행동을 탐욕적으로 선택.

분석은 가정 3.1에 의존하며, 이는 다음을 가정합니다:

• 훈련과 테스트가 발생하는 컴팩트한 집중 집합 ($C_t$).
• 최적 가치 함수와 가설 클래스의 리프시츠 연속성.
• 탐색 분포에 의한 상태 - 행동 공간의 충분한 커버리지.
• 노이즈를 줄이기 위해 쿼리당 여러 개의 독립적인 롤아웃 레이블 사용 가능.

주요 기여 및 결과

1. 주요 정리 (통계적 증명 가능성 경계)

중심 결과 (정리 3.1) 는 학습된 증명기의 성공 확률과 최적 증명기의 성공 확률 사이의 차이를 경계 짓습니다. 이 경계는 균일 행동 - 가치 오차의 점유 가중 합입니다:

$$SP^*_B(q_0) - SP^{\hat{\pi}}_B(q_0) \leq 2 \sum_{s=1}^B P^{\hat{\pi}}_{q_0}(T_G \geq s) \cdot \epsilon_{B-s+1}$$

여기서:

• $P^{\hat{\pi}}_{q_0}(T_G \geq s)$는 학습된 증명기가 $s$단계에서 문제를 아직 해결하지 못했을 확률 (미해결 질량 곡선) 입니다.
• $\epsilon_t$는 깊이 $t$에서 학습된 행동 - 가치 추정기에 대한 균일 오차 경계입니다.

오차 항 ($\epsilon_t$) 의 해석:
오차는 세 가지 구성 요소로 분해됩니다:

1. 근사 오차: 가설 클래스가 실제 가치 함수를 표현하지 못하는 능력.
2. 커버리지/기하학적 오차: 훈련 분포의 유효 국소 차원 ($d_t$) 과 커버리지 상수 ($c_t$) 에 의존.
3. 롤아웃 노이즈: 회귀에 사용된 유한한 수의 몬테카를로 레이블 ($m_t$) 로 인한 분산.

2. 평균 증명 길이의 역할

핵심 통찰은 경계에서 주도적인 복잡성 승수가 **학습된 증명기의 평균 절단된 증명 길이 ($Len^{\hat{\pi}}_B(q_0)$)**라는 점입니다.
$$SP^*_B(q_0) - SP^{\hat{\pi}}_B(q_0) \lesssim \bar{\epsilon}_B \cdot Len^{\hat{\pi}}_B(q_0)$$
이는 증명 길이를 단축시키는 메커니즘 (예: 효과적인 분해, 보조 정리 도입) 이 국소 가치 추정 오차 ($\bar{\epsilon}_B$) 가 일정하게 유지되더라도 종단 간 손실을 직접적으로 감소시킨다는 것을 의미합니다.

3. 마진 조건과 빠른 수렴 속도

마진 조건 하에서 (최고와 차고 행동 가치 간의 간격이 높은 확률로 충분히 큰 경우), 경계는 빠른 속도로 개선됩니다:
$$SP^*_B(q_0) - SP^{\hat{\pi}}_B(q_0) \lesssim Len^{\hat{\pi}}_B(q_0) \cdot \bar{\epsilon}_B^{\beta+1}$$
이는 행동 간격 (정확한 이동이 잘못된 이동보다 명확히 우월하게 만드는 것) 을 개선하면 수렴이 크게 가속화된다는 것을 시사합니다.

4. 스케일링 법칙

본 논문은 샘플 복잡성 휴리스틱을 유도합니다. 로그 인자를 무시하면 오차는 $n^{-1/(d+2)}$로 스케일링되며, 여기서 $n$은 검증기 레이블 예산이고 $d$는 유효 국소 차원입니다. 이는 '테스트 시간 스케일링' 이득이 다음과 같은 요인에서 발생할 수 있음을 명확히 합니다:

• 유효 시간 범위 단축 (더 짧은 증명).
• 유효 기하학적 차원 감소 (더 나은 검색/표현).
• 행동 간격 마진 증가.

중요성 및 주장

본 논문은 편향된 작업 부하에서 에이전트형 정리 증명기가 작동하는 이유에 대한 구성 요소 민감한 설명을 제공한다고 주장합니다. 이는 다음과 같이 고전적 논리와 통계적 학습 사이의 간극을 메웁니다:

1. 검증기 피드백: 근사 오차를 줄이고, 커버리지를 개선하며, 행동 간격을 증가시킴으로써 증명 가능성을 향상시킵니다.
2. 검색 및 표현: 가치 함수를 매끄럽게 하고, 상태 공간을 저차원 영역에 집중시키며, 나쁜 선택을 가지치기하여 마진을 증가시킴으로써 도움을 줍니다.
3. 증명 단축: 분해와 같은 메커니즘은 경계에서 오차의 주요 승수인 '점유 가중치 (평균 증명 길이)'를 감소시킵니다.

저자들은 이 이론이 최악의 경우 난이도와 모순되지 않는다고 강조합니다. 대신, 증명 길이가 짧고 간격이 크며 커버리지가 좋은 실제에서 발견되는 특정 구조화된 정리 분포 (라이브러리 정리, 벤치마크) 에서 에이전트 시스템이 성공하는 이유를 설명합니다. 이 프레임워크는 검증기를 정보 채널로, 증명기를 제한된 예산 하에서 유용한 정보를 추출하는 통계적 학습자로 취급하여, 현대 에이전트 시스템에서 널리 사용되는 공학적 선택 (검색, 분해, 검증기 루프) 에 대한 엄밀한 정당성을 제공합니다.