Lean Formalization of Generalization Error Bound by Rademacher Complexity

• URL: http://arxiv.org/abs/2503.19605v3
• Date: Mon, 15 Sep 2025 09:48:25 GMT
• Title: Lean Formalization of Generalization Error Bound by Rademacher Complexity
• Authors: Sho Sonoda, Kazumi Kasaura, Yuma Mizuno, Kei Tsukamoto, Naoto Onda,
• Abstract summary: We formalize the generalization error bound using the Rademacher complexity for the Lean 4 theorem prover based on the probability theory in the Mathlib 4 library.<n>We also present the formalization of generalization error bound for $L2$-regularization models.
• Score: 5.114451899552168
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: We formalize the generalization error bound using the Rademacher complexity for the Lean 4 theorem prover based on the probability theory in the Mathlib 4 library. Generalization error quantifies the gap between a learning machine's performance on given training data versus unseen test data, and the Rademacher complexity is a powerful tool to upper-bound the generalization error of a variety of modern learning problems. Previous studies have only formalized extremely simple cases such as bounds by parameter counts and analyses for very simple models (decision stumps). Formalizing the Rademacher complexity bound, also known as the uniform law of large numbers, requires substantial development and is achieved for the first time in this study. In the course of development, we formalize the Rademacher complexity and its unique arguments such as symmetrization, and clarify the topological assumptions on hypothesis classes under which the bound holds. As an application, we also present the formalization of generalization error bound for $L^2$-regularization models.

Related papers

• Do we really need the Rademacher complexities? [3.683202928838613]
  We study the fundamental problem of learning with respect to the squared loss in a convex class.<n>We prove that, contrary to prevailing belief and under minimal assumptions, the sample complexity is not governed by the Rademacher complexities.
  arXiv  Detail & Related papers  (2025-02-21T00:40:22Z)
• MathGAP: Out-of-Distribution Evaluation on Problems with Arbitrarily Complex Proofs [80.96119560172224]
  MathGAP generates problem statements and chain-of-thought reasoning traces according to specifications about their arithmetic proof structure.<n>Using MathGAP, we find that LLMs show a significant decrease in performance as proofs get deeper and wider.
  arXiv  Detail & Related papers  (2024-10-17T12:48:14Z)
• Revisiting Optimism and Model Complexity in the Wake of Overparameterized Machine Learning [6.278498348219108]
  We revisit model complexity from first principles, by first reinterpreting and then extending the classical statistical concept of (effective) degrees of freedom. We demonstrate the utility of our proposed complexity measures through a mix of conceptual arguments, theory, and experiments.
  arXiv  Detail & Related papers  (2024-10-02T06:09:57Z)
• Class-wise Generalization Error: an Information-Theoretic Analysis [22.877440350595222]
  We study the class-generalization error, which quantifies the generalization performance of each individual class. We empirically validate our proposed bounds in different neural networks and show that they accurately capture the complex class-generalization error behavior.
  arXiv  Detail & Related papers  (2024-01-05T17:05:14Z)
• Generalization Guarantees via Algorithm-dependent Rademacher Complexity [33.408679482592426]
  We propose a measure to control generalization error, which is the empirical Rademacher complexity of an algorithm- and data-dependent hypothesis class. We obtain novel bounds based on the finite fractal dimension, which (a) extend previous fractal-type bounds from continuous to finite hypothesis classes, and (b) avoid a mutual information term.
  arXiv  Detail & Related papers  (2023-07-04T18:37:38Z)
• The No Free Lunch Theorem, Kolmogorov Complexity, and the Role of Inductive Biases in Machine Learning [80.1018596899899]
  We argue that neural network models share this same preference, formalized using Kolmogorov complexity. Our experiments show that pre-trained and even randomly language models prefer to generate low-complexity sequences. These observations justify the trend in deep learning of unifying seemingly disparate problems with an increasingly small set of machine learning models.
  arXiv  Detail & Related papers  (2023-04-11T17:22:22Z)
• Generalization Analysis for Contrastive Representation Learning [80.89690821916653]
  Existing generalization error bounds depend linearly on the number $k$ of negative examples. We establish novel generalization bounds for contrastive learning which do not depend on $k$, up to logarithmic terms.
  arXiv  Detail & Related papers  (2023-02-24T01:03:56Z)
• Amortized Inference for Causal Structure Learning [72.84105256353801]
  Learning causal structure poses a search problem that typically involves evaluating structures using a score or independence test. We train a variational inference model to predict the causal structure from observational/interventional data. Our models exhibit robust generalization capabilities under substantial distribution shift.
  arXiv  Detail & Related papers  (2022-05-25T17:37:08Z)
• Partial Counterfactual Identification from Observational and Experimental Data [83.798237968683]
  We develop effective Monte Carlo algorithms to approximate the optimal bounds from an arbitrary combination of observational and experimental data. Our algorithms are validated extensively on synthetic and real-world datasets.
  arXiv  Detail & Related papers  (2021-10-12T02:21:30Z)
• Information-Theoretic Generalization Bounds for Iterative Semi-Supervised Learning [81.1071978288003]
  In particular, we seek to understand the behaviour of the em generalization error of iterative SSL algorithms using information-theoretic principles. Our theoretical results suggest that when the class conditional variances are not too large, the upper bound on the generalization error decreases monotonically with the number of iterations, but quickly saturates.
  arXiv  Detail & Related papers  (2021-10-03T05:38:49Z)
• High-dimensional separability for one- and few-shot learning [58.8599521537]
  This work is driven by a practical question, corrections of Artificial Intelligence (AI) errors. Special external devices, correctors, are developed. They should provide quick and non-iterative system fix without modification of a legacy AI system. New multi-correctors of AI systems are presented and illustrated with examples of predicting errors and learning new classes of objects by a deep convolutional neural network.
  arXiv  Detail & Related papers  (2021-06-28T14:58:14Z)
• Parsimonious Inference [0.0]
  Parsimonious inference is an information-theoretic formulation of inference over arbitrary architectures. Our approaches combine efficient encodings with prudent sampling strategies to construct predictive ensembles without cross-validation.
  arXiv  Detail & Related papers  (2021-03-03T04:13:14Z)
• Good Classifiers are Abundant in the Interpolating Regime [64.72044662855612]
  We develop a methodology to compute precisely the full distribution of test errors among interpolating classifiers. We find that test errors tend to concentrate around a small typical value $varepsilon*$, which deviates substantially from the test error of worst-case interpolating model. Our results show that the usual style of analysis in statistical learning theory may not be fine-grained enough to capture the good generalization performance observed in practice.
  arXiv  Detail & Related papers  (2020-06-22T21:12:31Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.