用计算机验证了经典效用理论的数学基础，确保决策模型绝对可靠。
From Axioms to Algorithms: Mechanized Proofs of the vNM Utility Theorem
- 用Lean 4形式化验证了冯诺依曼-摩根斯坦效用公理
- 证明了满足公理的偏好可唯一表示为期望效用最大化
- 适合研究可信决策系统与人工智能对齐的学者
本文使用Lean 4交互式定理证明器，全面形式化了冯诺依曼-摩根斯坦（vNM）期望效用定理。我们实现了偏好完备性、传递性、连续性和独立性等经典公理，实现了机器可验证的效用表示存在性与唯一性证明。形式化捕捉了彩票上偏好关系的数学结构，验证了满足vNM公理的偏好可由期望效用最大化表示。贡献包括对独立性公理的细粒度实现、混合彩票基本命题的正式证明、效用存在的构造性演示，以及验证结果的计算实验。证明与经典表述等价，同时在决策边界处提供更高精度。该形式化为经济建模、人工智能对齐和管理决策系统提供了严谨基础，弥合了理论决策论与计算实现之间的鸿沟。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。