Exponential Sample Complexity Separation between Flat and Hierarchical Agentic Theorem Provers

제목: 평면적 및 계층적 에이전트 정리 증명기 간의 지수적 샘플 복잡도 분리

저자: 소노다 쇼, 아키야마 켄타, 우에자토 유야
소속: 사이버에이전트, RIKEN AIP
날짜: 2026 년 5 월 7 일

1. 문제 제기

최근 에이전트 기반 정리 증명기들은 전술 수준 탐색에 착수하기 전에 중간 보조정리 생성, 증명 스케치 작성, 또는 하위 목표 분해와 같은 분해 전략을 종종 활용합니다. 고전적 증명 이론은 보조정리가 유도 과정을 단축할 수 있음을 시사하지만, 이러한 중간 단계를 발견하고 증명하는 데 드는 통계적 학습 비용은 여전히 열린 질문으로 남아 있습니다. 구체적으로, 보조정리를 증명하는 것 자체가 어렵다면, 학습된 증명기가 왜 그 노력에 에너지를 써야 할까요?

본 논문은 재사용 가능한 증명 구조 (계층적) 를 학습하는 것이 완전히 인라인된 증명 궤적 (평면적) 에서 학습하는 것에 비해 고정된 탐색 예산 내에서 검증된 증명을 찾을 확률을 높이는지에 대한 통계적 학습 문제를 다룹니다. 저자들은 모든 수식에 대한 최악의 경우 증명 복잡도가 아닌, '교사'증명기에 의해 유도된 데이터 분포, 즉 초기 정리 상태와 성공적인 검증된 증명 궤적으로 구성된 분포에 초점을 맞춥니다.

2. 방법론

저자들은 정리를 증명하는 과정을 결정론적 유한 시간 마르코프 의사결정 과정 (MDP) 으로 모델링하며, 여기서 상태는 증명 상태이고 행동은 전술, 추론 규칙, 또는 고수준 분해 동작입니다. 그들은 성공적인 교사 궤적에 대한 오프라인 모방 학습을 세 가지 다른 설정 하에서 분석합니다:

• 설정 1 (평면적): 교사는 완전히 인라인된 저수준 증명 궤적을 생성합니다. 학생은 그래프 예측이나 메모이제이션 없이 이러한 궤적을 모방합니다. 반복되는 하위 증명들은 훈련 및 테스트 데이터에서 서로 다른 복사된 발생으로 나타납니다.
• 설정 2 (계층적): 교사는 노드가 재사용 가능한 증명 블록을 나타내는 고수준 증명 방향 비순환 그래프 (DAG) 를 구성합니다. 학생은 고수준 그래프 행동 (블록 선택, 확장, 재사용) 과 저수준 지역 해결을 위한 그래프 예측기 및 정책을 학습합니다. 훈련 데이터는 인라인된 궤적으로 구성되며, 학생은 잠재적 증명 DAG 구조를 추론해야 합니다.
• 설정 3 (비교): 평면적 학생과 계층적 학생 모두 계층적 교사가 생성한 동일한 소스 데이터 (인라인된 궤적) 로 훈련됩니다. 평면적 학생은 잠재적 그래프 구조를 폐기하는 반면, 계층적 학생은 이를 추론합니다. 이 설정은 표현 방식이 샘플 복잡도에 미치는 영향을 분리합니다.

분석은 세 가지 주요 양에 의존합니다:

1. $L$ (평균 길이): 성공적인 증명에서의 평균 결정 수.
2. $\eta$ (고유 탐색 손실): 교사의 다음 행동이 학생의 상위-$k$ 후보 목록에 포함되지 않아 손실된 확률 질량 (지역 예측 가능성).
3. $e$ (모방 오차): 학생의 정책과 교사의 정책 간의 쿨백 - 라이블러 (KL) 발산.

저자들은 모방 오차를 상위-$k$ 누락 확률로 변환하기 위해 Tsybakov 유형의 마진 조건을 가정하며, 교사의 행동이 학생의 상위-$k$ 목록에 포함될 경우 탐색이 완전하다고 가정합니다.

3. 주요 기여

