AI4SLT: Empirical Processes in Lean 4 for Formal Statistical Learning Theory

Motivation

• Known: Empirical process theory는 학습 알고리즘의 excess risk를 concentration inequality와 capacity control(metric entropy, Dudley's entropy integral 등)을 통해 통제하는 통합된 uniform convergence framework를 제공하며, 이는 double descent, benign overfitting 등 현대 딥러닝 이론 분석의 기초가 되어왔다.
• Gap: Lean 4를 비롯한 interactive theorem prover에서 SLT의 핵심 도구인 concentration inequality, covering number, chaining 등은 아직 구조화된 machine-readable 라이브러리로 존재하지 않으며, 기존 연구(Sonoda et al., 2025)는 Rademacher complexity 기반의 매우 제한적인 setting만 다루어 localized empirical process에 기반한 sharp rate 분석은 formalize된 바 없다.
• Why: 이론이 점점 복잡해지면서(딥러닝, LLM 등) 현대 SLT 증명은 길고 정교해져 인간 검증이 어려워지고 있으며, formal verification은 machine-checkable한 정확성 보장과 재사용 가능한 구조화된 라이브러리를 동시에 제공함으로써 확장 가능한 이론 분석의 기반이 될 수 있다.
• Approach: 인간이 증명 전략을 설계하고 Claude Code(Opus-4.5) AI agent가 tactical proof construction을 수행하는 human-AI collaborative workflow를 통해, Mathlib의 부족한 인프라를 처음부터 체계적으로 구축하여 SLT의 전체 스택을 formalize한다.

Achievement

Figure 2. The dependency graph of our formalizations. All the contents in the graph have not been implemented in Lean 4

1. Gaussian Lipschitz Concentration의 완전한 formalization: Efron-Stein inequality, Gaussian Poincaré inequality, density argument, Gaussian logarithmic Sobolev inequality(LSI)를 아우르는 인프라를 구축하여 임의의 theorem prover에서 최초로 완전한 Gaussian analysis toolset을 완성함.
2. Dudley's Entropy Integral Theorem의 formalization: sub-Gaussian process에 대한 Dudley's entropy integral theorem을 Lean 4에서 최초로 formalize하였으며, dyadic 근사에 대한 telescoping sum으로 분해하는 chaining technique과 covering/packing number의 엄밀한 처리를 포함함.
3. Least-Squares Framework 응용: localized empirical process에 기반한 least-squares regression의 통합 framework를 개발하고, linear regression 및 ℓ1-constrained regression에 적용하여 minimax-level의 sharp rate를 도출함.
4. Human-AI Collaborative Formalization Paradigm 제시: 약 500시간의 supervised development를 통해 sorry나 axiom 없이 약 30,000줄의 Lean 4 코드를 완성하여, 대규모 formalization 프로젝트가 인간-AI 협업으로 가속화될 수 있음을 보임.

How

Figure 2. The dependency graph of our formalizations. All the contents in the graph have not been implemented in Lean 4

• Mathlib의 기존 인프라를 분석하고 인간 수학자가 증명 전략을 설계, 복잡한 정리를 관리 가능한 lemma로 분해
• AI agent(Claude Code with Opus-4.5)가 해당 계획을 실행하여 tactical proof construction 수행
• Efron-Stein inequality → Gaussian Poincaré inequality → density argument → Gaussian LSI 순으로 Gaussian Lipschitz concentration을 단계적으로 구축
• dyadic approximation에 대한 telescoping sum 분해를 통한 chaining argument로 Dudley's entropy integral theorem 구현
• localized function class F(δ), Gaussian/Rademacher complexity, metric entropy log N(F(δ), ϵ, d) 등의 개념을 형식적으로 정의하고 critical radius δ⋆를 도출하는 프레임워크 구축
• linear regression과 ℓ1-constrained regression에 프레임워크를 적용해 실용성 검증

Originality

• SLT를 empirical process theory 관점에서 Lean 4로 formalize한 최초의 포괄적 시도로, 기존 연구가 다루지 못한 concentration과 capacity control의 상호작용을 모두 포함
• Gaussian Lipschitz concentration과 Dudley's entropy integral theorem을 최초로 theorem prover에서 완전히 formalize
• 단순 이론 formalization을 넘어 least-squares (sparse) regression에 대한 sharp rate 응용까지 end-to-end로 구현
• 인간이 전략을 설계하고 AI가 tactic을 실행하는 human-AI collaborative formalization paradigm을 대규모(30,000줄, 500시간)로 실증

Limitation & Further Study

• 현재 formalization은 least-squares (sparse) regression과 같은 비교적 제한된 응용에 국한되어 있어, 딥러닝이나 대형 언어모델과 같은 복잡한 architecture의 이론(double descent, benign overfitting 등)으로의 확장이 필요함
• human-AI collaboration 과정에서 human의 supervision 비중과 AI agent의 실제 기여도에 대한 정량적 분석(예: 실패율, 반복 횟수)이 부족하여 재현성 및 일반화 가능성 평가가 제한적임
• 30,000줄 규모의 코드가 학습 자료로서 학생들에게 유용하다고 주장하지만, 실제 교육적 효과에 대한 실증적 평가는 제시되지 않음
• 향후 연구로 비모수적 모델, 심층 신경망 이론, 또는 다른 복잡도 측도(VC dimension 등)로의 확장이 기대됨

Evaluation

총평: SLT의 핵심 이론적 인프라를 Lean 4로 완전하게 formalize한 선구적이고 야심찬 작업으로, human-AI collaboration을 통한 대규모 formalization의 실용적 사례를 제시한다는 점에서 이론 및 formal methods 커뮤니티 모두에 의미 있는 기여를 한다.