Lean Formalization of Generalization Error Bound by Rademacher Complexity

要約

Lean 4定理を使用して、Rademacherの複雑さを使用して、一般化エラーバウンドを正式化します。
一般化エラーは、指定されたトレーニングデータと目に見えないテストデータでの学習マシンのパフォーマンスとの間のギャップを定量化し、Rademacherの複雑さは、学習マシンの複雑さまたは仮説クラスの複雑さに基づくこのエラーの推定値として機能します。
PAC学習やVCディメンションなどの従来の方法とは異なり、Rademacherの複雑さは、ディープラーニングやカーネルメソッドなどの多様な機械学習シナリオに適用されます。
経験的および人口のレーデマーの複雑さを含む重要な概念と定理を形式化し、McDiarmidの不平等、HoeffdingのLemma、および対称化の議論の正式な証拠を通じて一般化誤差境界を確立します。

要約(オリジナル)

We formalize the generalization error bound using Rademacher complexity in the Lean 4 theorem prover. Generalization error quantifies the gap between a learning machine’s performance on given training data versus unseen test data, and Rademacher complexity serves as an estimate of this error based on the complexity of learning machines, or hypothesis class. Unlike traditional methods such as PAC learning and VC dimension, Rademacher complexity is applicable across diverse machine learning scenarios including deep learning and kernel methods. We formalize key concepts and theorems, including the empirical and population Rademacher complexities, and establish generalization error bounds through formal proofs of McDiarmid’s inequality, Hoeffding’s lemma, and symmetrization arguments.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google