From SLT4AI to AI4SLT: Generalization under scaling, and infrastructure Lean 4

Abstract

This talk connects two directions in modern statistical learning theory. First, I will briefly discuss SLT4AI: how generalization curves behave under suitable model capacities, e.g., norm-based capacities. Our results present generalization under scaling via deterministic equivalence, which challenges classical views of generalization, including the U-shaped bias-variance curve, double descent, and empirical scaling laws. Second, I will talk about AI4SLT by presenting our Lean 4 formalization of SLT from empirical process theory with more than 30,000 lines code under a human-AI collaborative workflow (with some design principles), including Gaussian Lipschitz concentration, Dudley's entropy integral theorem for sub-Gaussian processes, and application to localized least squares. It highlights how formal AI4SLT infrastructure can make modern learning theory reliable, reusable, and machine-checkable.

Biography

刘方辉，上海交通大学自然科学研究院与数学学院副教授，数学学院与人工智能学院博士生导师。研究方向为现代机器学习的数学理论与大模型机理分析。其主要研究工作包括函数空间视角下的机器学习理论、尺度扩展下的泛化理论，并进一步推动其在大模型微调与参数高效训练中的应用，以及机器学习理论的形式化推理系统（AI4SLT）。近五年在JMLR、SIAM、NeurIPS、ICML、ICLR、TPAMI发表论文20余篇。2019年博士毕业于上海交通大学，曾在 KU Leuven、EPFL 从事博士后研究，在英国University of Warwick担任助理教授。2023年入选国家高层次青年人才，获 AAAI 2024新教师奖，2025年入选TUM全球访问教授计划等。担任NeurIPS、ICLR、AISTATS等会议领域主席。