The ForMaRE Project

Formal Mathematical Reasoning in Economics

http://cs.bham.ac.uk/research/projects/formare/  
• Manfred Kerber (School of Computer Science; Principal Investigator)
• Colin Rowat (Department of Economics; Investigator)
• Christoph Lange (School of Computer Science; Research Fellow)

The ForMaRE project applies for mal ma thematical reasoning to economics. We seek to increase confidence in economics' theoretical results, to aid in discovering new results, and to foster interest in formal methods, i.e. computer-aided reasoning, within economics. To formal methods, we seek to contribute new challenge problems and user experience feedback from new audiences. Particular areas of interest are auctions, where we are building a toolbox of reusable formalisations, as well as matching and financial risk management. In parallel to connecting economics and formal methods by research, we organise events and provide infrastructure to connect both communities, from fostering mutual awareness to targeted matchmaking.

Motivation

Theoretical economics draws on a wide range of mathematics to explore and prove properties of stylised economic environments. Proofs are error-prone, since typically for any new set of axioms humans have initially no or only limited intuition. One easily assumes false theorems or overlooks cases in proofs. In proofs that occur in practice, not all details are given, hidden assumptions may be overlooked, proof steps may be incorrect, generalisations may not hold. Thus, any mathematical discipline, including theoretical economics, can benefit from formalising proofs and verifying them using computer support, since this will make them much more reliable. Other potential benefits include easier reuse of proof efforts in experimentation. Furthermore, experiments with the computational content of theorems become possible, which would be time-consuming and error-prone without computer support. Formal methods have been applied to economics before, most prominently to social choice theory and game theory, however, almost exclusively by computer scientists, not by economists.

The ForMaRE Strategy

The 3-year EPSRC-funded ForMaRE project, kicked off by the authors in May 2012 and further advised by more than a dozen of external computer scientists and economist collaborators, seeks to foster interest in formal methods within economics. Our strategy consists in using formalisation technology to establish new results, building trust in it, and enabling economists to use it themselves.

We have not yet established new results but, for auctions, have verified old, well-known ones, as well as taken a closer look at details that tend to be overlooked on paper but make a difference in ensuring correct operation of economics software. In consultation with experts in the fields of auctions, matching and finance, we have defined further research goals:

• Auctions are widely used for allocating goods and services. Our adviser Peter Cramton (consultant and professor at the University of Maryland, USA) has designed auctions for allocating new top-level Internet domains. Even basic properties of such complex auctions, e.g. the expected revenue, are difficult to establish.
• Matching problems occur, e.g., in organ donation. M. Utku Ünver (professor at Boston College, USA) is one of the founders of the New England Program for Kidney Exchange and has advised the Boston school authorities on matching children to schools. Impossibility results are of particular interest here, i.e. finding examples that prove that for a given combination of desirable properties (such as fairness or efficiency) no matching mechanism exists that satisfies all of them.
• Finance relies on models to price assets or to compute risk, but banks and regulators still validate and check such models manually. One research challenge, introduced to us by Neels Vosloo of the Bank of England, is to develop minimal test portfolios to ensure that capital models incorporate relevant risk factors.

Contemporary economists still prove their theorems using pen and paper. While we aim at establishing new results to showcase the potential of formal methods, we also seek to establish confidence in formal methods within the economics community. Thus, as a first step, we have demonstrated the reliability of formal methods by re-establishing known results. We have started to formalise the review of a canonical auction theory textbook by Paul Milgrom in four theorem proving systems in parallel, collaborating with their developers or expert users.

Ultimately we aim at enabling economists to formalise their own designs and validate them themselves, or at least to train specialists beyond the core computer-aided reasoning community, who will assist economists with formalisation – just like lawyers assist with legal issues. To overcome the adoption barrier of formal methods, we will provide guides and toolboxes of ready-to-reuse formalisations of basic concepts in selected fields, starting with auctions. This means identifying rich but learnable languages for formal knowledge representation, as well as powerful but user-friendly theorem proving software.

Building, connecting, and serving communities

Our community building efforts include invited lectures and tutorials at computer science and economics venues. We aim at making developers and users of computer-aided reasoning systems aware of 1) new, challenging problems in the application domain of economics, of 2) new target audiences, and thus of 3) the need to enhance the systems' usability and documentation. Our message to economists, e.g. at the 2012 summer school of the Initiative for Computational Economics (ICE), is that there is a wide range of tools to assist with reliably solving relevant problems in economics. Technical infrastructure to support our outreach work includes a discussion mailing list and a community website to collect pointers to existing formalisations of theorems, models and theories in economics.

Finally, we are reaching out to further application domains beyond economics. At the 2013 convention of the UK Society for the Study of Artificial Intelligence and Simulation of Behaviour (AISB), we ran a symposium on enabling domain experts to use formalised reasoning. In a specially designed review process we had identified matches between domain problems (“nails”) and software (“hammers”) and pointed these out to the authors. We are committed to continuing our matchmaking efforts and community-bridging research as to utilise the full potential of computers in real-world applications, beyond mere computation and data processing.