Polya

A "natural" automated procedure for reasoning with inequalities

Rob Lewis

4/22/2014

Outline

  1. Automated vs. interactive theorem proving
  2. Decision procedures for real closed fields
  3. My project: an alternative approach
  4. Some philosophical comments

Why do we want computers to do math at all?

  • They're accurate!
  • They're fast!
  • They can "comprehend huge problems" (in a certain sense).
  • They can (sometimes) produce formal proofs.
  • A standardized proof library is extremely useful.
  • The math behind mechanized reasoning is interesting in its own right.

Automated and Interactive Theorem Proving

In automated reasoning, the computer attempts to solve a problem on its own, without input.

Examples: calculators, SAT solvers for boolean formulae


>>> s = Solver()
>>> s.add(Implies(p, q))
>>> s.add(Implies(q, r))
>>> s.add(p)
>>> s.add(Not(r))
>>> s.check()
unsat

					

Automated and Interactive Theorem Proving

In interactive theorem proving, the user gives "hints," and the computer fills in the gaps.

Examples: formalizations of prime number theorem, Kepler conjecture, homotopy type theory

These proofs often involve calls to automated tools.


                        
theorem succ_le_succ {a b : Nat} (H : a + 1 ≤ b + 1) : a ≤ b
:=
  obtain (x : Nat) (Hx : a + 1 + x = b + 1), from lt_elim H,
  have H2 : a + x + 1 = b + 1, from (calc
    a + x + 1 = a + (x + 1) : add_assoc _ _ _
          ... = a + (1 + x) : { add_comm x 1 }
          ... = a + 1 + x : symm (add_assoc _ _ _)
          ... = b + 1 : Hx),
  have H3 : a + x = b, from (succ_inj H2),
  show a ≤ b, from (le_intro H3)
					

Automated and Interactive Theorem Proving

My project sits near the intersection of these paradigms. It is an automated tool for a specific domain of problems, that frequently show up in interactive proofs.

Real Closed Fields

If $0 < x < 1$ and $\ 0 < y < 1$, then $$ x^{500} + y^{500} > x^{500} \cdot y^{500} $$

This is a theorem in the theory of real closed fields: we are allowed constants $0$ and $1$, operations $+$ and $\cdot$, and repeated applications of these operations, and make comparisons using $>$ and $=$.

Real Closed Fields

If $0 < x < 1$ and $\ 0 < y < 1$, then $$ x^{500} + y^{500} > x^{500} \cdot y^{500} $$

The theory of real closed fields is decidable: there is an algorithm that, given any sentence of this form, will determine whether it is provable or not. (Tarski, 1951)

But this algorithm is extremely inefficient! Its complexity doesn't correspond to any "intuitive" notion of difficulty.

And producing a proof certificate is even less efficient, by many orders of magnitude.

Real Closed Fields

If $0 < f(z) < 1$ for all $z$, then $$ f(x)^{500} + f(y)^{500} > f(x)^{500} \cdot f(y)^{500} $$

It is also broken by any changes to the underlying language.

Real Closed Fields

These shortcomings are disappointing:

  • Heterogeneous problems in (simple extensions of) RCF are quite common across many fields of mathematics.
  • They can be quite tedious to solve "manually" in interactive provers.

... and surprising:

  • Restricted to just addition (or just multiplication), the theory becomes quite simple.
  • Extensions of the language of RCF do not necessarily create structurally different terms.

Heuristics for Real Closed Fields

If we accept the possibility that we will "overlook" proofs that depend essentially on distributivity, we can fix a number of these shortcomings, and get:

  • Massive improvements in efficiency on a large class of problems
  • Complexity that respects an "intuitive" idea of difficulty
  • Easily constructible (and natural!) proof certificates
  • Flexibility and extensibility

We call something that does this a heuristic procedure.

Introducing: Polya


George Polya, known for his research in both problem-solving heuristics and in inequalities.

Polya: An Outline

Polya consists of a collection of individualized "modules" that communicate with a central database. The database stores information in a shared language.

Polya: An Outline

Given a collection of inequalities, Polya searches for a contradiction by the following steps:

  1. Convert each inequality into a standard normal form.
  2. Find all additive and multiplicative subterms and give them names.
  3. Iteratively run modules for additive and multiplicative arithmetic, to learn comparisons between these subterms.
  4. If the central database receives contradictory information, return "unsat".


Note: in classical logic, this is equivalent to proving a theorem from hypotheses.