• 형식화: 본 논문은 검증기 유도 정리 증명을 유한 시간 MDP 로 형식화하고, 초기 상태 분포 내에서 예산 내에서 검증된 증명을 찾을 평균 확률로 '통계적 증명 가능성'을 정의합니다.
• 성공 보장: 저자들은 인라인된 궤적으로 훈련된 평면적 학생과 재사용 가능한 DAG 예측을 위해 훈련된 계층적 학생 모두에 대한 유한 샘플 성공 상한을 유도합니다. 이 상한은 결정 수, 고유 상위-$k$ 손실, 그리고 학습된 순위 오차를 명시적으로 분리합니다.
• 지수적 분리: 주요 이론적 결과는 충분한 샘플 복잡도에서의 지수적 분리입니다. 재사용 가능한 증명 DAG 가 트리로 평면화될 때, 동일한 하위 증명은 지수적으로 많은 번 중복됩니다. 본 논문은 동일한 데이터 소스로 훈련되더라도 계층적 학습자의 충분한 샘플 인증서가 평면적 학습자의 것보다 지수적으로 작을 수 있음을 증명합니다.
• 잠재 그래프 학습: 본 논문은 EM 스타일 사후 가중 접근 방식을 사용하여 인라인된 궤적에서 잠재적 증명 DAG 를 추론해야 하는 계층적 학생에 대한 학습 속도를 제공합니다. 이는 그래프 예측 오차와 사후 불일치를 고려합니다.

4. 결과

핵심 결과는 정리 6에 제시되어 있으며, 목표 실패 수준 $\delta$를 달성하기 위해 평면적 및 계층적 학생에게 필요한 인증된 충분 샘플 수 ($\bar{N}$) 를 비교합니다.

• 평면적 상한: $\bar{N}_{flat}(\delta) \propto (L_{flat}/\delta)^{1/(p\gamma)}$
• 계층적 상한: $\bar{N}_{hier}(\delta) \propto \max(L_{hi}, L_{lo}/\delta)^{1/(p\gamma)}$

여기서 $L_{flat}$은 펼쳐진 궤적의 길이이고 $L_{hier} = L_{hi} + L_{lo}$는 계층적 표현의 길이입니다.

본 논문은 크기/깊이 매개변수 $D$로 인덱싱된 정리 계열에 대해, 평면화 과정이 증명 길이를 지수적으로 증가시킬 경우 ($L_{flat}/L_{hier} = \exp(\Omega(D))$), 필요한 샘플의 비율 또한 지수적으로 증가함을 보여줍니다:
$$\bar{N}_{flat}(\delta) / \bar{N}_{hier}(\delta) \geq \exp(\Omega(D))$$

이 분리는 평면적 학습자가 모든 발생마다 동일한 어려운 지역 논증을 독립적으로 학습해야 하는 반면, 계층적 학습자는 공유된 블록을 한 번 학습하고 재사용하기 때문에 발생합니다. 본 논문은 중간 보조정리를 제거 (평면화) 함으로써 증명 크기가 지수적으로 폭발할 수 있음을 보여주는 절제 제거 예시 (부록 G) 를 사용하여 이를 설명합니다. 이로 인해 평면적 학습자의 샘플 복잡도가 급증합니다.

5. 중요성 및 주장

본 논문은 최악의 경우 증명 복잡도 논증과 구별되는, 계층적 증명이 도움이 되는 이유를 설명하는 구체적인 통계적 메커니즘을 제공한다고 주장합니다. 그 중요성은 분해의 이점이 단순히 논리적 유도를 단축하는 것이 아니라 학습자의 통계적 부담을 줄이는 데 있음을 규명하는 데 있습니다.

• 데이터 분포 인식: 이 결과는 학습 효율성이 데이터 분포의 구조에 의존함을 강조합니다. 성공적인 증명들이 중간 논증을 재사용한다면, 계층적 표현은 이러한 공유를 포착하지만 평면적 표현은 이를 파괴하여 중복 학습 과제를 초래합니다.
• 한계: 저자들은 자신의 주장에 대해 겸손합니다. 이는 최악의 경우 하한이 아니며, 명시적 계층 없이도 동일한 하위 문제를 완벽하게 인식할 수 있는 완벽한 정규화를 달성할 수 있는 평면적 학습자를 배제하지는 않는다고 명시합니다. 이 분리는 평면화가 재사용 가능한 증명 구조를 파괴하고 데이터 분포에 그러한 공유가 광범위하게 포함된 증명이 존재할 때 특히 유효합니다.
• 실용적 함의: 이 발견은 검증기 기반 정리 증명을 위해 재사용 가능한 증명 구조 (보조정리, 하위 목표) 를 예측하는 것을 학습하는 것이, 그래프 예측기가 높은 확률로 교사의 인증서를 커버할 수 있다면 주어진 성공 확률을 달성하는 데 필요한 샘플 복잡도를 지수적으로 줄일 수 있음을 시사합니다.

본 논문은 보조정리를 증명하는 '비싼 우회로'가 그 보조정리들이 재사용 가능할 때 통계적으로 정당화됨을 결론지으며, 한 번 학습하는 비용은 평면적 프레임워크에서 반복적으로 재발견하는 비용보다 훨씬 낮다고 주장합니다.