Automating the Analysis of Matching Algorithms

This paper introduces a new approach to automating the task of evaluating the algorithms used to match job applicants to companies or students to schools.

The development of algorithms to match, for instance, students to schools or organ donors to patients has been one of the grand success stories of the Economic Sciences, leading to significant benefits to society at large. This was recognised with the Nobel Prize awarded to Alvin Roth and Lloyd Shapley in 2012.

Ideally, we would like to design matching algorithms that satisfy a wide range of attractive properties, such as leading to stable assignments, being fair, or incentivising participants to be truthful. But understanding the precise limits of what is possible in this domain is very difficult and continues to be an active area of research in Economics.

In this paper, I describe a new approach to automate some of the tasks of researchers in Economics who investigate the possibility of designing a new matching algorithm with a given set of desirable properties. The basic idea is to encode these properties in a logical language, thereby reducing the question of whether a matching algorithm of the desired kind exists to the question of whether a certain (very large) formula is logically consistent.

Reference: Ulle Endriss. Analysis of One-to-One Matching Mechanisms via SAT Solving: Impossibilities for Universal Axioms. In Proceedings of the 34th AAAI Conference on Artificial Intelligence, 2020.

Other papers

Are LLMs classical or nonmonotonic reasoners? Lessons from generics
Quantifying Context Mixing in Transformers
Reclaiming AI as a theoretical tool for cognitive science
Dealing with semantic underspecification in multimodal NLP
How robust and reliable can we expect language models to be?
Which stereotypes do search engines come with?