Holographic proofs: keeping computers and mathematicians honest

Science News, June 6, 1992 by Ivars Peterson

In contrast, result checking provides a way of determining whether a program, given a certain input, produces the correct answer for that particular input. Conceptually, the process isn't very different from the high-school exercise of substituting a calculated answer back into the original equation to check that the answer is correct.

"The principal idea here is that it's possible to get a program to convince you that the answer it gave you is correct," Blum says. "What you're interested in is either knowing that there's an error somewhere, in which case you would debug the program, or getting strong, convincing evidence that the particular answer you got from the program is correct, even though the program itself may contain bugs."

Blum illustrates his method with the example of determining whether two apparently dissimilar graphs -- sets of points, or nodes, connected to one another by lines to form networks -- are really the same. One such graph may represent, for example, the electrical properties of a circuit and another the related pattern of connections fabricated in a silicon chip.

Using a standard, off-the-shelf computer program, an engineer can ask whether the two graphs are really the same. But is the "yes" or "no" answer computed by the program correct?

If the two graphs really are the same, a checker has a standard, well-known method for confirming a "yes" answer. If the answer is "no," then the checker can trick an erroneous program into revealing that it has no good reason for its wrong answer. The checker feeds the program the first of the two graphs and either a new version of this graph - in which the nodes are randomly relabeled but the connections remain unchanged -- or a randomly relabeled version of the second graph.

If the program (and everything else, including the computer hardware) is functioning correctly, then it should give a "yes" answer whenever it sees the first graph paired with the relabeled version of the same graph and a "no" answer whenever it sees the first graph and a relabeled version of the second graph. Any other responses indicate that a fault lurks somewhere in the software or hardware.

In this case, because a checker presents one or the other of these alternative pairings randomly and repeats the process a few dozen times, the program has a negligible chance of "guessing" correctly and supplying the appropriate answer each and every time.

"There is a chance that the program can fool this checker, but the chances of doing so are extremely small," Blum says.

On a small scale, Blum already uses such a scheme for routinely checking the output of a calculator program designed to perform certain kinds of arithmetic useful in crytography. On one occasion, long after he had forgotten his software checker was there working in the background, Blum heard a signal indicating the checker had found a problem.

Although the program handled many pairs of 10-digit numbers successfully, there was a particular pair on which it failed. It turned out that the person who had written the original calculator program had inadvertently introduced a bug that became evident only under very special circumstances.