린 4에서의 통계적 학습 이론: 처음부터 시작하는 경험적 과정

초록

우리는 경험적 과정 이론에 기반한 통계적 학습 이론(SLT)의 최초의 포괄적인 Lean 4 형식화를 제시한다. 우리의 종단간 형식 인프라는 가우시안 립시츠 농도에 대한 완전한 전개, 부분 가우시안 과정을 위한 더들리 엔트로피 적분 정리의 최초 형식화, 그리고 날카로운 수렴 속도를 갖는 최소제곱(희소) 회귀 분석에의 응용을 포함하여 최신 Lean 4 Mathlib 라이브러리의 누락된 내용을 구현한다. 이 프로젝트는 인간이 증명 전략을 설계하고 AI 에이전트가 전술적 증명 구성을 실행하는 인간-AI 협업 워크플로우를 통해 수행되었으며, 이를 통해 인간이 검증한 SLT용 Lean 4 도구 상자를 구축하였다. 구현을 넘어, 이 형식화 과정은 표준 SLT 교과서에 내재된 암묵적 가정과 누락된 세부 사항을 드러내고 해결함으로써 이론에 대한 세밀한, 줄 단위의 이해를 강제한다. 이 작업은 재사용 가능한 형식 기초를 마련하고 향후 기계 학습 이론 발전의 문을 연다. 코드는 https://github.com/YuanheZ/lean-stat-learning-theory 에서 확인할 수 있다.

English

We present the first comprehensive Lean 4 formalization of statistical learning theory (SLT) grounded in empirical process theory. Our end-to-end formal infrastructure implement the missing contents in latest Lean 4 Mathlib library, including a complete development of Gaussian Lipschitz concentration, the first formalization of Dudley's entropy integral theorem for sub-Gaussian processes, and an application to least-squares (sparse) regression with a sharp rate. The project was carried out using a human-AI collaborative workflow, in which humans design proof strategies and AI agents execute tactical proof construction, leading to the human-verified Lean 4 toolbox for SLT. Beyond implementation, the formalization process exposes and resolves implicit assumptions and missing details in standard SLT textbooks, enforcing a granular, line-by-line understanding of the theory. This work establishes a reusable formal foundation and opens the door for future developments in machine learning theory. The code is available at https://github.com/YuanheZ/lean-stat-learning-theory

린 4에서의 통계적 학습 이론: 처음부터 시작하는 경험적 과정

Statistical Learning Theory in Lean 4: Empirical Processes from Scratch

초록

Support