拍卖的预算不平衡标准：一个形式化定理

是 否 +2 论坛币

k人 参与回答

经管之家送您一份

应届毕业生专属福利!

求职就业群

赵安豆老师微信：zhaoandou666

经管之家联合CDA

送您一个全额奖学金名额~ !

立即领取

感谢您参与论坛问题回答

经管之家送您两个论坛币！

+2 论坛币

英文标题：
《Budget Imbalance Criteria for Auctions: A Formalized Theorem》
---
作者：
Marco B. Caminati, Manfred Kerber, Colin Rowat
---
最新提交年份：
2014
---
英文摘要：
  We present an original theorem in auction theory: it specifies general conditions under which the sum of the payments of all bidders is necessarily not identically zero, and more generally not constant. Moreover, it explicitly supplies a construction for a finite minimal set of possible bids on which such a sum is not constant. In particular, this theorem applies to the important case of a second-price Vickrey auction, where it reduces to a basic result of which a novel proof is given. To enhance the confidence in this new theorem, it has been formalized in Isabelle/HOL: the main results and definitions of the formal proof are re- produced here in common mathematical language, and are accompanied by an informal discussion about the underlying ideas.
---
中文摘要：
我们在拍卖理论中提出了一个原始定理：它规定了一般条件，在此条件下，所有投标人的付款总额不一定为零，更一般地说，也不是常数。此外，它显式地提供了一个有限最小可能出价集的构造，在这个集合上，这样的总和不是常数。特别地，这个定理适用于第二价格Vickrey拍卖的重要情况，在这种情况下，它归结为一个基本结果，并给出了一个新的证明。为了增强对这个新定理的信心，它在Isabelle/HOL中被形式化：这里用通用数学语言重新生成了形式证明的主要结果和定义，并伴随着关于基本思想的非正式讨论。
---
分类信息：

一级分类：Quantitative Finance        数量金融学
二级分类：Mathematical Finance        数学金融学
分类描述：Mathematical and analytical methods of finance, including stochastic, probabilistic and functional analysis, algebraic, geometric and other methods
金融的数学和分析方法，包括随机、概率和泛函分析、代数、几何和其他方法
--
一级分类：Computer Science        计算机科学
二级分类：Computer Science and Game Theory        计算机科学与博弈论
分类描述：Covers all theoretical and applied aspects at the intersection of computer science and game theory, including work in mechanism design, learning in games (which may overlap with Learning), foundations of agent modeling in games (which may overlap with Multiagent systems), coordination, specification and formal methods for non-cooperative computational environments. The area also deals with applications of game theory to areas such as electronic commerce.
涵盖计算机科学和博弈论交叉的所有理论和应用方面，包括机制设计的工作，游戏中的学习（可能与学习重叠），游戏中的agent建模的基础（可能与多agent系统重叠），非合作计算环境的协调、规范和形式化方法。该领域还涉及博弈论在电子商务等领域的应用。
--
一级分类：Computer Science        计算机科学
二级分类：Logic in Computer Science        计算机科学中的逻辑
分类描述：Covers all aspects of logic in computer science, including finite model theory, logics of programs, modal logic, and program verification. Programming language semantics should have Programming Languages as the primary subject area. Roughly includes material in ACM Subject Classes D.2.4, F.3.1, F.4.0, F.4.1, and F.4.2; some material in F.4.3 (formal languages) may also be appropriate here, although Computational Complexity is typically the more appropriate subject area.
涵盖计算机科学中逻辑的所有方面，包括有限模型理论，程序逻辑，模态逻辑和程序验证。程序设计语言语义学应该把程序设计语言作为主要的学科领域。大致包括ACM学科类D.2.4、F.3.1、F.4.0、F.4.1和F.4.2中的材料；F.4.3（形式语言）中的一些材料在这里也可能是合适的，尽管计算复杂性通常是更合适的主题领域。
--
一级分类：Quantitative Finance        数量金融学
二级分类：Economics        经济学
分类描述：q-fin.EC is an alias for econ.GN. Economics, including micro and macro economics, international economics, theory of the firm, labor economics, and other economic topics outside finance
q-fin.ec是econ.gn的别名。经济学，包括微观和宏观经济学、国际经济学、企业理论、劳动经济学和其他金融以外的经济专题
--

