Christian Geist and Ulle Endriss win 2016 IJCAI-JAIR Best Paper Prize

Christian Geist and Ulle Endriss will receive the 2016 IJCAI-JAIR Best Paper Prize for their paper "Automated Search for Impossibility Theorems in Social Choice Theory: Ranking Sets of Objects", published in the Journal of Artificial Intelligence Research (JAIR) in 2011. The paper is based on Christian's Master of Logic thesis, which he defended at the ILLC in 2010. This prize is awarded annually to an outstanding paper published in the journal in the preceding five calendar years. Funding for the award is provided by the International Joint Conference on Artificial Intelligence (IJCAI). The prize will be formally announced during an awards ceremony at IJCAI in New York City this July.

The paper develops a methodology, based on core techniques in Artificial Intelligence, to automatically discover mathematical theorems in an area of Economics known as "ranking sets of objects".

Economists, who have systematically worked on this topic since the 1980's, have formulated general principles, so-called axioms, for modelling the behaviour of rational decision makers with known preferences over individual objects who get asked to choose between two sets of such objects. For example, a risk-averse decision maker who prefers wine, to beer, to milk for her lunch should prefer being served beer with certainty to facing the uncertain prospect of getting either wine or milk. Or, to mention a second example, a decision maker preferring wine to beer whose behaviour is consistent with the so-called independence axiom should also prefer uncertainty between wine and milk to uncertainty between beer and milk (so, your preferences should be independent of adding an additional outside option on both sides). A third example is the dominance axiom, according to which adding a strictly worse option always makes things worse: you should prefer uncertainty between wine and beer to uncertainty between all three beverages.

The seminal result in the field, a theorem by mathematician Yakar Kannai and economist Bezalel Peleg that got published in 1984, shows that---against all intuition---it is in fact a mathematical impossibility for a decision maker's rational preferences to satisfy both the independence axiom and the dominance axiom when there are six or more objects to choose between. Only a relatively small number of similar impossibility theorems were known before 2010.

The methodology for automatically discovering such theorems developed in the award-winning paper has three components. First, the authors devised a formal language for writing down many of the axioms proposed in the Economics literature in a uniform manner. This formal language is a so-called many-sorted first-order logic. Using techniques from model theory, they were able to prove a general result saying that, if all axioms considered are of a certain syntactic form, then any impossibility found for a specific number of objects always generalises to an impossibility for an even larger number of objects. This means that the task of proving general impossibility theorems reduces to the much simpler task of proving such theorems for specific numbers of objects (such as the six objects featuring in the Kannai-Peleg Theorem). Second, for concrete (and small) numbers of objects, they showed that it is possible to translate axioms expressed in the general but very unwieldy many-sorted first-order logic into the much more restrictive but manageable classical propositional logic. For the latter logic, very powerful tools, so-called SAT-solvers, are available to automatically check the logical consistency of a given set of formulas. Now any inconsistency spotted by a SAT-solver corresponds to a general impossibility theorem. Thus, the first two components together provide a method for verifying known theorems. Third, the authors devised an algorithm for systematically searching through all possible combinations of axioms from a given set, to be able to automatically discover and prove new theorems.

When applied to a space of 20 axioms from the Economics literature, after a night of heavy computation on the Dutch national compute cluster Lisa, this methodology yielded a total of 84 impossibility theorems, including both known and nontrivial new results. Amongst the known results re-discovered in this manner is the Kannai-Peleg Theorem. Amongst the new ones is an impossibility theorem for a combination of axioms that, for a few years around the turn of the century, were wrongly believed to lead to a possibility result.

For further information, visit http://jair.org/bestpaper.html or contact Ulle Endriss <ulle.endriss at uva.nl>.