論文の概要: Hypothesis-Disciplined Multi-Agent Automated Formalization of Asymptotic Statistical Theory
- arxiv url: http://arxiv.org/abs/2606.20642v1
- Date: Wed, 03 Jun 2026 20:03:38 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-06-30 20:45:40.122076
- Title: Hypothesis-Disciplined Multi-Agent Automated Formalization of Asymptotic Statistical Theory
- Title（参考訳）: 仮説分割多元自動漸近統計理論の形式化
- Abstract要約: 漸近統計理論はAI支援形式化の挑戦的な領域である。
複数のエージェントから構築された仮説に分類したLean 4形式化パイプラインを提案する。
結果として得られるリーン開発は、公理的クリーンでソース忠実です。
- 参考スコア（独自算出の注目度）: 17.20738506776148
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: Asymptotic statistical theory is a challenging domain for AI-assisted formalization: its central results mix convergence statements, asymptotic expansions, functional analysis, and regularity conditions that have a large gap from existing infrastructure in Lean 4 formalization. To address these challenges, we propose a hypothesis-disciplined Lean 4 formalization pipeline built from multiple agents: a manager that coordinates seven specialist roles for proof planning, skeleton scaffolding, Mathlib reconnaissance, proof construction, integration, independent review, and audit. The main methodological discipline is the hypothesis-disciplined audit, implemented by the Auditor agent: every main-theorem hypothesis and concept-layer field must be anchored in the source mathematical prose, justified as a Lean encoding adapter, marked as source-implied, or rejected as an unsupported strengthening. Using this workflow, we build a systematic formalization of asymptotic statistical theory, especially the parametric and semi-parametric models' asymptotic distribution and efficiency results. The resulting Lean development is axiom-clean and source-faithful, with Lean-checked and human-audited proofs of core parametric and semi-parametric theorems organized so that theorem-agnostic infrastructure and statistical concept definitions are separated from theorem-specific assembly. The formalization results are available at https://github.com/junwei-lu/Lean-Asymptotic-Statistical-Theory.
- Abstract（参考訳）: 中心的な結果は、収束ステートメント、漸近的拡張、機能分析、そしてリーン4の形式化における既存のインフラストラクチャとの大きなギャップを持つ規則性条件を混ぜています。
これらの課題に対処するために、複数のエージェントから構築された仮説を分類したLean 4形式化パイプラインを提案します。
すべての主理論仮説と概念層フィールドは、元の数学的散文に固定され、Leanエンコーディングアダプタとして正当化され、ソース実装としてマークされ、あるいは控えめな強化として拒否されなければならない。
このワークフローを用いて、漸近統計理論、特にパラメトリックおよび半パラメトリックモデルの漸近分布と効率結果の体系的な形式化を構築する。
コアパラメトリックと半パラメトリックの定理が組織され、定理に依存しないインフラストラクチャと統計的概念定義が、定理固有のアセンブリから分離される。
公式化結果はhttps://github.com/junwei-lu/Lean-Asymptotic-Statistical-Theoryで公開されている。
関連論文リスト
- MathCoPilot: An Interactive System for Human-AI Symbiotic Paradigm of Mathematical Research [62.221184989046826]
MathCoPilotは、数学研究のための新しいAI共生パラダイムを具現化したループシステムである。
MathCoPilotは3つのコア機能を統合する: 証明をナビゲート可能なステップに分解するインタラクティブな証明青写真、適応的な知識ベース検索とリーン統合された反復検証を備えた自動証明スキルオーケストレーション、トピック駆動の紙検索と自動形式化を検証可能なリーン知識ベースに統合する。
論文 参考訳（メタデータ） (2026-07-16T05:22:40Z) - Why Agentic Theorem Prover Works: A Statistical Provability Theory of Mathematical Reasoning Models [8.948475969696075]
エージェント定理プロバーは、数学的推論モデルとライブラリ検索、サブゴール分解/探索プランナー、証明アシスタント検証とを結合したパイプラインである。
本稿では, 検証された証明に到達する有限水平成功確率として定義される分布的視点を提案し, 証明可能性を導入する。
本稿では,エージェント定理の証明者が実世界の偏りのある問題分布にいつ,なぜ成功するのかを,原理的かつコンポーネントに敏感に説明する。
論文 参考訳（メタデータ） (2026-02-11T05:22:24Z) - Statistical Learning Theory in Lean 4: Empirical Processes from Scratch [57.00315741159824]
本稿では,経験的プロセス理論に基づく統計学習理論(SLT)の総合的なLean 4形式化について述べる。
エンドツーエンドの正式なインフラストラクチャは、最新のLean 4 Mathlibライブラリに欠けている内容を実装しています。
この研究は再利用可能な形式基盤を確立し、機械学習理論の今後の発展への扉を開く。
論文 参考訳（メタデータ） (2026-02-02T16:24:53Z) - A Foundational Theory of Quantitative Abstraction: Adjunctions, Duality, and Logic for Probabilistic Systems [2.362412515574206]
大規模あるいは連続的な状態空間は、正確に解析しやすくし、原理化された量的抽象を要求する。
この研究は、圏論、コレージュブラ、量論理、最適輸送を統合することで、そのような抽象の統一理論を発展させる。
論文 参考訳（メタデータ） (2025-10-22T10:16:24Z) - From Axioms to Algorithms: Mechanized Proofs of the vNM Utility Theorem [0.0]
我々は、選好完全性、推移性、連続性、独立性の古典的な公理を実践する。
我々の定式化は、宝くじに対する嗜好関係の数学的構造を捉えている。
この形式化は、経済モデリング、AIアライメント、管理決定システムにおける応用のための厳格な基盤を提供する。
論文 参考訳（メタデータ） (2025-06-08T10:09:54Z) - DeepTheorem: Advancing LLM Reasoning for Theorem Proving Through Natural Language and Reinforcement Learning [67.93945726549289]
DeepTheoremは、数学的推論を強化するために自然言語を活用する包括的な非公式な定理証明フレームワークである。
DeepTheoremには、121Kの高品質なIMOレベルの非公式な定理と証明からなる大規模なベンチマークデータセットが含まれている。
我々は、証明された定理の変種を利用して堅牢な数学的推論を動機付けることによって、非公式な定理証明に適した新しい強化学習戦略(RL-Zero)を考案する。
論文 参考訳（メタデータ） (2025-05-29T17:59:39Z) - Model-free Methods for Event History Analysis and Efficient Adjustment (PhD Thesis) [55.2480439325792]
この論文は、モデルフリーの観点から統一された統計学への独立した貢献のシリーズである。
第1章では、機械学習から予測技術を活用する柔軟なメソッドを定式化するために、モデルフリーの視点をどのように利用できるか、詳しく説明している。
第2章では、あるプロセスの進化が他のプロセスに直接影響されるかどうかを記述した地域独立の概念を研究している。
論文 参考訳（メタデータ） (2025-02-11T19:24:09Z) - Alchemy: Amplifying Theorem-Proving Capability through Symbolic Mutation [71.32761934724867]
この研究は、記号的突然変異を通じて形式的な定理を構成するデータ合成のフレームワークであるAlchemyを提案する。
マドリブにおける各候補定理について、書き直しや適用に使用できるすべてのイベーシブルな定理を同定する。
その結果、マドリブの定理の数は110kから6Mへと桁違いに増加する。
論文 参考訳（メタデータ） (2024-10-21T08:04:21Z) - Measurability in the Fundamental Theorem of Statistical Learning [0.0]
統計的学習の基本定理は、仮説空間がPAC学習可能であることと、そのVC次元が有限であることは同値である。
本稿では、実数 O-極小展開上で定義された仮説空間のPAC学習可能性について十分な条件を示す。
この仮説空間のクラスは、ReLUやシグモイド関数のようなよく用いられる活性化関数を使用する二項分類のためのすべての人工ニューラルネットワークをカバーする。
論文 参考訳（メタデータ） (2024-10-14T08:03:06Z) - The Foundations of Tokenization: Statistical and Computational Concerns [51.370165245628975]
トークン化は、NLPパイプラインにおける重要なステップである。
NLPにおける標準表現法としての重要性は認識されているが、トークン化の理論的基盤はまだ完全には理解されていない。
本稿では,トークン化モデルの表現と解析のための統一的な形式的枠組みを提案することによって,この理論的ギャップに対処することに貢献している。
論文 参考訳（メタデータ） (2024-07-16T11:12:28Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。