---
PDF下载：
--> Budget_Imbalance_Criteria_for_Auctions:_A_Formalized_Theorem.pdf (139.56 KB)

2022-5-7 04:56:44 上传

扫码加我 拉你入群

请注明：姓名-公司-职位

以便审核进群资格，未注明则拒绝

分享0 收藏0 回帖

关键词：不平衡 形式化 Mathematical Quantitative Construction

拍卖的预算不平衡标准：非规范化定理*Marco B.Caminati、Manfred Kerber和Colin Rowat英国伯明翰大学计算机科学学院英国伯明翰大学经济学英国伯明翰大学项目主页：http://cs.bham.ac.uk/research/projects/formare/Abstract.我们在拍卖理论中提出了一个原始定理：它规定了一般条件，在此条件下，所有投标人的付款总额不一定为零，更一般地说，也不一定为常数。此外，它明确地提供了一个有限的最小可能投标集的构造，在该投标集上，此类SUM不是恒定的。特别地，这个定理适用于第二价格Vickrey拍卖的重要情况，在这种情况下，它归结为一个基本结果，并给出了一个新的证明。为了增强对这一新定理的信心，它已在Sabelle/HOL中正式化：这里用通用数学语言再现了正式证明的主要结果和定义，并伴随着对基本思想的非正式讨论。1简介ForMaRE项目[4]采用形式化方法，为运行拍卖的可执行代码的生成和相关定理的提供提供统一的方法。在本文中，我们将描述关于Vickrey第二次价格拍卖（将在第2节中介绍）的一个分类结果的形式化，说明所有参与者的付款总额不能为零。我们将该结果表示为NB（无平衡）。据我们所知，我们为NB提供的机制是新的。虽然它也适用于Vickrey拍卖的具体案例，但我们的证据适用于一系列可能的拍卖机制：事实上，它给出了它所持有的拍卖类型的特征。

相比之下，我们所知道的所有现有证明都严重依赖于该机制在Vickrey拍卖的特定情况下假设的特定代数形式。此外，我们的证明明确地构造了一个最小的、有限的可能出价集，其中所有付款的总和不是常数函数。所有结果都已在Isabelle/HOL定理证明器[7]中进行了形式化和检查。因为这些结果是新的，所以在这里用通用的数学语言来描述，这对读者来说应该更友好。本文中的引理、定义和定理尽可能符合它们的可能性*这项工作得到了EPSRC基金EP/J007498/1和LMS计算机科学小额基金的支持。形式化的副本，对于each语句，我们用打字机字体表示相应的Isabelle名称。

相关的伊莎贝尔理论文件是马斯金3。你的，可在https://github.com/formare/auctions/.1.1论文结构在第2节中，给出了一些背景：我们将看到拍卖的基本数学定义，这将是陈述主要定理NB所需的，NB是目前形式化的目标。第3节非正式地说明了NB原始证明背后的想法，第4节给出了实现这个想法的正式结果，即引理1。这个引理是这里提出的整个形式化工作的基石：所有其他结果都依赖于它。第5节对这一事实进行了说明，其中非正式地解释了Howlema 1可适用于Vickrey拍卖的特殊情况。第6节对这个非正式的解释进行了形式化和系统化的解释，其中给出了辅助引理和定义，以便从引理1正式推导出主要结果定理1，这是我们对NB广义版本的正式陈述。1.2符号——我们将以一套理论的方式表示任何功能（例如，与每个参与方投标相关的功能）；也就是说，作为集合{（x，f（x））|x∈ domf}，通常被称为f的gr-aph。因此，例如，ca rtesian productX×{y}是定义在X上并产生y的常数函数。类似地，任何关系都将表示为通过它关联的元素对的集合；形式上，这意味着任何关系都是某个笛卡尔乘积X×Y的子集给定一个关系R，R（X）将是集合X到R:R（X）：={y |（X，y）的映像∈ R和x∈ 十} 嗯。