Normal Forms and Named Subterms

$$y\cdot x \cdot x + \frac{1}{5}\cdot y^3\cdot z \cdot 5 \cdot x \cdot z < -x $$ becomes

$$\underbrace{\underbrace{x^2\cdot y}_{t_1} + \underbrace{x\cdot y^3\cdot z^2}_{t_2} + \underbrace{x}_{t_3}}_{t_4} < 0$$

Note that a comparison like $t_4 < 0$ is both additive and multiplicative!

Arithmetical Modules

If we take a set of purely additive (or multiplicative) equations and/or comparisons, we can use variable elimination to find new comparisons in the common language.

$$ t_3 + t_8 < t_5 \wedge t_3 > 0 \implies t_8 < t_5 $$

$$ t_9 = 3\cdot t_1^2 \wedge 0 < t_1 < 1 \implies t_9 < 3 $$

Arithmetical Modules

There are multiple ways to do this:

  • Fourier-Motzkin variable elimination: simple, but can "blow up" in difficult cases
  • Geometric methods: potentially better bounds on complexity, but more complicated

Additive Fourier-Motzkin Elimination

Our goal: given a list of additive equalities and inequalities involving variables $t_i$ for $1\leq i \leq n$, find the strongest derivable comparisons between each pair $(t_k, t_l)$.

Suppose the following: \begin{align*} t_1 &< 3t_4 + t_7 \\ t_4 &< t_7 - 2t_5 \\ t_7 &< 8t_0 \\ t_7 &< -t_3 \\ 3t_5 &= 2t_1 + 2t_4 \end{align*}

We want to find comparisons between $t_1$ and $t_4$, so let's eliminate $t_7$.

Additive Fourier-Motzkin Elimination

Our goal: given a list of additive equalities and inequalities involving variables $t_i$ for $1\leq i \leq n$, find the strongest derivable comparisons between each pair $(t_k, t_l)$.

First, rewrite everything so that $t_7$ is isolated: \begin{align*} t_1 - 3t_4 &< t_7 \\ t_4 + 2t_5 &< t_7 \\ t_7 &< 8t_0 \\ t_7 &< -t_3 \\ 3t_5 &= 2t_1 + 2t_4 \end{align*}

Additive Fourier-Motzkin Elimination

Our goal: given a list of additive equalities and inequalities involving variables $t_i$ for $1\leq i \leq n$, find the strongest derivable comparisons between each pair $(t_k, t_l)$.

Now, split into three categories:

$t_1 - 3t_4 < t_7$ $t_7 < 8t_0$ $3t_5 = 2t_1 + 2t_4 $
$t_4 + 2t_5 < t_7$ $t_7 < -t_3$

Additive Fourier-Motzkin Elimination

Our goal: given a list of additive equalities and inequalities involving variables $t_i$ for $1\leq i \leq n$, find the strongest derivable comparisons between each pair $(t_k, t_l)$.

For every pair of inequalities, one from the first category and one from the second, we derive a new inequality in the third:

$t_1 - 3t_4 < t_7$ $t_7 < 8t_0$ $3t_5 = 2t_1 + 2t_4 $
$t_4 + 2t_5 < t_7$ $t_7 < -t_3$ $t_1 - 3t_4$ $<$ $-t_3$

Additive Fourier-Motzkin Elimination

Our goal: given a list of additive equalities and inequalities involving variables $t_i$ for $1\leq i \leq n$, find the strongest derivable comparisons between each pair $(t_k, t_l)$.

We end up with the following set of inequalities, which are equisatisfiable to the original set: \begin{align*} t_1 - 3t_4 &< -t_3 \\ t_1 - 3t_4 &< 8t_0 \\ t_4 + 2t_5 &< -t_3 \\ t_4 + 2t_5 &< 8t_0 \\ 3t_5 &= 2t_1 + 2t_4 \end{align*}

Additive Fourier-Motzkin Elimination

Our goal: given a list of additive equalities and inequalities involving variables $t_i$ for $1\leq i \leq n$, find the strongest derivable comparisons between each pair $(t_k, t_l)$.

If we repeat this procedure to eliminate $t_0$, $t_3$, and $t_5$, we end up with \begin{align*} t_1 &> -\frac{2}{5}t_4 \\ t_1 &< -\frac{8}{3}t_4 \end{align*}

Multiplicative Fourier-Motzkin Elimination

