Lean Formalization of Generalization Error Bound by Rademacher Complexity and Dudley's Entropy Integral

기술적 요약: 라데마허 복잡도와 더들리 엔트로피 적분에 의한 일반화 오차 경계의 Lean 형식화

문제 제기

이 논문에서 다루는 핵심 과제는 기계 학습의 일반화 성능에 대한 형식적 검증이다. 구체적으로 저자들은 측도론적 프레임워크를 사용하여 훈련 오차 (경험적 위험) 로부터 테스트 오차 (모집단 위험) 에 대한 이론적 추정을 도출하는 것을 목표로 한다. 고전적 접근법은 Vapnik–Chervonenkis (VC) 차원에 의존하지만, 이는 종종 데이터와 무관하며 이진 분류에 맞춰져 있다. 현대 학습 이론은 실수값 손실과 다양한 함수 클래스 (예: 딥러닝, 커널 방법) 에 적용 가능한 날카롭고 데이터 의존적인 경계를 제공하는 라데마허 복잡도 (Rademacher complexity) 를 increasingly 활용한다. 그러나 가측성 (특히 비가산 가설 클래스에 대한 상한) 과 곱측도, 집중 부등식에 대한 엄밀한 처리가 필요하기 때문에 이러한 논증을 증명 보조도구 (proof assistants) 에서 형식화하는 것은 어렵다.

방법론

저자들은 Mathlib 라이브러리의 광범위한 측도론적 확률 인프라를 활용하여 Lean 4에서 일반화 오차 경계를 형식화했다. 개발은 교과서 (예: Mohri 등, Wainwright) 에서 발견되는 표준적인 "대칭화 + 유계 차이 (symmetrization + bounded differences)" 파이프라인을 따르지만, 형식적 검증을 위한 제약 조건에 맞게 적응시켰다:

1. 측도론적 설정: 프레임워크는 확률 공간 $(\Omega, m_\Omega, \mu)$ 와 확률 변수 $X: \Omega \to \mathcal{X}$ 를 통해 데이터 생성을 모델링한다. 샘플은 함수 $\omega: \text{Fin } n \to \Omega$ 로 모델링되며, $S = X \circ \omega$ 를 얻기 위해 푸시포워드 (pushed forward) 된다.
2. 핵심 정의:
   • 라데마허 복잡도: 고정된 샘플 $S$ 에 대한 경험적 경우와 곱측도 $\mu^n$ 에 대한 기대값 경우 모두에 대해 정의된다. 경험적 버전은 모든 부호 벡터 $\sigma \in \{-1, 1\}^n$ 에 대해 평균을 낸다.
   • 균일 편차 (Uniform Deviation): 가설 클래스 $F = \{f_i\}_{i \in \iota}$ 에 대한 경험적 평균과 모집단 평균 사이의 절대 차이의 상한으로 정의된다.
3. 대칭화: 형식적 정리 (abs_symmetrization_equation) 는 두 개의 독립적인 샘플 간의 차이의 상한을 부호가 바뀐 합의 평균으로 대체하여 균일 편차를 라데마허 복잡도와 연결한다.
4. 집중 (Concentration): 저자들은 Lean 내에서 McDiarmid 부등식을 처음부터 증명한다. 균일 편차 함수가 유계 차이 속성 (하나의 샘플 점을 변경하면 값이 최대 $2b/n$ 만큼만 변함) 을 만족함을 입증하여, 고확률 꼬리 경계 (tail bounds) 를 유도할 수 있게 한다.
5. 비가산 인덱스 집합 처리: 비가산 인덱스 집합 $\iota$ 에 대한 상한의 가측성이 중요한 기술적 장애물이다. Mathlib 은 가산 인덱스에 대해서는 가측성을 제공하지만 비가산 인덱스에 대해서는 자동으로 제공하지 않는다. 저자들은 다음을 통해 이를 해결한다:
   • 먼저 가산 인덱스 집합에 대한 정리를 증명한다.
   • 가분 위상 (separable topological) 인덱스 집합으로 결과를 확장하기 위해 가산 조밀 축소 (countable dense reduction) 를 적용한다. 이는 연속 함수의 경우, 균일 지배 (uniform domination) 에 의해 보장된 적분 하에서의 연속성이 유지된다는 전제하에, 가분 공간에 대한 상한이 가산 조밀 부분집합에 대한 상한과 같음을 증명하는 과정을 포함한다.

