Formal Representation and Proof for Cooperative Games: A Foundation for Complex Social Behaviour

合作博弈的形式表示和证明：复杂社会行为的基础

• 批准号: EP/J007498/1
• 负责人: Manfred Kerber
• 金额: $ 49.64万
• 依托单位: University of Birmingham
• 依托单位国家: 英国
• 项目类别: Research Grant
• 财政年份: 2012
• 资助国家: 英国
• 起止时间: 2012 至 无数据
• 项目状态: 已结题
• 来源: https://gtr.ukri.org/projects?ref=EP%2FJ007498%2F1
• 关键词: Formal; Representation; Proof; Cooperative; Games

This research applies methods and tools from mathematical knowledgemanagement and theorem proving to theoretical economics, by workingwith a class of cooperative games called pillage games. Pillagegames, introduced by Jordan in 2006, provide a formal way ofthinking about the ability of powerful coalitions to take resourcesfrom less powerful ones. While their name suggests primitive,violent interactions, pillage games are more applicable to advanceddemocracies, in which coalitions seek to form governments to alterthe distribution of society's resources in their favour. If, forsome allocation of society's resources, the coalition preferringanother allocation is stronger than that preferring the status quo,the other allocation `dominates' the status quo.The most conceptually intriguing, and the most computationallyintractable solution concept for cooperative games is the `stableset'. A stable set, has two features: no allocation in the setdominates another; each allocation outside the set is dominated by anallocation in the set. For pillage games with three agents under a fewadditional conditions, we have determined when stable sets exist, thatthey are unique and contain no more than 15 allocations, and how todetermine them for a given power function.In this research, we first formally represent the mathematicalknowledge developed in Jordan's and our work using sTeX, amathematical knowledge management tool. This allows, e.g., automaticidentification of how various results depend on each other.We then use two modern automated theorem provers (ATPs), Isabelle andTheorema, to formally prove these results. Theorem proving is a hardtask and if not provided with domain specific knowledge ATPs have tosearch through big search spaces in order to find proofs. To increasetheir reasoning power, we shall seek to identify recurring patterns inproofs, and extract proof tactics, reducing the interactions necessaryto prove the theorems interactively. As important results in pillagegames can be summarised in pseudo-algorithms, containing bothcomputational and non-computational steps, we shall study suchpseudo-algorithms, seeking to push them towards the much moreefficient computational steps. Finally, we shall use the identifiedproof tactics to help the ATPs prove new results in order evaluatetheir true value.The research seeks to make a number of contributions. For theoremproving, pillage games form a new set of challenge problems. As thestudy of pillage games is new, and the canon of applicable knowledgesmall, this gives an unprecedented opportunity to encode most ofit. The research will expand the tractable problem domain for ATPs;and - by identifying successful tactics - increase both the efficiencywith which ATPs search for proofs, and - ideally - their ability toestablish new results.For economics, this is the first major application of formal knowledgemanagement and theorem proving techniques. The few previousapplications of ATP to economics have formalised isolated resultswithout engaging economists and have thus largely gone unnoticed bythe discipline. As cooperative games are a known hard class ofeconomic problems, and pillage games known to be tractable, thisresearch therefore presents a strong `proof of concept' for the use ofATP within economics. Cooperative game theory is formally similarto graph theory, the techniques and insights developed may beapplicable to matching problems, network economics, operationsresearch, and combinatorial optimisation more generally.Additionally, the researchers will introduce ATP techniques to theleading PhD summer school in computational economics, and are workingin collaboration with economic theorists with strong computationalbackgrounds. Thus, the research seeks to form a focal point for formalknowledge management and theorem proving efforts in economics.

这项研究通过一类称为掠夺游戏的合作游戏，将数学知识管理和定理证明的方法和工具应用于理论经济学。约旦于 2006 年推出的掠夺游戏提供了一种正式的方式来思考强大联盟从较弱联盟手中夺取资源的能力。虽然掠夺游戏的名字暗示着原始的、暴力的互动，但它更适用于先进的民主国家，在这些国家中，联盟寻求组建政府，以有利于自己的方式改变社会资源的分配。如果，对于社会资源的某种配置，偏好另一种分配的联盟比偏好现状的联盟更强，则另一种分配“支配”现状。对于合作博弈，概念上最有趣、计算上最难解决的解决方案概念是“稳定集” 。一个稳定的集合，有两个特点：集合中没有分配支配另一个集合；集合外的每个分配都受集合内分配的支配。对于在一些附加条件下具有三个代理的掠夺博弈，我们已经确定了何时存在稳定集，它们是唯一的且包含不超过 15 个分配，以及如何针对给定的幂函数确定它们。在本研究中，我们首先正式表示数学知识Jordan 和我们使用 sTeX（数学知识管理工具）开发的。例如，这允许自动识别各种结果如何相互依赖。然后，我们使用两个现代自动定理证明器（ATP）Isabelle 和 Theorema 来正式证明这些结果。定理证明是一项艰巨的任务，如果没有提供特定领域的知识，ATP 就必须在巨大的搜索空间中进行搜索才能找到证明。为了提高他们的推理能力，我们将寻求识别证明中重复出现的模式，并提取证明策略，减少交互式证明定理所需的交互。由于掠夺游戏中的重要结果可以概括为包含计算步骤和非计算步骤的伪算法，因此我们将研究此类伪算法，寻求将它们推向更高效的计算步骤。最后，我们将使用已识别的证明策略来帮助 ATP 证明新结果，以评估其真正价值。本研究旨在做出一些贡献。为了改进理论，掠夺博弈形成了一组新的挑战问题。由于掠夺游戏的研究是新的，并且适用知识的标准很小，这为编码大部分知识提供了前所未有的机会。该研究将扩大 ATP 的可处理问题领域；并且通过确定成功的策略，提高 ATP 搜索证据的效率，以及理想情况下建立新结果的能力。对于经济学来说，这是正式知识管理的第一个主要应用和定理证明技术。 ATP 之前在经济学中的少数应用在没有经济学家参与的情况下将孤立的结果形式化，因此在很大程度上没有被该学科注意到。由于合作博弈是一类已知的困难经济问题，而掠夺博弈则易于处理，因此这项研究为 ATP 在经济学中的使用提供了强有力的“概念证明”。合作博弈论在形式上类似于图论，所开发的技术和见解可能适用于匹配问题、网络经济学、运筹学和更广泛的组合优化。此外，研究人员将向计算经济学领域领先的博士暑期学校介绍 ATP 技术，并且与具有强大计算背景的经济理论家合作。因此，该研究旨在形成经济学中正式知识管理和定理证明工作的焦点。

项目成果

An Introduction to Mechanized Reasoning

• DOI: 10.1016/j.jmateco.2016.06.005
• 发表时间: 2016-03
• 期刊: ArXiv
• 作者: Manfred Kerber;C. Lange;C. Rowat

Sound Auction Specification and Implementation

完善的拍卖规范和实施

• DOI: 10.1145/2764468.2764511
• 发表时间: 2015
• 作者: Caminati M

Efficient sets are small

高效集很小

• DOI: 10.1016/j.jmateco.2013.04.006
• 发表时间: 2013
• 期刊: Journal of Mathematical Economics
• 影响因子: 1.3
• 作者: Beardon A

Proving soundness of combinatorial Vickrey auctions and generating verified executable code

证明组合维克里拍卖的健全性并生成经过验证的可执行代码

• DOI: 10.48550/arxiv.1308.1779
• 发表时间: 2013
• 期刊: arXiv e-prints
• 作者: Caminati Marco B.

Applying Mechanised Reasoning in Economics - Making Reasoners Applicable for Domain Experts

在经济学中应用机械化推理——使推理器适用于领域专家

• 发表时间: 2013
• 作者: Christoph Lange