Formal Methods for Social Choice Theory

社会选择理论的形式化方法

• 批准号: 1931623
• 金额: --
• 依托单位: University of Edinburgh
• 依托单位国家: 英国
• 项目类别: Studentship
• 财政年份: 2017
• 资助国家: 英国
• 起止时间: 2017 至 无数据
• 项目状态: 已结题
• 来源: https://gtr.ukri.org/projects?ref=studentship-1931623
• 关键词: Formal; Methods; Social; Choice; Theory

Social choice theory provides a mathematical framework for combining the preferences of individuals in such a way as to maximise collective social welfare. Some of the most famous results come from the branch of social choice theory known as voting theory, namely Arrow's impossibility theorem and the Gibbard-Satterthwaite theorem. They both describe some simple, desirable properties of a system such as there being no dictator (a voter who can unilaterally decide the outcome), and prove that there must be a dictator if all other desirable properties hold.This form of argument is a familiar sight to mathematicians, particularly those who practice formal logic. You begin with some sensible, consistent axioms and explore the consequences. After exploring thoroughly, tweak an axiom or two and explore again. This is essentially how hyperbolic geometry was discovered, born from traditional Euclidean geometry by tweaking one axiom. Social choice theory has historically not been so rigorous and the arguments, while mathematical, were nevertheless informal.There is an increasing interest in the intersection of computer science and social choice thoery. Considering the field's application to reasoning about what is best for a person, group, or larger society, it is certainly something we want to get right, particularly with the looming AI explosion. While the majority of recent developments in this intersection have been about the computational aspects of algorithms and developing new aggregation mechanisms with computational properties in mind (often referred to as Computational Social Choice Theory), we will be investigating the application of formal logic to the field.We will develop a dynamic logic in the Isabelle/HOL interactive proof system and use it to formally prove properties of various mechanisms. Much of the effort related to formal methods in social chocie theory has been about semi-informal (informal in the sense of not implemented and verified in a proof system) developments of domain-specific logics, such as logics for game theory, coalition formation, and resource negotiations. We believe it would be highly beneficial to use a generic logic such as an extended dynamic logic for proving input-output properties of mechanisms, and being able to extract correct programs verified by this logic. This logic should be extendable by users to include new axioms while leaving them with access to the body of proofs proven without the additional axioms, and Isabelle's locales are a convenient mechanism for achieving this.Finally, while social choice theory typically concerns itself with deterministic environments and mechanisms (eg. auctions, voting, resource allocations), we will also extend this logic to equip it with the expressive power to be able to formalise properties of probabilistic mechanisms and systems, with the hope that this can serve as a basis for future formal developments of social choice theory and its related fields.

社会选择理论提供了一个数学框架，用于将个人偏好以最大化集体社会福利的方式结合起来。一些最著名的结果来自社会选择理论的分支，即阿罗不可能定理和吉布斯-萨特思韦特定理。他们都描述了系统的一些简单的、令人满意的性质，比如没有独裁者（一个可以单方面决定结果的选民），并证明了如果所有其他令人满意的性质都成立，那么就必须有一个独裁者。你开始与一些明智的，一致的公理和探索的后果。在彻底探索之后，调整一两个公理，然后再探索。这就是双曲几何被发现的本质，它是通过调整一个公理从传统的欧几里得几何中诞生的。社会选择理论在历史上并不那么严格，其论点虽然是数学的，但也是非正式的。人们对计算机科学和社会选择理论的交叉越来越感兴趣。考虑到该领域在推理什么对一个人、一个团体或更大的社会最好方面的应用，这当然是我们想要做好的事情，特别是在人工智能爆炸即将到来的情况下。虽然在这个交叉点的大多数最近的发展是关于算法的计算方面和开发新的聚合机制与计算属性铭记（通常被称为计算社会选择理论），我们将研究形式逻辑在该领域的应用。我们将在Isabelle/中开发动态逻辑HOL交互式证明系统，并利用它对各种机制的性质进行形式化证明。社会选择理论中与形式方法相关的大部分努力都是关于特定领域逻辑的半非正式（非正式的意义是在证明系统中没有实现和验证）发展，例如博弈论，联盟形成和资源谈判的逻辑。我们相信，这将是非常有益的，使用一个通用的逻辑，如扩展的动态逻辑证明输入输出性能的机制，并能够提取正确的程序验证了这个逻辑。这种逻辑应该是可扩展的用户，包括新的公理，同时让他们访问的身体证明没有额外的公理，和伊莎贝尔的地区是一个方便的机制，实现这一点。最后，虽然社会选择理论通常关注自己与确定性的环境和机制（例如，社会选择理论）。拍卖，投票，资源分配），我们还将扩展这个逻辑，使其具有表达能力，能够形式化概率机制和系统的属性，希望这可以作为社会选择理论及其相关领域未来正式发展的基础。