Manuel Blum - US grants

This proposal seeks to develop mathematical methods of computer science for the purpose of testing program correctness. The simpler but nevertheless nontrivial problem of deciding whether or not a given program on a given input outputs the correct answer will be investigated. Consider a program P that, while having been written to solve general instances of a certain problem, is actually run on just one or a few select instances. In this case, instead of proving the correctness of program P on all inputs, it suffices to prove that the output of P on the given few instances is correct (or to exhibit a bug in P). For example, suppose program P is supposed to decide if two graphs G and H are isomorphic. If P supplies the isomorphism, then it is easy to check that the isomorphism really works. Interestingly, the interactive proof for graph nonisomorphism serves to test the correctness of a program that asserts that G and H are not isomorphic. Given any program for graph isomorphism, this test procedure either gives quantifiable mathematical evidence that the program's answer is correct, or else it proves that the program has a bug. This raises the question: which computational problems (such as graph isomorphism) have the property that a program for the problem on any given input can be efficiently tested for correctness? Initial studies show that a large collection of programming problems drawn from block designs, graphs, codes, matrices over GF(q), latin squares, etc., can be tested by similar techniques. A useful natural (group theoretic) description of a broad class of computational problems, including those mentioned above, whose programs can be tested by such schemes is sought.

This research is concerned with a new idea for increasing the reliability of software, an idea that the principal investigator calls program result checking (or program answer checking). The idea is to design programs to check their work. As a rule, students in the sciences must learn that each time they "solve" a problem, they should "check" their result. If an equation is solved for x, then x should be substituted back into the equation to ensure that it works correctly. The importance within mathematics, science, and engineering of checking one's work cannot be emphasized enough. It is a crucial ingredient of all good work. Is it possible/desirable for a program to check its own work? This research seeks to show that in a number of cases it is also possible for programs to correct their own work. Checking sounds similar to Verification, but it is different. For one, Verification proves that a program is correct on all inputs. Checking only proves that it is correct on the given input. It is felt that Checking can be of use to Verification and Testing, just as Verification and Testing can each be of use to Checking. More to the point, it is felt that program checking has the potential to increase program reliability substantially.

With the explosion in connectivity of computers and in the size of data sets available for analysis, mathematically sophisticated algorithms are becoming increasingly crucial for a wide range of real-world applications. Unfortunately, it often takes many years for an algorithm to make it from theory into applications. In fact, the trend has been for different areas to develop their own algorithms independently, with the result that similar techniques reinvented many times in different contexts, and radically new approaches that require an algorithmic level of abstraction take a long time to make it into applications.
The intellectual core of this proposal is to create a coordinated effort in "Algorithms from Theory to Practice" that connects the basic development of fundamental algorithms and data structures to their many disparate uses. This work will address critical needs by connecting relevant algorithms to application areas, by exposing and tackling important issues that are common to multiple applications, and by developing fundamentally new approaches to solving key problems via the connections made.
This proposal aims to provide impact at a number of different levels. At the lowest level are specific research projects that target key application domains. These include algorithms for mesh generation with applications to scientific simulations and graphics, algorithms for indexing and searching needed for a number of data analysis tasks, and protocols that connect machine learning with cryptography to produce a fundamentally new way for people to securely authenticate to their computers. At a higher level, this proposal will create a center to which researchers in application areas can come to build connections and integrate algorithmic techniques and principles into their own projects. At the highest level, this proposal will create tools to improve the process of moving algorithms from theory to applications more broadly. As one example, the course "Algorithms in the Real World" run by PI Blelloch has already developed a set of web pages detailing how algorithms are used in various applications and what turn out to be the crucial issues involved. A new, extensible version of this database would provide support for theoreticians, practitioners, and educators. We hope the end result to be both a faster pipeline from algorithm design to application, and improved sharing of algorithm techniques across application areas. In addition, we expect the students supported by this effort to fulfill the highest-level goals of this project becoming the next generation vertically-integrated algorithm researchers.
The PIs each have a strong track-record in algorithms, both theoretical and applied. Guy Blelloch is developer of the NESL parallel programming language, as well as fast parallel algorithms for a number of core problems. Arvin Blum is known for his work in machine learning and approximation algorithms, and is developer of the Graphphan planning algorithm, used as the basis of many AI planning systems. Manuel Blum is winner of the ACM Turning Award for his work in the foundation of computational complexity theory and its applications to cryptography and program checking. John lafferty is known for his work in language modeling and information retrieval, and is co-developer (along with PI Sleator)of the Link Grammar natural-language parser. Daniel Sleator is winner of this year's ACM Kanellakis "Theory and Practice" award for the development of the Splay Tree data structure, and more recently been developing algorithms for natural language applications.