![Lean 4での統計的学習理論の形式化 [R]](https://external-preview.redd.it/vcCPMFQJ_Ba1RGnmGbl8xPO9fb1vZ01Ht3Hg4xF7i0Q.png?width=640&crop=smart&auto=webp&s=66c23bc95d8b7a4cf205d906d8b6fed9fda955ab) | 私は、統計的学習理論の一部を形式化することに焦点を当てた Lean 4 プロジェクトを進めています： 現在の成果には以下が含まれます：
主な考え方は、単発の宣言だけでなく、ML 理論のための読みやすく教育的に構成された「定理ラダー」を構築することです。 私は次の点を維持したいと考えています：
経験過程の基盤や抽象的な確率の仕組みにより重きを置く、いくつかの既存の Lean SLT の取り組みと比べて、このプロジェクトは現状、明示的な有限サンプルの PAC/Rademacher/安定性のルートと、読みやすいエンドツーエンドの定理の連鎖により重点を置いています。 特に次についてフィードバックをいただけると嬉しいです：
ありがとうございます、 [リンク] [コメント] |
Lean 4で統計的学習理論を形式化する（R）
Reddit r/MachineLearning / 2026/5/9
💬 オピニオンDeveloper Stack & InfrastructureIdeas & Deep AnalysisModels & Research
要点
- FormalSLTはLean 4上で統計的学習理論の主要部分を形式化する取り組みであり、厳密さと読みやすさを両立した定理構築を目指している。
- 現在、有限クラスのERM境界、ラデマッハ対称化、高確率ラデマッハ境界、VC次元との関係（Sauer–Shelah）、有限スカラー縮約、線形予測子の境界、有限PAC-Bayes境界、アルゴリズム的安定性など、多数の代表的な学習理論の結果が形式化されている。
- 方針としては「定理ラダー（theorem ladder）」を作ることで、前提の明示、定理のスコープ管理、そしてLeanの未完成証明（`sorry`）を使わないことを重視している。
- 他のLean SLTの取り組みが抽象的な確率や経験過程の基盤により強く焦点を当てるのに対し、本プロジェクトは有限サンプルのPAC/Rademacher/安定性ルートと、標準的なSLTの流れに沿った読みやすい一連の定理鎖を優先している。
- 著者は、定理の整理、証明構造、命名・API設計、次に形式化すべき有用なターゲットについてのフィードバックを求めている。
![[MTP Drafter] LLM高速化技術の裏側 〜隠されざる下書きコストの天秤〜](/_next/image?url=https%3A%2F%2Fassets.st-note.com%2Fproduction%2Fuploads%2Fimages%2F275956375%2Frectangle_large_type_2_1777831d30d90144bac0162637953c16.png%3Fwidth%3D219%26dpr%3D2%26frame%3D1%26format%3Djpg&w=3840&q=75)