例如，给定一个函数f，f-1（{y}）将是f下点y的fib-er函数f对集合理论差dom f\\X的限制将写成f- 十、此外，在X={X}的特殊情况下，我们经常使用符号，写f- x而不是f- {x} .–多集（也称为包）将被扩展表示为书写，例如，{| 0，0，1，1，1，2 |}：我们记得多集类似于一个集，但每个成员都有一个多重性，描述它在多集中出现的次数。我们将使用+作为成对多集联合的FIX符号；我们会写的≤ B表示A是B的子多集的事实：例如，{2,1,1}≤ {0,0,1,1,1,2}是真的最后，x X表示X与集合X:X族中的每个集合的并运算 X:={X∪ x′：x′∈ 十} 。我们需要这个运算来说明引理1.2关于主要结果的陈述。拍卖机制通过一对函数进行数学表示。a，p：第一个描述的是如何在投标人（也称为参与者或代理人）之间分配相关商品，而第二个描述的是每个投标人在分配后支付的金额。这对函数的每个可能输出都被称为拍卖的结果。这两个函数采用相同的函数，这是另一个函数，通常称为bid向量；它描述了每个投标人对拍卖的每个可能结果的偏好程度。这种偏好关系通常通过金钱来表达，因此出价向量将某个结果与参与者对该结果的重视程度相关联。为了坚持传统的表示法，我们将使用粗体作为投标向量，如a（b）中所示。在拍卖单个商品的情况下，出价向量只需将其出价与每个投标人关联。

此外，给定一个固定的投标人i，aii的值为{0，1}，对应于我是否赢得该项目的事实。对于一个好的拍卖，Vickrey机制具有特殊的相关性，因为它具有形式属性[5,3]。它的工作原理是将货物分配给出价最高的人。然后，每个代理人支付一笔“费用”条款PI（b）- i） 不管结果如何；这笔费用并不取决于自己出价多少，而只取决于其他参与者的出价：因此p’IISB的论点- 我不喜欢全班同学。此外，胜利者支付一个适当的价格条件，该价格条件是根据不包括胜利者本人在内的一组参与者计算的最高出价（第二价格）；给定固定的投标向量b，我们将该金额表示为f（b）。拍卖机制的一个常见特性是实现预算平衡[6，第2.3节]。这意味着每个参与者所给予或接受的资金总额始终为零：bXipi（b）=0。（1） 当希望在代理集团内保持尽可能多的财富，并且转移支付可以被视为一种不受欢迎的“实施成本”时，这样的房产就具有吸引力。[1] 在一些重要的情况下，（1）采用更具体的形式：bf（b）+Xip′i（b）- i） =0，（2）其中f通常提取某种最大值：例如，对于单一良好的Vickrey机构，f（b）是第二个价格f（b）。函数p′iis通过一个简单的构造与pithr相关，我们在这里不感兴趣。

在这里，最重要的是pian和pi之间的形式差异：前者将其作为参数——我们记得bid向量被建模为函数，因此我们可以编写b-i、 使用第1.2节中介绍的符号。完整的出价向量，而后者采用缩减的出价向量，其中出价向量i已被重新移动。一个标准结果[6，定理2.2]，[5，命题3]，[2，定理4.1]是，在这种情况下，预算平衡无法满足：（1）是错误的。然而，它的已知结果都利用了（2）中出现的mapf的特殊形式，即off是f。反之亦然，我们将从（2）开始进行证明，后者被认为是未知的；专业人士将制定出需要在地图上施加的条件：只有在这之后，我们才能确定我们感兴趣的案例（例如，提到的单一商品Vickrey拍卖）的条件已经满足。为了提供更多信息，本文将介绍如何伪造方程式（2），不需要对其进行总体量化，也不需要将其作为可接受的参数tof：更小、有限的集合X将由证明本身提出。因此，我们将考虑逻辑公式B∈ XXip′i（b）- i） =f（b）（3）并研究X和f会导致什么矛盾（当然，这将包括我们的起始情况（2），其中f=-f） 。由于我们将建立一种防范机制，最大限度地降低对通用f的要求（例如，我们不会期望f是投标的最大值或第二个最大值），因此我们必须通过证明施加一些不同的前提。

