論文の概要: Statistical Learning Theory in Lean 4: Empirical Processes from Scratch

• arxiv url: http://arxiv.org/abs/2602.02285v1
• Date: Mon, 02 Feb 2026 16:24:53 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-02-03 19:28:34.288201
• Title: Statistical Learning Theory in Lean 4: Empirical Processes from Scratch
• Title（参考訳）: リーン4の統計的学習理論:スクラッチからの経験的プロセス
• Authors: Yuanhe Zhang, Jason D. Lee, Fanghui Liu,
• Abstract要約: 本稿では,経験的プロセス理論に基づく統計学習理論(SLT)の総合的なLean 4形式化について述べる。 エンドツーエンドの正式なインフラストラクチャは、最新のLean 4 Mathlibライブラリに欠けている内容を実装しています。 この研究は再利用可能な形式基盤を確立し、機械学習理論の今後の発展への扉を開く。
• 参考スコア（独自算出の注目度）: 57.00315741159824
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: We present the first comprehensive Lean 4 formalization of statistical learning theory (SLT) grounded in empirical process theory. Our end-to-end formal infrastructure implement the missing contents in latest Lean 4 Mathlib library, including a complete development of Gaussian Lipschitz concentration, the first formalization of 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 available at https://github.com/YuanheZ/lean-stat-learning-theory
• Abstract（参考訳）: 本稿では,経験的プロセス理論に基づく統計学習理論(SLT)の総合的なLean 4形式化について述べる。 私たちのエンドツーエンドのフォーマルインフラストラクチャは、最新のLean 4 Mathlibライブラリに欠けている内容を実装しています。その中には、ガウスリプシッツ濃度の完全な開発、サブガウス過程に対するダドリーのエントロピー積分定理の最初の形式化、そして、急速で最小二乗(スパース)回帰への応用が含まれます。 このプロジェクトは、人間が実証戦略を設計し、AIエージェントが戦術実証構築を実行するという、人間とAIの協調ワークフローを使用して実施された。 実装の他に、形式化プロセスは標準のSLT教科書で暗黙の仮定と詳細を公開し、解決し、理論の粒度の細かい直線的理解を強制する。 この研究は再利用可能な形式基盤を確立し、機械学習理論の今後の発展への扉を開く。 コードはhttps://github.com/YuanheZ/lean-stat-learning-theoryで公開されている。

関連論文リスト

• Towards Formalizing Reinforcement Learning Theory [21.93657660333281]
  マルコフサンプルを用いて,Q$学習と線形時間差(TD)学習のほぼ確実な収束を定式化する。 この研究は、収束RL結果を完全形式化するための重要なステップとなる。
  論文  参考訳（メタデータ） (2025-11-05T16:35:47Z)
• LOGOS: LLM-driven End-to-End Grounded Theory Development and Schema Induction for Qualitative Research [9.819685510441902]
  グラウンドド理論は質的なデータから深い洞察を提供するが、専門家が集中する手動コーディングに依存しているため、大きなスケーラビリティのボトルネックが生じる。 基礎理論ワークフローを完全に自動化する新しいエンドツーエンドフレームワークであるLOGOSを紹介する。 LOGOSはLLM駆動のコーディング、セマンティッククラスタリング、グラフ推論、そして再利用可能なコードブックを構築するための新しい反復的洗練プロセスを統合している。
  論文  参考訳（メタデータ） (2025-09-29T05:16:09Z)
• FormalML: A Benchmark for Evaluating Formal Subgoal Completion in Machine Learning Theory [44.64175433092553]
  大規模言語モデル (LLM) は、最近、形式定理の証明において顕著な進歩を見せている。 しかし、数学者の実践的なアシスタントとして機能する能力は、複雑な証明の中で欠落したステップを埋めるものであり、まだ解明されていない。 機械学習の基礎理論に基づいて構築された、リーン4ベンチマークであるFormalMLを紹介します。
  論文  参考訳（メタデータ） (2025-09-26T14:40:14Z)
• Emergent Cognitive Convergence via Implementation: A Structured Loop Reflecting Four Theories of Mind [0.0]
  我々は、心の4つの影響力のある理論の間に構造的な収束を報告する。 収束は、エージェントフローと呼ばれる実用的なAIアーキテクチャの中で意図せずに現れる。 本稿では,知的アーキテクチャが,実践的制約によって形成される共有構造パターンへと進化する可能性を示唆する。
  論文  参考訳（メタデータ） (2025-07-22T02:54:45Z)
• Alchemy: Amplifying Theorem-Proving Capability through Symbolic Mutation [71.32761934724867]
  この研究は、記号的突然変異を通じて形式的な定理を構成するデータ合成のフレームワークであるAlchemyを提案する。 マドリブにおける各候補定理について、書き直しや適用に使用できるすべてのイベーシブルな定理を同定する。 その結果、マドリブの定理の数は110kから6Mへと桁違いに増加する。
  論文  参考訳（メタデータ） (2024-10-21T08:04:21Z)
• LeanDojo: Theorem Proving with Retrieval-Augmented Language Models [72.54339382005732]
  大規模言語モデル(LLM)は、Leanのような証明アシスタントを使って形式的な定理を証明することを約束している。 既存のメソッドは、プライベートコード、データ、計算要求のために、複製や構築が難しい。 本稿では、ツールキット、データ、モデルからなるオープンソースのリーンツールキットであるLeanDojoを紹介します。 本研究では,LLM ベースの証明器 ReProver を開発した。
  論文  参考訳（メタデータ） (2023-06-27T17:05:32Z)
• Variance Reduced ProxSkip: Algorithm, Theory and Application to Federated Learning [0.0]
  本研究では,Em Local Training(LT)パラダイムに基づく分散最適化手法について検討する。 提案手法は,最先端の手法であるProxSkipよりも,総合的なトレーニングコストの面ではるかに高速であることを示す。
  論文  参考訳（メタデータ） (2022-07-09T20:59:30Z)
• Linear Temporal Logic Modulo Theories over Finite Traces (Extended Version) [72.38188258853155]
  有限トレース(LTLf)上の線形時間論理について検討する。 命題の文字は任意の理論で解釈された一階述語式に置き換えられる。 Satisfiability Modulo Theories (LTLfMT) と呼ばれる結果の論理は半決定可能である。
  論文  参考訳（メタデータ） (2022-04-28T17:57:33Z)
• On Computation and Generalization of Generative Adversarial Imitation Learning [134.17122587138897]
  GAIL(Generative Adversarial Learning)は、シーケンシャルな意思決定ポリシーを学習するための強力で実践的なアプローチである。 本稿ではGAILの理論的性質について考察する。
  論文  参考訳（メタデータ） (2020-01-09T00:40:19Z)

関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。

指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。