Formal Representation and Proof for Cooperative Games: A Foundation for Complex Social Behaviour
Lead Research Organisation:
University of Birmingham
Department Name: School of Computer Science
Abstract
This research applies methods and tools from mathematical knowledge
management and theorem proving to theoretical economics, by working
with a class of cooperative games called pillage games. Pillage
games, introduced by Jordan in 2006, provide a formal way of
thinking about the ability of powerful coalitions to take resources
from less powerful ones. While their name suggests primitive,
violent interactions, pillage games are more applicable to advanced
democracies, in which coalitions seek to form governments to alter
the distribution of society's resources in their favour. If, for
some allocation of society's resources, the coalition preferring
another allocation is stronger than that preferring the status quo,
the other allocation `dominates' the status quo.
The most conceptually intriguing, and the most computationally
intractable solution concept for cooperative games is the `stable
set'. A stable set, has two features: no allocation in the set
dominates another; each allocation outside the set is dominated by an
allocation in the set. For pillage games with three agents under a few
additional conditions, we have determined when stable sets exist, that
they are unique and contain no more than 15 allocations, and how to
determine them for a given power function.
In this research, we first formally represent the mathematical
knowledge developed in Jordan's and our work using sTeX, a
mathematical knowledge management tool. This allows, e.g., automatic
identification of how various results depend on each other.
We then use two modern automated theorem provers (ATPs), Isabelle and
Theorema, to formally prove these results. Theorem proving is a hard
task and if not provided with domain specific knowledge ATPs have to
search through big search spaces in order to find proofs. To increase
their reasoning power, we shall seek to identify recurring patterns in
proofs, and extract proof tactics, reducing the interactions necessary
to prove the theorems interactively. As important results in pillage
games can be summarised in pseudo-algorithms, containing both
computational and non-computational steps, we shall study such
pseudo-algorithms, seeking to push them towards the much more
efficient computational steps. Finally, we shall use the identified
proof tactics to help the ATPs prove new results in order evaluate
their true value.
The research seeks to make a number of contributions. For theorem
proving, pillage games form a new set of challenge problems. As the
study of pillage games is new, and the canon of applicable knowledge
small, this gives an unprecedented opportunity to encode most of
it. The research will expand the tractable problem domain for ATPs;
and - by identifying successful tactics - increase both the efficiency
with which ATPs search for proofs, and - ideally - their ability to
establish new results.
For economics, this is the first major application of formal knowledge
management and theorem proving techniques. The few previous
applications of ATP to economics have formalised isolated results
without engaging economists and have thus largely gone unnoticed by
the discipline. As cooperative games are a known hard class of
economic problems, and pillage games known to be tractable, this
research therefore presents a strong `proof of concept' for the use of
ATP within economics. Cooperative game theory is formally similar
to graph theory, the techniques and insights developed may be
applicable to matching problems, network economics, operations
research, and combinatorial optimisation more generally.
Additionally, the researchers will introduce ATP techniques to the
leading PhD summer school in computational economics, and are working
in collaboration with economic theorists with strong computational
backgrounds. Thus, the research seeks to form a focal point for formal
knowledge management and theorem proving efforts in economics.
management and theorem proving to theoretical economics, by working
with a class of cooperative games called pillage games. Pillage
games, introduced by Jordan in 2006, provide a formal way of
thinking about the ability of powerful coalitions to take resources
from less powerful ones. While their name suggests primitive,
violent interactions, pillage games are more applicable to advanced
democracies, in which coalitions seek to form governments to alter
the distribution of society's resources in their favour. If, for
some allocation of society's resources, the coalition preferring
another allocation is stronger than that preferring the status quo,
the other allocation `dominates' the status quo.
The most conceptually intriguing, and the most computationally
intractable solution concept for cooperative games is the `stable
set'. A stable set, has two features: no allocation in the set
dominates another; each allocation outside the set is dominated by an
allocation in the set. For pillage games with three agents under a few
additional conditions, we have determined when stable sets exist, that
they are unique and contain no more than 15 allocations, and how to
determine them for a given power function.
In this research, we first formally represent the mathematical
knowledge developed in Jordan's and our work using sTeX, a
mathematical knowledge management tool. This allows, e.g., automatic
identification of how various results depend on each other.
We then use two modern automated theorem provers (ATPs), Isabelle and
Theorema, to formally prove these results. Theorem proving is a hard
task and if not provided with domain specific knowledge ATPs have to
search through big search spaces in order to find proofs. To increase
their reasoning power, we shall seek to identify recurring patterns in
proofs, and extract proof tactics, reducing the interactions necessary
to prove the theorems interactively. As important results in pillage
games can be summarised in pseudo-algorithms, containing both
computational and non-computational steps, we shall study such
pseudo-algorithms, seeking to push them towards the much more
efficient computational steps. Finally, we shall use the identified
proof tactics to help the ATPs prove new results in order evaluate
their true value.
The research seeks to make a number of contributions. For theorem
proving, pillage games form a new set of challenge problems. As the
study of pillage games is new, and the canon of applicable knowledge
small, this gives an unprecedented opportunity to encode most of
it. The research will expand the tractable problem domain for ATPs;
and - by identifying successful tactics - increase both the efficiency
with which ATPs search for proofs, and - ideally - their ability to
establish new results.
For economics, this is the first major application of formal knowledge
management and theorem proving techniques. The few previous
applications of ATP to economics have formalised isolated results
without engaging economists and have thus largely gone unnoticed by
the discipline. As cooperative games are a known hard class of
economic problems, and pillage games known to be tractable, this
research therefore presents a strong `proof of concept' for the use of
ATP within economics. Cooperative game theory is formally similar
to graph theory, the techniques and insights developed may be
applicable to matching problems, network economics, operations
research, and combinatorial optimisation more generally.
Additionally, the researchers will introduce ATP techniques to the
leading PhD summer school in computational economics, and are working
in collaboration with economic theorists with strong computational
backgrounds. Thus, the research seeks to form a focal point for formal
knowledge management and theorem proving efforts in economics.
Planned Impact
The project seeks impact primarily by engaging with the academic
computer science and economics communities. This will be done in
departmental seminars, workshops (e.g., UK Automated Reasoning
Workshop), tutorials (e.g., the ESSLLI summer school) and
conferences (e.g., CICM, and conferences by economics societies
such as the Society for Computational Economics). We have been
invited to present the work to the 2012 Initiative for
Computational Economics in Chicago, economics' principle training
ground in computational methods for PhD students.
Finished work will be submitted to internationally recognised
journals. Within computer science, these are journals such as the
Journal of Automated Reasoning, Artificial Intelligence, the
Journal of Applied Logic. Within economics, outlets include leading
theory journals such as the International Journal of Game Theory,
Games and Economic Behavior, Computational Economics and, for a
survey article, the Journal of Economic Literature.
Efforts will be made to communicate results to the public more
broadly, ideally through a popular science journal.
The project will also establish a website with three goals. First,
to disseminate work and results, including research reports,
encodings of the problems for various theorem provers, all code and
algorithms written. Second, the website will seek to facilitate the
growth of an ATP sub-community within economics, encouraging the
use and understanding of ATP and a search for fruitful application
domains. Initially, this will be organised around a wiki on key
theorems in economics. It will also host a discussion forum for the
discussion of approaches, problems, and solutions in formalised
economics. Finally, the website will be a key resource for formally
representing and proving knowledge related to theoretical
economics, whether by hosting material itself, or linking to it
elsewhere.
Research in mechanised theorem proving has applications beyond
academia. We shall initially explore applications formally close to
either our work or to previous work. As our work is formally similar
to matching problems, they are a natural application domain. Matching
problems include that of matching students to schools, organ donors to
recipients, and interns to hospitals.
Existing applications of mechanised theorem proving to economics have
focused on results in social choice. One of these, the
Gibbard-Satterthwaite theorem, is a central result in mechanism
design, which includes auction theory as a subfield. Auctions are now
a major method for allocating resources, whether via Google's online
ads, oil fields development, contract auctions, or procurement
auctions. Further, good design can make large differences to the
revenues generated: the top two European spectrum license auctions in
2000 earned over 30 times what the bottom one earned. Thus, mechanised
theorem proving could aid in the design of and participation in
auctions.
Another important way to achieve impact is by our internationally
leading project partners. They will not only advise us but also
actively support us in our aspiration and in the dissemination of
the results. We have an industrial advisor who will not only advise
us on the research side of the project but will also give valuable
contributions on how to apply the work outside academia. Our other
project partners are senior figures in computer science and
economics. They have strong expertise in all relevant aspects of
the project. We have leading figures who are opinion formers in
their respective fields of expertise: development of mathematical
knowledge representation formalisms, theorem proving systems,
maintaining a large collection of challenge problems on the
computer science side of the project; pillage games, rationality,
computational economics, developing software for solving
non-cooperative games on the economics side.
computer science and economics communities. This will be done in
departmental seminars, workshops (e.g., UK Automated Reasoning
Workshop), tutorials (e.g., the ESSLLI summer school) and
conferences (e.g., CICM, and conferences by economics societies
such as the Society for Computational Economics). We have been
invited to present the work to the 2012 Initiative for
Computational Economics in Chicago, economics' principle training
ground in computational methods for PhD students.
Finished work will be submitted to internationally recognised
journals. Within computer science, these are journals such as the
Journal of Automated Reasoning, Artificial Intelligence, the
Journal of Applied Logic. Within economics, outlets include leading
theory journals such as the International Journal of Game Theory,
Games and Economic Behavior, Computational Economics and, for a
survey article, the Journal of Economic Literature.
Efforts will be made to communicate results to the public more
broadly, ideally through a popular science journal.
The project will also establish a website with three goals. First,
to disseminate work and results, including research reports,
encodings of the problems for various theorem provers, all code and
algorithms written. Second, the website will seek to facilitate the
growth of an ATP sub-community within economics, encouraging the
use and understanding of ATP and a search for fruitful application
domains. Initially, this will be organised around a wiki on key
theorems in economics. It will also host a discussion forum for the
discussion of approaches, problems, and solutions in formalised
economics. Finally, the website will be a key resource for formally
representing and proving knowledge related to theoretical
economics, whether by hosting material itself, or linking to it
elsewhere.
Research in mechanised theorem proving has applications beyond
academia. We shall initially explore applications formally close to
either our work or to previous work. As our work is formally similar
to matching problems, they are a natural application domain. Matching
problems include that of matching students to schools, organ donors to
recipients, and interns to hospitals.
Existing applications of mechanised theorem proving to economics have
focused on results in social choice. One of these, the
Gibbard-Satterthwaite theorem, is a central result in mechanism
design, which includes auction theory as a subfield. Auctions are now
a major method for allocating resources, whether via Google's online
ads, oil fields development, contract auctions, or procurement
auctions. Further, good design can make large differences to the
revenues generated: the top two European spectrum license auctions in
2000 earned over 30 times what the bottom one earned. Thus, mechanised
theorem proving could aid in the design of and participation in
auctions.
Another important way to achieve impact is by our internationally
leading project partners. They will not only advise us but also
actively support us in our aspiration and in the dissemination of
the results. We have an industrial advisor who will not only advise
us on the research side of the project but will also give valuable
contributions on how to apply the work outside academia. Our other
project partners are senior figures in computer science and
economics. They have strong expertise in all relevant aspects of
the project. We have leading figures who are opinion formers in
their respective fields of expertise: development of mathematical
knowledge representation formalisms, theorem proving systems,
maintaining a large collection of challenge problems on the
computer science side of the project; pillage games, rationality,
computational economics, developing software for solving
non-cooperative games on the economics side.
Organisations
- University of Birmingham (Lead Research Organisation)
- University of Michigan–Ann Arbor (Project Partner)
- Stanford University (Project Partner)
- University of Miami (Project Partner)
- Articulate Software (Project Partner)
- University of Queensland (Project Partner)
- Pennsylvania State University (Project Partner)
- Johannes Kepler University of Linz (Project Partner)
- University of Bristol (Project Partner)
- Jacobs University (Project Partner)
People |
ORCID iD |
Manfred Kerber (Principal Investigator) | |
Colin Rowat (Co-Investigator) |
Publications
Marco B. Caminati
(2015)
VCG - Combinatorial Vickrey-Clarke-Groves Auctions
in Archive of Formal Proofs
Caminati Marco B.
(2014)
Set Theory or Higher Order Logic to Represent Auction Concepts in Isabelle?
in arXiv e-prints
Caminati Marco B.
(2014)
Budget Imbalance Criteria for Auctions: A Formalized Theorem
in arXiv e-prints
Caminati Marco B.
(2013)
Proving soundness of combinatorial Vickrey auctions and generating verified executable code
in arXiv e-prints
Zeng X
(2023)
Win-Win: Anthropogenic circularity for metal criticality and carbon neutrality.
in Frontiers of environmental science & engineering
MacKenzie S
(2015)
Pillage games with multiple stable sets
in International Journal of Game Theory
Kerber M
(2016)
An introduction to mechanized reasoning
in Journal of Mathematical Economics
Beardon A
(2013)
Efficient sets are small
in Journal of Mathematical Economics
Rowat C
(2014)
Sufficient conditions for unique stable sets in three agent pillage games
in Mathematical Social Sciences
Wang MD
(2022)
Measuring political and economic uncertainty: a supervised computational linguistic approach.
in SN business & economics
Description | We have developed an approach to generate provably reliable software in applications of the field of economics. We have applied the method in the area of auction design. The approach consists of formalising an auction in the formal language of the Isabelle theorem prover, proving its properties within the system and using the code extraction mechanism to generate the code automatically. |
Exploitation Route | Up to now the approach has been used to give a proof of principle. The next step will be to apply it to one (or some) of the most recently developed auction schemas. |
Sectors | Creative Economy Retail Other |
URL | http://www.cs.bham.ac.uk/research/projects/formare/ |
Description | We have actively approached economists and have found interest there, but up to now the results have not been used (to our knowledge). We put further efforts into the application in the auction domain. We have continued applying formal methods developed in the project to other domains. We (the two investigators) have founded a company and try to offer services on applying formal verification in finance, in particular, by proving formal properties of risk analysis. |
First Year Of Impact | 2017 |
Sector | Financial Services, and Management Consultancy |
Impact Types | Economic |
Title | Auction Theory Toolbox (ATT) |
Description | We have used different languages for the formalisation of Auctions. For details, see http://www.cs.bham.ac.uk/research/projects/formare/code/auction-theory/ |
Type Of Technology | Software |
Year Produced | 2012 |
Open Source License? | Yes |
Impact | Building on the implementation it is much easier to formalise and implement other auction schemas. |
URL | http://www.cs.bham.ac.uk/research/projects/formare/code/auction-theory/ |
Description | An economist's guide to mechanized reasoning or My computer just proved 84 impossibility theorems |
Form Of Engagement Activity | A talk or presentation |
Part Of Official Scheme? | Yes |
Geographic Reach | International |
Primary Audience | Postgraduate students |
Results and Impact | Invited lecture at the Summer School of the Initiative for Computational Economics, 2012 in Chicago, USA. We gave an overview of the potential of applying formal methods to economics from an economics perspective. We have been in touch with a number of economists who showed interest in our work. This is essential for our project, since we want to show the usefulness of formal systems in economics. |
Year(s) Of Engagement Activity | 2012 |
URL | http://cs.bham.ac.uk/research/projects/formare/pubs/ice2012/2012-07-25-ice-mech-reas-econ.pdf |
Description | Departmental Seminar |
Form Of Engagement Activity | A talk or presentation |
Part Of Official Scheme? | No |
Geographic Reach | Local |
Primary Audience | Other academic audiences (collaborators, peers etc.) |
Results and Impact | Application of different theorem proving systems Exchange of ideas |
Year(s) Of Engagement Activity | 2015 |
URL | http://www.cs.york.ac.uk/research/research-seminars/ |
Description | Formalising "100" Theorems/Models/Theories in Economics |
Form Of Engagement Activity | A magazine, newsletter or online publication |
Part Of Official Scheme? | No |
Geographic Reach | International |
Primary Audience | Professional Practitioners |
Results and Impact | This page attempts to do for theorems in economics what Freek Wiedijk's page does for mathematical theorems more generally. It inherits the same caveats, as well as adopting a dynamic definition of 100. This has not yet attracted major attention to our knowledge. |
Year(s) Of Engagement Activity | 2012 |
URL | https://github.com/formare/community/wiki/Formalising-%E2%80%9C100%E2%80%9D-Theorems-Models-Theories... |
Description | Invited Talk |
Form Of Engagement Activity | A talk or presentation |
Part Of Official Scheme? | No |
Geographic Reach | International |
Primary Audience | Policymakers/politicians |
Results and Impact | Discussion on Electricity Auctions |
Year(s) Of Engagement Activity | 2013 |
URL | http://www.cwciraqpower.com/ |
Description | Seminar at the Technical University of Munich, Isabelle Group |
Form Of Engagement Activity | A talk or presentation |
Part Of Official Scheme? | No |
Geographic Reach | International |
Primary Audience | Other audiences |
Results and Impact | Presentation of a seminar and discussion on the application of the Isabelle system for the verification of auctions. |
Year(s) Of Engagement Activity | 2016 |
URL | http://www.cs.bham.ac.uk/~mmk/talks/16-munich.pdf |