The multiplicative version of this algorithm works very similarly, with one notable sticking point: we need to know (or assume) the signs of terms.


(This is because the logarithm function is only defined on positive reals!)

Geometric Variable Elimination

There are inefficiencies in the Fourier-Motzkin procedure that would be nice to avoid.

An improvement to this procedure can be seen by interpreting matters geometrically.

Geometric Variable Elimination

With respect to variables $t_1,\ldots, t_n$, an equation $c_1t_1 + \ldots c_n t_n = 0$ defines an $(n-1)$-dimensional hyperplane through the origin in $\mathbb{R}^n$.

An inequality $c_1t_1 + \ldots c_n t_n < 0$ defines a half-space in $\mathbb{R}^n$.

A collection of inequalities of this form determine a polytope (an "infinite pyramid") with vertex at the origin.

Geometric Variable Elimination

A polytope in $\mathbb{R}^3$ defined by three half-planes, emerging "out of" the screen.

Geometric Variable Elimination

We're interested in two dimensions at a time. So if we project the polytope to the $t_i t_j$ plane, we can read off the comparisons between $t_i$ and $t_j$ from the "shadow."

Geometric Variable Elimination

This projection is easy, if we convert the polytope to its vertex representation first.

But this conversion is hard!

In effect, converting the polytope to its V-rep does the entire Fourier-Motzkin routine at once, without (as much) redundancy.

But using external tools to do this is opaque, and it isn't entirely clear how to construct a proof certificate with this method.

Iterating Arithmetical Modules

No matter which arithmetical method we use, we derive the same facts about subterms of the original problem.

These facts lead us to an "unwinding" proof of the desired sentence, via simple inferences.

A contradiction is found when the modules find a subterm with inconsistent bounds: say, $t_5 > 3$ and $t_5 < 2$.

Modular Structure

$$ f(x)^{500} + f(y)^{500} > f(x)^{500} \cdot f(y)^{500} $$

The decentralized structure makes it simple to extend the procedure to new types of terms.

A sentence of this form is "comprehensible" almost by default.

Modular Structure

$$ f(x)^{500} + f(y)^{500} > f(x)^{500} \cdot f(y)^{500} $$

But we can do even more than comprehend it, by adding new modules.

Because of the architecture, new modules and new term structures can't interfere with the core arithmetical base.

Axiom Instantiation Module

One important module takes universal axioms from the user, of the form $$ (\forall x, y)(x < y \rightarrow f(x) < f(y)). $$

The module instantiates this axiom with respect to terms in the central database: if we have defined $t_3 = f(a)$ and $t_5=f(b)$, we will learn the clause $$a < b \to t_3 < t_5.$$

`

Axiom Instantiation Module

We want to avoid instantiating everything: if $f(a)$ doesn't show up in the problem, we shouldn't bother instantiating axioms that give information about $f(a)$.

But, we don't want to be too conservative: if $f(a)+f(b)$ is not a problem term, but $f(a)+f(b)+c$ is, an axiom that tells us about the former could be useful.

Axiom Instantiation Module

The solution: a balance, using trigger terms.

We'll allow the axioms to create new "terms of interest," as long as they're combinations of current terms in the problem.

This is, again, a heuristic!

Modular Structure

We have additional modules planned for:

  • Exponential and logarithmic functions:
  • $$e^{t_1 + t_2} = e^{t_1}e^{t_2}$$
  • Integer arithmetic:
  • $$int(z)\implies \lceil z \rceil = z$$
  • Second-order operators
  • $$f(x)>1 \implies \int_a^b f(x) > b-a$$

Where Is This Going?

We envision Polya as a complement to the standard automated methods available in interactive proof assistants.

There are some situations where the old methods are better, and some where ours is better!

Areas we can improve on:

  • Implementing proof certificates
  • Better case splitting and backtracking
  • More modules for more domains
  • More efficiency in general

Philosophical Questions

What counts as a mathematical proof?

Traditionally, a proof is something that convinces mathematicians of the truth of a statement.

Proof-theoretically, a proof is a sequence of valid inferences in a specified deductive system.

In between, a proof is something that convinces mathematicians that such a deduction is possible in principle.

Philosophical Questions

How do we recognize something as a mathematical proof?

  • Peer reviewers?
  • (Manual) formal deductions?
  • Computer-verified proofs?

Philosophical Questions

How do we recognize something as a formal deduction?

What does this say about the epistemic status of a proof-theoretic proof?

The End!