Communications of the ACM

ing of spheres is the densest possible. This proof, in addition to involving extensive case enumerations at different levels, is also very complicated in the interaction between the various parts. In August 2014, a team headed by Hales announced the completion of the Flyspeck project, constructing a formal proof of Kepler’s conjecture. 16 Yet another example is the proof by Tucker30 for Lorenz’s conjecture ( number 14 in Smale’s list of challenging problems for the 21st century). The conjecture states that Lorenz’s system of three differential equations, providing a model for atmospheric convection, supports a strange attractor. Tucker (page 104) 30 described the run of a parallel ODE solver several times on different computer setups, obtaining similar results.

Certified Computation. This technique is based on the idea it may be easier to check a given answer for correctness than come up with such an answer from scratch. The prototype example is the solution of an equation like 3x3 − 4x2 − 5x + 2 = 0. While it may be a challenge to find the solution x = 2, it is straightforward to substitute the solution into the equation and check whether it is fulfilled. The result is trustworthy not because it is accompanied by a formal proof but because it is so simple to check, much simpler than the algorithm (perhaps Newton iteration in this case) used to solve the problem in the first place. In addition to the solution itself, it may be required that a certifying algorithm provide a certificate in order to facilitate the checking procedure. 25 Developing such certificates and computing them without excessive overhead may require algorithmic innovations (see the first sidebar “Certified Computations”).

In our case, the result computed by our program can be interpreted as the eigenvalue of a giant matrix Q, which is not explicitly stored but implicitly defined through an iteration procedure. The certificate is a vector v that is a good-enough approximation of the corresponding eigenvector. From this vector, one can compute certified bounds on the eigenvalue in a rather straightforward way by comparing the vector v to the product Qv.

These two approaches comple-
ment each other; a simpler check-
ing procedure is more amenable to a
formal proof and verification proce-
dure. However, we did not go to such
lengths; a formal verification of the
program would have made sense only
in the context of a full verification that
includes also the human-readable
parts of the proof. We instead used
traditional methods of ensuring pro-
gram correctness of the certificate-
checking program.

Twisted Cylinders

A “twisted cylinder” is a half-infinite wraparound spiral-like square lattice (see Figure 3). We denote the perim-

A certifying algorithm not only produces the result but also justifies its correctness by supplying a certificate that makes it easy to check the result. In contrast with formally verified computation, correctness is established for a particular instance of the problem and a concrete result. Here, we illustrate this concept with a few examples; see the survey by McConnell et al. 25 for a thorough treatment.

The greatest common divisor. The greatest common divisor of two numbers can be found through the ancient Euclidean algorithm. For example, the greatest common divisor of 880215 and 244035 is 15. Checking that 15 is indeed a common divisor is rather easy, but not clear is that 15 is the greatest. Luckily, the “extended” Euclidean algorithm provides a certificate: two integers p = −7571 and q = 27308, such that

880215p + 244035q = 15. This proves any common divisor of 880215 and 244035 must divide 15. No number greater than 15 can thus divide 880215 and 244035.

Systems of linear equations and inequalities. Consider the three equations 4x − 3y

+ z = 2, 3x − y + z = 3, and x − 7y – z = 4 in three unknowns x, y, z. It is straightforward to verify any proposed solution; however, the equations have no solution. Multiplying them by 4, − 5, − 1, respectively, and adding them up leads to the contradiction 0 = − 11.

The three multipliers thus provide an easy-to-check certificate for the answer. Such multipliers can always be found for an unsolvable linear system and can be computed as a by-product of the usual solution algorithms. A well-known extension of this example is linear programming, the optimization of a linear objective function subject to linear equations and inequalities, where an optimality certificate is provided by the dual solution.

Testing a graph for 3-connectedness. Certifying that a graph is not 3-connected is straightforward. The certificate consists of two vertices whose removal disconnects the graph into several pieces. It has been known since 1973 that a graph can be tested for

3-connectedness in linear time, 17 but all algorithms for this task are complicated. While providing a certificate in the negative case is easy, defining an easy-to-check certificate in the positive case and finding such a certificate in linear time has required graph-theoretic and algorithmic innovations. 28 This example illustrates that certifiability is not primarily an issue of running time. All algorithms, for constructing, as well as for checking, the certificate, run in linear time, just like classical non-certifying algorithms. The crucial distinction is that the short certificate-checking program is by far simpler than the construction algorithm.

Comparison with the class NP. There is some analogy between a certifying algorithm and the complexity class NP. For membership in NP, it is necessary only to have a certificate by which correctness of a solution can be checked in polynomial time. It does not matter how difficult it is to come up with the solution and find the certificate. In contrast with a certifying algorithm, the criterion for the checker is not simplicity but more clear-cut—running time. Another difference is that only “positive” answers to the problem need to be certified.