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.