需要的主要假设是对称性：虽然（1）中的PI（以及p′isin（2））是完全任意的，但我们需要要求它们不依赖于重新标记参与者：Pi b p′i（b）=p（kbk），（4）其中kRk是从关系R中获得的多集（或包）：即R的范围，但考虑到其中可能重复值的多重性。§这意味着，任何参与者i支付的价格由规则给出，仅取决于除我之外的每一次投标的金额，而不取决于谁出价。此外，这样的规则本身不能依赖于i。有了这个假设，（3）就变成了B∈ XXiP（kb）- ik）=f（b）。（5） §例如，考虑到与参与者1的投标10、参与者2的投标20和参与者3的投标10相关联的地图，获得的多集是{10，10，20}。3证明理想是投标人的数量。首先要证明的是，他们都提交了相同的（固定但任意的）投标b，由此（5）产生：PBb |{z}N-1.= kfBb |{z}N, （6） k:=nno取决于b。然后我们继续使用b，其中只有一个分量（比如说第一个分量）假设一个不同于b的任意值bdi；因此，（5）给出（N）- 1） Pb、 b，b |{z}N-2.= -PBb |{z}N-1.- f（b，b，…，b）。（7） 此时，我们希望通过利用（6）中的（7）来触发一个迭代机制。为了实现这一点，一种自然的强制方法是要求F（b，b，…，b）=qf（b，…，b）（8）对任意常数q进行替换。然后我们可以在（7）中替换（6），根据b，b得到一个有理数结b、 b，b |{z}N-2.= kf（b，…，b）。（9） 用同样的方法，我们可以建立一个有理常数k，比如thatPb、 b，b。

，b |{z}N-3.= kf（b，…，b）（10）表示任意的b，b。因此，通过迭代这个机制，我们可以构造一个绑定泛型P（{b，…，bN）的关系-2，b |}到f（b，…，b）：P（{b，…，bN）-2，b |}）=kN-2f（b，…，b）。（11） 此外，在该迭代的每个步骤中，需求（8）给出了q、q、…、。，如果我们想证明机制起作用，X和f必须是相关的。重要的是要注意，在这样做的过程中，这种相互关系应该被尽可能地削弱，唯一的理由是它们应该承认刚才概述的证明机制实际上是有效的。例如，我们在每一个归纳步骤中施加一个等式（8），但这些等式实际上只需要在某个极小值Lx内的投标向量中保持；否则，我们将把我们自己局限于f的非常小的例子。在这一节中，我们想给出一个关于证明的一般概念，但我们没有明确说明b、X和f之间的确切相互关系。事实上，这种关系一开始并非立竿见影：当证明本身正式化时，它们实际上变得更加清晰；我们觉得，用标准的纸质证据来管理这个过程会更加困难。这些关系将在第4节定义1中详细说明。上面解释的迭代意味着我们给数字q，q。。我们认为它们是任意的，因为无论我们赋予它们什么样的值，证明机制都是有效的。然而，为了简单起见，我们将工作限制在case1=q=q=，（12） 这对于任何拍卖理论的应用来说都是足够普遍的。现在的想法是取方程（11），它是用方程（5）得到的，并推导出它和方程（5）之间的协方差。

因此，形式化可以被视为分为两个阶段：第4节中介绍了引理1，它对等式（11）进行了形式化，并负责列出所有确切的要求，以便利用我们上面非正式介绍的思想推导出它。第6节还介绍了其他辅助定义和引理，它们使用引理1来获得想要的矛盾（在定理1的论文中给出）。4从概念到形式陈述给定一个多集m，b的m-限制是任何b′ b使得kb′k=m。b到b的m-完成可写为b的anm限制与常值函数b的不交并，并且dom b=dom b′。换句话说，通过改变b的值来避免对b的某些m-r限制，b到b的m-完成就可以从b得到。b的一个完整的b-完备族是一个集合，它包含一个m-对每一个可能的m的b-完备≤ kbk。引理1（lll57）。考虑b的一个完整的b-完备族Y，setX:=（{i，i}×{b}） Y代表一些i6=ioutside dom b。假设，b′∈ X:f（b′）=f（{i，i}∪ domb）×{b}（13）f（b′）=Xi∈domb′P（b′）- i） 。（14） 然后p（kbk+{| b |}）=2+| dom b | f（{i，i}∪ domb）×{b}）。在后面的讨论中，将引理1中的需求表示为谓词形式的等式（13）是有用的：定义1。[pred2，pred3]如果-X={i，i}，那么集合X对于五元组（b，b，f，i，i）是足够的 对于某些情况，Y是b的b-完全族；——b′∈ xf（b′）=f（{i，i}∪ domb）×{b}）。这允许我们将引理1重新表述为引理2（lll57）。