Holographic proofs: keeping computers and mathematicians honest

Science News, June 6, 1992 by Ivars Peterson

The "clique" problem, in which one has to find -- given a long list of people and their friendships - the largest group of people in which everyone in the group likes everyone else in the group, represents a typical example. Computer scientists have proved that a variety of other important problems that involve searching for optimal strategies in the face of a large number of choices or possibilities have the same level of difficulty.

Formulated by Lund, Szegedy, Rajeev Motwani of Stanford University, and Sanjeev Arora and Madhu Sudan, both students at Berkeley, the latest result proves that for a significant group of such hard optimization problems, one cannot guarantee finding even an approximate answer within a reasonable time. For these cases, it's no easier to find approximate solutions than to find the exact answers.

"This [result] doesn't help you do anything. It doesn't give you a new algorithm to do something faster," says David S. Johnson of Bell Labs. "It helps you by telling you what you can do and what you cannot expect to do."

"What's exciting is that you get [insights] relevant to real-world problems... out of highly theoretical, flights-of-fancy considerations," he adds.

After the breath-taking ride of recent years from one surprising insight to another, computer scientists still face a host of unanswered questions. The latest results on the difficulty of efficiently arriving at approximate solutions apply to only a portion of the hard optimization problems that computer scientists face in handling everything from airline schedules to telephone networks. It still leaves the feasibility and efficiency of many approaches unresolved.

At the same time, computer scientists are exploring what it would take to convert properly expressed mathematical proofs or computations into a transparent, or holographic, form. One difficulty stems from the great length of the transparent proof that one would typically obtain from a given formalized proof.

"We are trying to reduce that size, and once we reduce it to a reasonable level, one would hope that practical applications could be found," Babai says.

Anyone hoping to apply this technique to a real mathematical proof, written initially in a human language, would have to find a way of translating it into a formal language based explicitly on the rules of logic. Only then could the proof be transformed into its transparent guise. At the same time, checking that a large computer system is doing what it's supposed to do is limited by the difficulty of accurately specifying a program's or computer system's objectives.

More immediate practical benefits may lie in the application of Blum's program-checking schemes to computer calculations. With such methods, even in bug-infested computer systems, one can obtain an ironclad guarantee that particular answers are really correct.