量化有限理性：通过柔性随机占优对西蒙满意准则的形式化验证
数理金融
2025-07-10 v1 计算工程、金融与科学
摘要
本文引入了柔性一阶随机占优（FFSD），这是一个数学上严谨的框架，使用 Lean 4 定理证明器形式化了赫伯特·西蒙的有限理性概念。我们开发了机器验证的证明，表明 FFSD 通过参数化的容忍阈值，在经典期望效用理论与西蒙的满意行为之间架起了桥梁。我们的方法产生了几个关键结果：（1）一个临界阈值 ，保证了参考点的唯一性；（2）一个等价定理，将 FFSD 与近似指示函数的期望效用最大化联系起来；（3）扩展到多维决策设定。通过将这些概念编码在 Lean 4 的依赖类型理论中，我们提供了第一个机器检查的西蒙有限理性形式化，为在认知限制下对不确定性下的经济决策进行机械化推理奠定了基础。这项工作为形式数学与经济理论之间日益增长的交集做出了贡献，展示了交互式定理证明如何能够增进我们对传统上仅以定性方式表达的行为经济学概念的理解。
引用
@article{arxiv.2507.07052,
title = {Quantifying Bounded Rationality: Formal Verification of Simon's Satisficing Through Flexible Stochastic Dominance},
author = {Jingyuan Li and Zhou Lin},
journal= {arXiv preprint arXiv:2507.07052},
year = {2025}
}