We consider problems originating in economics that may be solved automatically using mathematical software. We present and make freely available a new benchmark set of such problems. The problems have been shown to fall within the framework of non-linear real arithmetic, and so are in theory soluble via Quanti er Elimination (QE) technology as usually implemented in computer algebra systems. Further, they all can be phrased in prenex normal form with only existential quanti ers and so are also admissible to those Satis ability Module Theory (SMT) solvers that support the QF_NRA logic. There is a great body of work considering QE and SMT application in science and engineering, but we demonstrate here that there is potential for this technology also in the social sciences.
1.1
A general task in economic reasoning is to determine whether, with variables v = (v1; : : : ; vn), the hypotheses H(v) follow from the assumptions A(v), i.e. is it the case that :9v[A ^ :H]
True Contradictory Assumptions 9v[A ^ :H]
Mixed False
We categorise the situation into four possibilities that are of interest to an economist (Table 1) via the outcome of a pair of fully existentially quanti ed statements which check the existence of both an example (9v[A ^ H]) and counterexample (9v[A^:H]) of the theorem. So we see that every economics theorem generates a pair of SAT problems, in practice actually a trio since we would rst perform the cheaper check of the compatibility of the assumptions (9v[A]).
Such a categorisation is valuable to an economist. They may gain a proof of their theorem, but if not they still have important information to guide their research: knowledge that their assumptions contradict; or information about fv : A(v) ) H(v)g:
Also of great value to an economist are the options for exploration that such technology would provide. An economist could vary the question by strengthening the assumptions that led to a Mixed result in search of a True theorem. However, of equal interest would be to weaken the assumption that generated a True result for the purpose of identifying a theorem that can be applied more widely. Such weakening or strengthening is implemented by quantifying more or less of the variables in v. For example, we might partition v as v1; v2 and ask for fv1 : 8v2 : A(v1; v2) ) H(v1; v2)g. The result in these cases would be a formula in the free variables that weakens or strengthens the assumptions as appropriate. 1.2
Technology to solve such problems automatically Such problems all fall within the framework of Quanti er Elimination (QE). QE refers to the generation of an equivalent quanti er free formula from one that contains quanti ers. SAT problems are thus a sub-case of QE when all variables are existentially quanti ed.
QE is known to be possible over real closed elds (real QE) thanks to the
seminal work of Tarski [
The economics problems identi ed all fall within the framework of QE over
the reals. Further, the core economics problem of checking a theorem can be
answered via fully existentially quanti ed QE problems, and so also soluble using
the technology of Satis ability Modulo Theory (SMT) Solvers; at least those that
support the QF_NRA (Quanti er Free Non-Linear Real Arithmetic) logic such as
SMT-RAT [
QE has found many applications within engineering and the life sciences. Recent
examples include the derivation of optimal numerical schemes [
Similarly, for SMT with non-linear reals, applications seem focussed on other
areas of computer science. The original nlsat benchmark set [
The reader may wonder why QE has not been used in economics previously.
On a few occasions when QE algorithms have been mentioned in economics they
have been characterized as \something that is do-able in principle, but not by any
computer that you and I are ever likely to see" [
Availability and further details The benchmark set consists of 45 potential economic theorems. Each theorem requires the three QE/SMT calls to check the compatibility of assumptions, the existence of an example, and the existence of a counterexample, so 135 problems in total. In all cases the assumption and example checks are SAT, in fact often fully satis ed (any point can witness it) as they relate to a true theorem. Correspondingly, the counterexample is usually UNSAT (for 42/45 theorems) and thus the more di cult problem from the SMT point of view.
The benchmark problems are hosted on the Zenodo data repository at URL
https://doi.org/10.5281/zenodo.1226892 in both the SMT2 format and as
input les suitable for Redlog and Maple. The SMT2 les have been accepted
into the SMT-LIB [
Available from http://examples.economicreasoning.com/ are Mathematica notebooks5 which contain commands to solve the examples in Mathematica and also further information on the economic background: meaning of variable names and economic implications of results etc. 5 A Mathematica licence is needed to run them, but static pdf print outs are also available to download.
Plan The paper proceeds as follows. In Section 2 we describe in detail some examples from economics, ranging from textbook examples common in education to questions arising from current research discussions. Then in Section 3 we o er some statistics on the logical and algebraic structure of these examples. We then give some nal thoughts on future and ongoing work in Section 4. 2
Examples of Economic Reasoning in Tarski's Algebra The elds of economics ranging from macroeconomics to industrial organization to labour economics to econometrics involve deducing conclusions from assumptions or observations. Will a corporate tax cut cause workers to get paid more? Will a wage regulation reduce income inequality? Under what conditions will political candidates cater to the median voter? We detail in this section a variety of such examples. 2.1
Comparative static analysis
We start with Alfred Marshall's [
One way to express his reasoning in Tarski's framework is to look at the industry's local comparative statics: meaning a comparison of two di erent equilibrium states between supply and demand. With a downward supply shift represented as da > 0 (where a is a reduction in costs) we have here:
A H
D0(q) < 0 ^ S0(q) > 0
d ^ da S(q) dq dp da > 0 ^ da < 0
dp dp a = da ^ da d da =
D(q) where: { D0(q) is the slope of the inverse demand curve in the neighborhood of the industry equilibrium; { S0(q) is the slope of the inverse supply curve;
dq { is the quantity impact of the cost reduction; and da dp { is the price impact of the cost reduction.
da Economically, the rst atoms of A are the usual slope conditions: that demand slopes down and supply slopes up. The last two atoms of A say that the cost change moves the industry from one equilibrium to another. Marshall's hypothesis was that the result is a greater quantity traded at a lesser price.
Hence we set the \variables" v to be four real numbers (v1; v2; v3; v4): v =
D0(q); S0(q); dq dp
; da da : Then, after applying the chain rule, A and H may be understood as Boolean combinations of polynomial equalities and inequalities:
A H v1 < 0 ^ v2 > 0 ^ v3v2
1 = v4 ^ v4 = v3v1; v3 > 0 ^ v4 < 0: Thus Marshall's reasoning ts in the Tarski framework and therefore is amenable to automatic solution. Any of the tools mentioned in the introduction can easily evaluate the two existential problems for Table 1 and conclude easily that 8v : A ) H is True, con rming Marshall's conclusion.
In fact, for this example it is straightforward to produce a short hand proof in a couple of lines6 and so we did not include it in the benchmark set. But it demonstrates the basic approach to placing economics reasoning into a form admissible for QE/SMT tools. A similar approach is used for many of the larger examples forming the benchmark set, such as the next one. 2.2
Scenario analysis Economics is replete with \what if ?" questions. Such questions are logically and algebraically more complicated, and thereby susceptible to human error, because they require tracking various scenarios. We consider now one such question originating from recent economic debate.
Writing at nytimes.com7, Economics Nobel laureate Paul Krugman asserted that whenever taxes on labour supply are primarily responsible for a recession, then wages increase. Two scenarios are discussed here: what actually happens (act) when taxes (t) and demand forces (a) together create a recession, and what would have happened (hyp) if taxes on labour supply had been the only factor a ecting the labour market. 6 Subtract the nal assumption from the penultimate one and then apply the sign conditions of the other assumptions to conclude v3 > 0. Then with this the last assumption provides the other hypothesis, v4 < 0. 7 https://krugman.blogs.nytimes.com/2012/11/03/soup-kitchens-caused-thegreat-depression/ Expressed logically we have:
A H < 0 ^ = 1 ^ d ^ dact D(w; a) = q = S(w; t)
d ^ dhyp D(w; a) = q = S(w; t)
dt dt da ^ dact = dhyp ^ dhyp = 0
dq 1 dq ^ dhyp < 2 dact < 0 dw
> 0: dact In economics terms, the rst line of assumptions contains the usual slope restrictions on the supply and demand curves. Because nothing is asserted about the units of a or t, the next line just contains normalizations. The third and fourth lines say that each scenario involves moving the labour market from one equilibrium (at the beginning of a recession) to another (at the end of a recession). The fth line de nes the scenarios: both have the same tax change but only the act scenario has a demand shift. The nal assumption / assertion is that a majority of the reduction in the quantity q of labour was due to supply (that is, most of dq dact would have occurred without any shift in demand). The hypothesis is that wages w are higher at the end of the recession than they were at the beginning.
Viewed as a Tarski formula this has twelve variables, v = ; each of which is a real number representing a partial derivative describing the supply and demand function or a total derivative indicating a change over time within a scenario.
An analysis of the two existential problems as suggested in Section 1.1. shows that the result is Mixed: that is both examples and counterexamples exist. In particular, even when all of the assumptions are satis ed, it is possible that wages actually go down.
Moreover, if @D(w;a) and @S(w;t) are left as free variables, a QE analysis
@w @w
recovers a disjunction of three quanti er-free formulae. Two of them contradict
the assumptions, but the third does not and can therefore be added to A in
order to guarantee the truth of H:
> 0:
I.e. assuming that labour supply is at least as sensitive to wages as labour demand
is (recall that the demand slope is a negative number) guarantees that wages w
are higher at the end of the recession that is primarily due to taxes on labour
supply. See also [
This example can be found in the benchmark set as Model #0013. 2.3
Vector summaries
Economics problems sometimes involve an unspeci ed (and presumably large)
number of variables. Take Sir John Hicks' analysis of household decisions among
a large number N of goods and services [
We assume that when prices are p (p^), the household makes purchases q (q^), respectively:8
A (p q p q^) ^ (p^ q^ p^ q): Hicks asserted that the quantity impact of the price changes q^ positively correlated with the price changes p^ p: q cannot be H (q^ q) (p^ p) 0: Hicks' reasoning depends only on the value of vector dot products, four of which appear above, rather than the actual vectors themselves whose length remains unspeci ed.
Hicks implicitly assumed that prices and quantities are real valued, which places additional restrictions on the dot products. We need then to restrict that the symmetric Gram matrix corresponding to the four vectors q^; q; p^; p be positive semi-de nite. To state this restriction we then need to increase the list of variables from the four dot products that appear in A and H to all ten that it is possible to produce with four vectors.
QE technology certi es that there are no values for the dot products that can simultaneously satisfy A and contradict H. It follows that Sir John Hicks was correct regardless of the length N of the price and quantity vectors. In fact, further, it turns out that the additional restriction to real valued quantities is not needed for this example (there are no counter-examples even without this). While those additional restrictions could hence be removed from the theorem we have left them in the statement in the benchmark set because (a) they would 8 The price change is compensated in the Hicksian sense, which means that q and q^ are the same in terms of results or \utility", so that the consumer compares them only on the basis of what they cost (dot product with prices). be standard restrictions an economist would work with and (b) it is not obvious that they are unnecessary before the analysis.
The above analysis could be performed easily with both Mathematica and Z3 but proved di cult for Redlog. We have yet to nd a variable ordering that leads to a result in reasonable time9. It is perhaps not surprising that a tool like Z3 excels in comparison to computer algebra here, since the problem has a large part of the logical statement irrelevant to its truth: the search based SAT algorithms are explicitly designed to avoid considering this.
This example can be found in the benchmark set as Model #0078. 2.4
Concave production function
Our nal example is adapted from the graduate-level microeconomics textbook
[
A v1v10 + v2v7 + v3v5 = 0 ^ v1v11 + v2v8 + v3v7 = 0 ^ v1v12 + v10v3 + v11v2 = 0
In disjunctive normal form (DNF) A ^ :H is a disjunction of seven clauses. Each atom of H, and therefore each clause of A ^ :H in DNF, corresponds to a principal minor of the production function's Hessian matrix. So the clauses in the DNF are A ^ v12 > 0; A ^ v5 > 0 ^ : : : in the same sequence used in H above. The existential quanti ers applied to A ^ :H can be distributed across the clauses to form seven smaller QE problems.
As of early 2018, Z3 could not determine whether the Tarski formula A ^ :H is satis able: it was left running for several days without producing a result or 9 Since the problem is fully existentially quanti ed we are free to use any ordering of the 10 variables; but there are 10! = 3; 628; 800 such orderings; so we have not tried them all. error message. For this problem virtual substitution techniques may be advantageous (note the degree in any one variable is at most two). Indeed, Redlog and Mathematica can resolve it quickly. The problem would certainly be difcult for CAD based tools (which underline the theory solver used by Z3 for such problems). For example, if we take only the rst clause of the disjunction (the one containing v12 > 0), then the Tarski formula has twelve polynomials in twelve variables, and just three CAD projections (using Brown's projection operator) to eliminate fv12; v11; v10g results in 200 unique polynomials with nine variables still remaining to eliminate!
We note that the problem has a lot of structure to exploit in regards to the sparse distribution of variables in atoms. One approach currently under investigation is to eliminate quanti ers incrementally, taking advantage of the repetitive structure of the sub-problems one uncovers this way (an approach that works on several other problems in the benchmark set). This will be the topic of a future paper.
This example can be found in the benchmark set as Model #0056. 3
Analysis of the Structure of Economics Benchmarks The examples collected for the benchmark set come from a variety of areas of economics. They were chosen for their importance in economic reasoning and their ability to be expressed in the Tarski framework, not on the basis of their computational complexity. The sentences tend to be signi cantly larger formulae than the initial examples described above. We summarise some statistics on the benchmarks. These statistics are generated for the 45 counterexample checks (9v[A ^ :H]) which are representative of the full 135 problems. 3.1
Logical size Presented in DNF the benchmarks have number of clauses ranging from 7 to 43 with a mean average of 18.5 and median of 18. Of course each clause can be a conjunction but this is fairly rare: the average number of literals in a clause is at most 1.5 in the dataset, with the average number of atoms in a formula only slightly more than the number of clauses at 19.3. 3.2
Algebraic size
The number of polynomials involved in the benchmarks varies from 7 to 43 with
both mean average of 19.2 and median average of 19. The number of variables
ranges from 8 to 101 with an mean average of 17.2 and median of 14. It is worth
noting that examples with this number of variables would rarely appear in the
QE literature, since many QE algorithms have complexity doubly exponential
in the number of variables [
Low degrees While the algebraic dimensions of these examples are large in comparison to the QE literature, their algebraic structure is usually less complex. In particular the degrees are strictly limited. The maximum total degree of a polynomial in a benchmark ranges from 2 to 7 with an average of 4.2. So although linear methods cannot help with any of these benchmarks the degrees do not rise far. The mean total degree of a polynomial in a benchmark is only 1.8 so the non-linearity while always present can be quite sparse.
However, of greater relevance to QE techniques is not total degree of a
polynomial but the maximum degree in any one variable: e.g. this controls the
number of potential roots of a polynomial and thus cell decompositions in a CAD
(with this degree becoming the base for the double exponent in the complexity
bound); see for example the complexity analysis in [
Plentiful useful side conditions With variables frequently multiplying each other in a sentence's polynomials, a potentially large number of polynomial singularities might be relevant to a QE procedure. However, we note that the benchmarks here will typically include sign conditions that in principle rule out the need to consider many such singularities. That is, these side conditions will often coincide with unrealistic economic interpretations that are excluded in the assumptions. Of course, the computational path of many algorithms may not necessarily exploit these currently without human guidance. 3.5
Sparse occurrence of variables For each sentence 9v[A ^ :H] (these are the computationally more challenging of the 135) we have formed a matrix of occurrences, with rows representing variables and columns representing polynomials. A matrix entry is one if and only if the variable appears in the polynomial, and zero otherwise. The average entry of all 45 occurrence matrices is 0.15. This sparsity indicates that the use of specialised methods or optimisations for sparse systems could be bene cial. 3.6
Variable orderings
Since the problems are fully existentially quanti ed we have a free choice of
variable ordering for the theory tools. It is well known that the ordering can
greatly a ect the performance of tools. A classic result in CAD presents a class
of problems in which one variable ordering gave output of double exponential
complexity in the number of variables and another output of a constant size
[
We have presented a dataset of examples from economic reasoning suitable for automatic solution by QE or SMT technology. These clearly broaden the application domains present in the relevant category of the SMT-LIB, and the literature of QE. Further, their logical and algebraic structure are sources of additional diversity.
While some examples can be solved easily there are others that prove challenging to the various tools on o er. The example in Section 2.3 could not be tackled by Redlog while the one in Section 2.4 caused problems for Z3. Of the tools we tried, only Mathematica was able to decide all problems in the benchmark set. However, in terms of median average timing over the benchmark set Mathematica takes longer with 825ms than Redlog (50ms) or Z3 (< 15ms). 4.2
Ongoing and future work As noted at the end of Section 2, some of these problems have a lot of structure to exploit and so the optimisation of existing QE tools for problems from economics is an ongoing area of work.
More broadly, we hope these benchmarks and examples will promote interest
from the Computer Science community in problems from the social sciences, and
correspondingly, that successful automated solution of these problems will
promote greater interest in the social sciences for such technology. A key barrier to
the latter is the learning curve that technology like Computer Algebra Systems
and SMT solvers has, particularly to users from outside Mathematics and
Computer Science. In [