AI4SLT: Empirical Processes in Lean 4 for Formal Statistical Learning Theory
We present the first comprehensive Lean 4 formalization of statistical learning theory (SLT) grounded in empirical process theory. Our en-to-end formal infrastructure implement the missing contents in latest Lean library, including a complete development of Gaussian Lipschitz concentration, 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 provided in https://github.com/YuanheZ/lean-stat-learning-theory.
Code (0)
등록된 구현이 없습니다.
Tasks
Gaussian ProcessesSimilar Papers 제목 키워드 기반
Hypothesis-Disciplined Multi-Agent Automated Formalization of Asymptotic Statistical Theory
Asymptotic statistical theory is a challenging domain for AI-assisted formalization: its central results mix convergence statements, asymptotic expansions, functional analysis, and regularity conditions that have a large…
LeanCat: A Benchmark Suite for Formal Category Theory in Lean (Part I: 1-Categories)
While large language models (LLMs) have demonstrated impressive capabilities in formal theorem proving, current benchmarks fail to adequately measure library-grounded abstraction -- the ability to reason with high-level …
A Simple Generative Model of Logical Reasoning and Statistical Learning
Statistical learning and logical reasoning are two major fields of AI expected to be unified for human-like machine intelligence. Most existing work considers how to combine existing logical and statistical systems. Howe…
Bayesian InferenceFormal LogicLogical ReasoningModel-agnostic information transfer and fusion for classification with label noise
Label noise presents a fundamental challenge in modern machine learning, especially when large-scale datasets are generated via automated processes. An increasingly common and important data paradigm, particularly in dom…
Transfer LearningProcess-Verified Reinforcement Learning for Theorem Proving via Lean
While reinforcement learning from verifiable rewards (RLVR) typically has relied on a single binary verification signal, symbolic proof assistants in formal reasoning offer rich, fine-grained structured feedback. This ga…
Reinforcement Learning