論文の概要: From Axioms to Algorithms: Mechanized Proofs of the vNM Utility Theorem

• arxiv url: http://arxiv.org/abs/2506.07066v1
• Date: Sun, 08 Jun 2025 10:09:54 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-06-10 16:33:10.658809
• Title: From Axioms to Algorithms: Mechanized Proofs of the vNM Utility Theorem
• Title（参考訳）: 公理からアルゴリズムへ:vNMユーティリティ理論の機械的証明
• Authors: Li Jingyuan,
• Abstract要約: 我々は、選好完全性、推移性、連続性、独立性の古典的な公理を実践する。 我々の定式化は、宝くじに対する嗜好関係の数学的構造を捉えている。 この形式化は、経済モデリング、AIアライメント、管理決定システムにおける応用のための厳格な基盤を提供する。
• 参考スコア（独自算出の注目度）: 0.0
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: This paper presents a comprehensive formalization of the von Neumann-Morgenstern (vNM) expected utility theorem using the Lean 4 interactive theorem prover. We implement the classical axioms of preference-completeness, transitivity, continuity, and independence-enabling machine-verified proofs of both the existence and uniqueness of utility representations. Our formalization captures the mathematical structure of preference relations over lotteries, verifying that preferences satisfying the vNM axioms can be represented by expected utility maximization. Our contributions include a granular implementation of the independence axiom, formally verified proofs of fundamental claims about mixture lotteries, constructive demonstrations of utility existence, and computational experiments validating the results. We prove equivalence to classical presentations while offering greater precision at decision boundaries. This formalization provides a rigorous foundation for applications in economic modeling, AI alignment, and management decision systems, bridging the gap between theoretical decision theory and computational implementation.
• Abstract（参考訳）: 本稿では、Lean 4インタラクティブ定理証明器を用いて、von Neumann-Morgenstern(vNM)予測ユーティリティ定理の包括的形式化を提案する。 便宜表現の存在と一意性の両方を示す古典的公理として、選好完全性、推移性、連続性、独立性の証明を実装した。 我々の定式化は、抽選よりも優先関係の数学的構造を捉え、vNM公理を満たす選好が期待された効用最大化によって表現できることを検証する。 我々の貢献には、独立公理のきめ細かい実装、混合宝くじに関する基本的な主張の証明の形式的証明、実用性の存在に関する建設的実証、結果を検証する計算実験が含まれる。 我々は、決定境界においてより精度の高い提示を行いながら、古典的な提示と等価性を証明した。 この形式化は、経済モデリング、AIアライメント、管理決定システムにおける応用のための厳密な基盤を提供し、理論決定理論と計算実装のギャップを埋める。

関連論文リスト

• 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)
• Theory: Multidimensional Space of Events [0.0]
  本稿では,事象と仮説集合の間の相互影響を考慮に入れた多次元事象空間(MDSE)理論を開発する。 MDSEは、予測精度を15～20%改善した関係変数をうまくモデル化した。 このアプローチは、リスクアセスメント、リソース最適化、予測問題など、エンジニアリング上の課題における実践的な応用を提供する。
  論文  参考訳（メタデータ） (2025-05-16T08:54:12Z)
• Function-coherent gambles [0.0]
  本稿では,非線形効用に対応する一般化である関数コヒーレントギャンブルを提案する。 連続線型汎函数を通した許容ギャンブルを特徴づける表現定理を証明する。 関数コヒーレントフレームワークに定レート指数割引の代替手段を組み込むことを実証する。
  論文  参考訳（メタデータ） (2025-02-22T14:44:54Z)
• The Foundations of Tokenization: Statistical and Computational Concerns [51.370165245628975]
  トークン化は、NLPパイプラインにおける重要なステップである。 NLPにおける標準表現法としての重要性は認識されているが、トークン化の理論的基盤はまだ完全には理解されていない。 本稿では,トークン化モデルの表現と解析のための統一的な形式的枠組みを提案することによって,この理論的ギャップに対処することに貢献している。
  論文  参考訳（メタデータ） (2024-07-16T11:12:28Z)
• The vacuum provides quantum advantage to otherwise simulatable architectures [49.1574468325115]
  理想のゴッテマン・キタエフ・プレスキル安定化状態からなる計算モデルを考える。 測定結果の確率密度関数を計算するアルゴリズムを提案する。
  論文  参考訳（メタデータ） (2022-05-19T18:03:17Z)
• A Topological Perspective on Causal Inference [10.965065178451104]
  仮定のない因果推論は、構造因果モデルの単なる集合においてのみ可能であることを示す。 以上の結果から,有効な因果推論を行うのに十分な帰納的仮定は,原理上は統計的に検証できないことが示唆された。 我々のトポロジカルアプローチのさらなる利点は、無限に多くの変数を持つSCMに容易に対応できることである。
  論文  参考訳（メタデータ） (2021-07-18T23:09:03Z)

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

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