주요 기여

이 논문은 라데마허 복잡도를 통한 일반화 분석의 첫 번째 체계적인 형식화를 제시한다. 구체적인 기여 사항은 다음과 같다:

• 재사용 가능한 형식 인프라: 경험적/기대 라데마허 복잡도, 대칭화, 유계 차이 분석, McDiarmid 부등식을 포괄하는 기계적으로 검증된 파이프라인.
• 가측성 해결: 가산 가설 클래스에서 가분 위상 매개변수 공간으로 결과를 끌어올리기 위한 재사용 가능한 메커니즘. 이는 비가산 상한을 가측으로 만들기 위해 필요한 충분 조건 (가분성, 첫 번째 가산성, 균일 지배, 적분 하에서의 연속성) 을 명시적으로 패키징하며, 이는 비형식적 증명에서 종종 암묵적으로 처리되는 단계이다.
• 형식화된 집중 도구: McDiarmid 부등식의 완전한 증명과 최대 부등식, Massart 보조정리, 덮개 수 (covering numbers) 를 위한 지원 보조정리.
• 구체적 적용 사례:
  • 선형 예측기: $\ell_2$ 정규화 예측기에 대한 표준 $O(1/\sqrt{n})$ 경계와 $\ell_1$ 정규화 예측기에 대한 $O(\sqrt{\log(d)/n})$ 경계의 형식화.
  • 더들리 엔트로피 적분: 사슬 연결 (chaining) 구성을 통해 라데마허 복잡도와 덮개 수를 연관시키는 더들리 유형의 경계에 대한 형식화. 이는 경험적 의사거리 (empirical pseudo-metrics) 를 정의하고 이산적 사슬 연결 합에서 적분 경계로의 전환을 처리하는 것을 요구했다.

결과

이 형식화는 표준 학습 이론적 경계의 기계적으로 검증된 버전을 산출한다:

1. 기대 경계: $E[\text{UD}_n(F)] \leq 2 R_n(F)$, 여기서 $R_n(F)$ 는 라데마허 복잡도이다.
2. 고확률 경계: 임의의 $\delta \in (0, 1)$ 에 대해, 확률 $1-\delta$ 이상으로:
   $$\text{UD}_n(F) \leq 2 R_n(F) + b \sqrt{\frac{2 \log(1/\delta)}{n}}$$
3. 구체적 경계: 저장소는 $\ell_2$ 및 $\ell_1$ 제약 하의 선형 예측기에 대한 경험적 라데마허 복잡도, 그리고 더들리 엔트로피 적분 경계에 대한 구체적인 증명을 제공한다.

중요성과 주장

저자들은 이 작업을 신뢰할 수 있고 인증된 기계 학습 이론을 향한 기초적인 단계로 위치시킨다.

• 이론과 검증의 연결: 이 작업은 곱측도, 포락선 (envelopes) 의 적분 가능성, 집중 등에 의존하는 현대적 측도론적 학습 이론이 지나치게 단순화된 이산적 대리 모델에 의존하지 않고 증명 보조도구에서 형식화될 수 있음을 보여준다.
• 암묵적 가정의 명확화: 주요 기여는 비가산 가설 클래스를 처리하는 데 필요한 조건의 명시적 식별이다. 형식화는 "가산 - 조밀 축소"와 표준 교과서에서 종종 간과되는 특정 연속성/적분성 가설을 분리해낸다.
• 모듈성: 개발은 추상적 라데마허 파이프라인이 재사용될 수 있도록 설계되었다. 구체적인 경계는 함수 클래스를 인스턴스화하고 특정 분석적 추정 (예: 노름 제약) 을 해결함으로써 얻어지는 "실행 가능한 귀결 (executable corollaries)"이 된다.
• 이전 작업과의 비교: 이전의 형식화가 유한 가설 클래스 (예: Bagnall & Stewart) 나 특정 알고리즘 사례 (예: 결정 스템프) 로 제한된 것과 달리, 이 작업은 실수값 손실을 가진 일반적이고 잠재적으로 비가산인 함수 클래스를 처리한다.

이 논문은 수학적 경계 자체가 고전적이지만, 형식화가 엄밀한 설정에서 그 유효성에 필요한 정확한 논리적 구조와 부수 조건을 명확히 하여, 리프시츠 수축 부등식과 가우스 복잡도와의 연결과 같은 향후 확장의 기초를 제공한다고 결론지었다.