[FOM] Talk on Formal Verification

[Mario Carneiro]

On Sat, Jan 30, 2016 at 2:05 PM, Ben Sherman <sherman at csail.mit.edu> wrote:

> I think it's important to distinguish between computation required for
> proof search and computation required for proof checking. While I can
> imagine using lots of computation for proof search, I doubt that the
> verification of any "good" proof of a "major theorem" should require
> excessive computation (not including dependencies).
>

To me this is a major flaw in Flyspeck (which I might have the opportunity
to rectify in my lifetime) - it takes too long to run. My personal views
are probably nonstandard in this regard, but I would spend 100 times the
computation to cut down the size of a formal proof by half (since the
one-time cost will eventually pay dividends in later re-verifications).


> The checkers example is also interesting in that it should be a relatively
> short formal proof that requires a lot of computation to check. Which of
> these two metrics, generally, should we aim to minimize?
>

This sounds like a contradiction. If it requires a lot of computation, then
in what sense is the proof short? If you are merely measuring the length of
a program which generates the proof proper (the sequence of steps that are
followed in some axiomatic framework), then that's no measure at all: many,
if not all, formal systems have r.e. proofs, so I can easily write a tiny
program that finds proofs for any provable statement. Obviously it won't be
practical, but at least this shows that as a measure of proof complexity it
is not very well-defined.

I would advocate for the measure of interest being the number of steps in
the formal proof. For a sensible definition of "step" (which in particular
allows the definition and reuse of theorems), this will be proportional to
the run time of a proof verification software, as well as being roughly
proportional (for large n) to the amount of text in an informal proof, and
the amount of effort needed for a human to understand the proof.

One unfortunate side effect of high-automation languages like HOL Light or
Coq is that users are naturally driven, by the nature of text-based input,
to minimize the number of characters they write (as a first-order
approximation), provided that the proofs that are generated take a
"reasonable time" to be discovered. The problem here is that "reasonable
time" is defined on a human scale, so probably in the order of seconds to
minutes, but this applies separately to each proof program that is written,
so a large composite proof like Flyspeck, involving tens of thousands of
these "reasonable times" adds up to something quite unreasonable. If a
little extra in the way of search hints was stored, this could doubtless be
cut down considerably. There is a tradeoff between storage space and
verification time here, but I think it is clear which resource is in
shorter supply right now.


> Tim, perhaps I don't understand what you mean by a (computerized)
> semiformal proof. What springs to mind for me is, for example, a tactic
> script in Coq, which can indeed require far more computation to run
> (generate the formal proof term) than to check the formal term it
> generates. But many tactics (particularly the time-consuming ones) are more
> proof-search commands than proofs. In principle, one could replace the
> proof-search commands with the proof terms that are actually found, and
> arrive at a proof that is both quicker to run and more explanatory. In my
> mind, a semiformal proof is a document which explains to a human why a
> theorem is true, so I fail to see how computation would play a major role.
>

To draw an analogy, the difficulty of a theorem is probably not
well-measured by giving the statement to an undergraduate and seeing how
long it takes him to find a solution. Such a measure is strongly biased by
the capacity of the individual student, and additionally counts all sorts
of dead-ends discovered along the way. Much better would be to get the
whole class together, work on a nice and clean proof, and record that in
the textbook instead.

Mario
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20160130/53f18667/attachment.html>