論文の概要: 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アライメント、管理決定システムにおける応用のための厳密な基盤を提供し、理論決定理論と計算実装のギャップを埋める。

関連論文リスト

• Formal Power Series Representations in Probability and Expected Utility Theory [0.24578723416255752]
  我々は、正統主義の教義に具現化された制限を放棄するコヒーレントな選好の理論を前進させる。 デ・フィネッティの理論とは異なり、我々が提唱した理論は推移性もアルキメデス性も境界性も好みの連続性も必要としない。 実用性による表現可能性(Representability by utility)は、H"older's Theorem"を拡張し、Hhn's Embedding Theoremを強化したこの論文の中心的な結果のまとめである。
  論文  参考訳（メタデータ） (2025-08-01T03:34:39Z)
• LeanConjecturer: Automatic Generation of Mathematical Conjectures for Theorem Proving [6.220998637943786]
  LeanConjecturerは、Large Language Models(LLMs)を使用して、Lean 4で大学レベルの数学予想を自動的に生成するパイプラインである。 反復生成と評価により、LeanConjecturerは40のMathlibシードファイルから12,289の予想を生成し、3,776は構文的に有効で非自明であると同定された。
  論文  参考訳（メタデータ） (2025-06-27T08:17:18Z)
• 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)
• Alchemy: Amplifying Theorem-Proving Capability through Symbolic Mutation [71.32761934724867]
  この研究は、記号的突然変異を通じて形式的な定理を構成するデータ合成のフレームワークであるAlchemyを提案する。 マドリブにおける各候補定理について、書き直しや適用に使用できるすべてのイベーシブルな定理を同定する。 その結果、マドリブの定理の数は110kから6Mへと桁違いに増加する。
  論文  参考訳（メタデータ） (2024-10-21T08:04:21Z)
• The Foundations of Tokenization: Statistical and Computational Concerns [51.370165245628975]
  トークン化は、NLPパイプラインにおける重要なステップである。 NLPにおける標準表現法としての重要性は認識されているが、トークン化の理論的基盤はまだ完全には理解されていない。 本稿では,トークン化モデルの表現と解析のための統一的な形式的枠組みを提案することによって,この理論的ギャップに対処することに貢献している。
  論文  参考訳（メタデータ） (2024-07-16T11:12:28Z)
• Prototype-based Aleatoric Uncertainty Quantification for Cross-modal Retrieval [139.21955930418815]
  クロスモーダル検索手法は、共通表現空間を共同学習することにより、視覚と言語モダリティの類似性関係を構築する。 しかし、この予測は、低品質なデータ、例えば、腐敗した画像、速いペースの動画、詳細でないテキストによって引き起こされるアレタリック不確実性のために、しばしば信頼性が低い。 本稿では, 原型に基づくAleatoric Uncertainity Quantification (PAU) フレームワークを提案する。
  論文  参考訳（メタデータ） (2023-09-29T09:41:19Z)
• Making Linear MDPs Practical via Contrastive Representation Learning [101.75885788118131]
  マルコフ決定過程(MDP)における次元性の呪いに、低ランク表現を利用することで対処することが一般的である。 本稿では,効率的な表現学習を可能にしつつ,正規化を自動的に保証する線形MDPの代替的定義について考察する。 いくつかのベンチマークにおいて、既存の最先端モデルベースおよびモデルフリーアルゴリズムよりも優れた性能を示す。
  論文  参考訳（メタデータ） (2022-07-14T18:18:02Z)
• 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)

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

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