About the Project
Matching is a fundamental problem in combinatorial optimisation with multiple applications in AI, like in belief propagation [10], multi-agent resource allocation algorithms [6], and constraint solving [16], and in economics, like the stable marriage problem [17] and the Adwords market [15], among many other applications. In its most basic form, given an undirected graph, a matching is a set of vertex disjoint edges, and a maximum cardinality matching is a matching with the maximum number of edges. In addition to those wide applications, the theory of matching and its connections to other optimisation problems is one of the richest areas in computer science and combinatorial optimisation. For example, the notion of polynomial time computation as efficient computation was conceived by Jack Edmonds, when he discovered his blossom shrinking algorithm for solving maximum cardinality matching in general graphs [1].
In this project, we propose you do research on the formal verification of matching algorithms and matching theory, with some emphasis on applications with a social welfare dimension. Concrete examples are the verification of software used for socially relevant problems, like kidney matching [4], school-pupil matching [14], and hospital-doctor matching [9]. Having formal guarantees on these programs is of great importance due what is at stake if they are unverified: for instance, not as many people might live if a kidney exchange matching program has bugs, and diversity or other social welfare goals might be jeopardised if a school-pupil matching program has bugs.
As a method to obtain formal correctness guarantees, we propose you use interactive theorem provers (ITPs). To prove a fact in an ITP, the user provides high-level steps of a proof, and the ITP fills in the details, at the level of axioms, culminating in a formal proof. The fact that ITPs can use human expertise is a source of their strength in many applications, e.g. when the properties to prove are undecidable. E.g. ITPs are the most successful approach to implement verified realistic software systems [13, 12, 11], where automated methods stand no chance. Also, importantly, ITPs have been used to construct formal proofs of correctness for many central results in combinatorial optimisation, e.g. Edmond’s blossom shrinking algorithm for computing maximum cardinality matchings in general graphs [5], the Edmond-Karp algorithms for computing flows [7], and the simplex algorithm to optimally solve linear programs [8].
There are multiple directions in which you could take this project. Taking the kidney matching example, you might focus on building formal mathematical libraries, containing correct algorithms and linear programming encodings to solve kidney matching optimally w.r.t. several existing criteria (e.g. see [4]), or you can focus on devising new criteria w.r.t. which one can judge kidney matchings, and devise new methods to compute matchings optimising these new criteria, and formally prove properties of those methods and criteria with an ITP. Another direction is the verification of areas of matching theory with game-theoretic aspects, which are mainly applied to the organisation of multi-agent systems (see for instance [3, 2]). An important of your research in this project is formally verifying significant parts of state-of-the-art matching algorithms and theory.
References
[1] Jack Edmonds. Paths, Trees, and Flowers. Can. J. Math., 1965/ed.
[2] Jugal Garg, Thorben Tröbst, and Vijay V. Vazirani. One-Sided Matching Markets with Endowments: Equilibria
and Algorithms. In 21st International Conference on Autonomous Agents and Multiagent Systems, AAMAS
2022, Auckland, New Zealand, May 9-13, 2022, 2022.
[3] Mojtaba Hosseini and Vijay V. Vazirani. Nash-Bargaining-Based Models for Matching Markets: One-Sided and
Two-Sided; Fisher and Arrow-Debreu. In 13th Innovations in Theoretical Computer Science Conference, ITCS
2022, January 31 – February 3, 2022, Berkeley, CA, USA, 2022.
[4] Péter Biró, Joris van de Klundert, David Manlove, William Pettersson, Tommy Andersson, Lisa Burnapp, Pavel
Chromy, Pablo Delgado, Piotr Dworczak, Bernadette Haase, Aline Hemke, Rachel Johnson, Xenia Klimentova,
Dirk Kuypers, Alessandro Nanni Costa, Bart Smeulders, Frits Spieksma, Marı́a O. Valentı́n, and Ana Viana.
Modelling and optimisation in European Kidney Exchange Programmes. Eur. J. Oper. Res., 2021.
[5] Mohammad Abdulaziz, Kurt Mehlhorn, and Tobias Nipkow. Trustworthy graph algorithms (invited paper). In
The 44th International Symposium on Mathematical Foundations of Computer Science (MFCS), 2019.
[6] Haris Aziz, Serge Gaspers, Zhaohong Sun, and Toby Walsh. From Matching with Diversity Constraints to
Matching with Regional Quotas. In 18th International Conference on Autonomous Agents and MultiAgent
Systems (AAMAS), 2019.[7] Peter Lammich and S. Reza Sefidgar. Formalizing Network Flow Algorithms: A Refinement Approach in Isabelle/HOL. J. Autom. Reason., 2019.
[8] Filip Maric, Mirko Spasic, and René Thiemann. An Incremental Simplex Algorithm with Unsatisfiable Core
Generation. Arch. Formal Proofs, 2018.
[9] Yuichiro Kamada and Fuhito Kojima. Stability concepts in matching under distributional constraints. Journal
of Economic Theory, 2017.
[10] Sungsoo Ahn, Sejun Park, Michael Chertkov, and Jinwoo Shin. Minimum Weight Perfect Matching via Blossom Belief Propagation. In Advances in Neural Information Processing Systems 28: Annual Conference on Neural Information Processing Systems 2015, December 7-12, 2015, Montreal, Quebec, Canada, 2015.
[11] Sudeep Kanav, Peter Lammich, and Andrei Popescu. A Conference Management System with Verified Document Confidentiality. In The 26th International Conference on Computer Aided Verification (CAV), 2014.
[12] Gerwin Klein, Kevin Elphinstone, Gernot Heiser, June Andronick, David Cock, Philip Derrin, Dhammika
Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, Thomas Sewell, Harvey Tuch, and Simon Winwood.
seL4: Formal verification of an OS kernel. In 22nd ACM Symposium on Operating Systems Principles 2009
(SOSP), 2009.
[13] Xavier Leroy. Formal verification of a realistic compiler. Commun. ACM, 2009.
[14] Atila Abdulkadiroglu. College admissions with affirmative action. Int. J. Game Theory, 2005.
[15] Aranyak Mehta, Amin Saberi, Umesh V. Vazirani, and Vijay V. Vazirani. AdWords and Generalized On-line
Matching. In 46th Annual IEEE Symposium on Foundations of Computer Science (FOCS 2005), 23-25 October
2005, Pittsburgh, PA, USA, Proceedings, 2005.
[16] Jean-Charles Régin. A Filtering Algorithm for Constraints of Difference in CSPs. In Proceedings of the 12th
National Conference on Artificial Intelligence, Seattle, WA, USA, July 31 – August 4, 1994, Volume 1, 1994.
[17] D. Gale and L. S. Shapley. College Admissions and the Stability of Marriage. The American Mathematical
Monthly, 1962.
Continue with Facebook
