This post is a survey on optimal proof systems. I will not cover any results in detail, but try to present the general picture of what is known and what to expect.
A general proof system in the sense of Cook and Reckhow (1979) can be understood as a nondeterministic guess-and-verify algorithm. The question whether there exist optimal proof systems essentially asks whether there exists a best such verification procedure. For practical purposes, such an optimal proof system would be extremely useful, as both the search for good verification algorithms as well as the quest for lower bounds to the proof size could concentrate on the optimal system. Thus the following question is of great significance: Do there exist optimal proof systems for a given language ?
Formally, a proof system for is optimal, if for any proof of in any proof system for there exists a proof of in the system that is at most polynomially longer than . If this transformation of into can even be computed efficiently, then is called p-optimal. Currently, it is only known that all languages in NP have optimal proof systems and all languages in P even admit p-optimal proof systems. However, it is open whether there exist languages outside NP with optimal proof systems or outside P with p-optimal proof systems.
Of central interest is the question whether there exists an optimal proof system for the coNP complete set of classical propositional tautologies. This question was posed by Krajíček and Pudlák (1989). Understanding the question better through characterizations is an important line of research with connections to a number of different topics. The first result in this area is due to Krajíček and Pudlák (1989) who showed the equivalence between the existence of p-optimal proof systems for propositional tautologies and the existence of optimal acceptors (algorithms that are optimal on the positive instances) for this problem. This equivalence was generalized to other problems by Sadowski (1999) and Messner (1999). Beyersdorff, Köbler, and Messner (2009) showed that optimality implies p-optimality for any system and any language if and only if the natural proof system for SAT (where proofs are just satisfying assignments) is p-optimal; the existence of an optimal system would imply the existence of a p-optimal system if there is some p-optimal system for SAT.
Recently, Chen and Flum (2012) uncovered further surprising relations of optimal proof systems to descriptive complexity and parameterized complexity. The link between these fields is provided by studying listings, i.e., enumerations of machines that compute all easy subsets of intractable problems like TAUT. Through this link Chen and Flum relate optimal proof systems to the existence of bounded logics for complexity classes such as polynomial time as well as deterministic and nondeterministic logarithmic space.
2. Necessary and sufficient conditions
There are also interesting connections to core questions of complexity theory. As already mentioned, an optimal system for propositional tautologies would allow to reduce the NP vs coNP question to proving proof size bounds for just this optimal proof system. Optimal proof systems also imply the existence of complete problems for various promise complexity classes as disjoint NP pairs (Razborov 1994, Pudlák 2003, Glaßer et al. 2005, Beyersdorff 2007), NPcoNP (Sadowski 1997) and probabilistic classes such as BPP (Köbler et al. 2003). Further to these implications, Itsykson (2010) has shown the surprising result that the average-case version of BPP has a complete problem.
Computational complexity also provides sufficient conditions for the existence of (p-)optimal proof systems; however, these are not as widely believed as structural assumptions like NPcoNP. Krajíček and Pudlák (1989) showed that the existence of optimal (resp., p-optimal) propositional proof systems is implied by NE=coNE (resp., E=NE), and Köbler, Messner, and Torán (2003) weakened these assumptions to double exponential time.
3. Positive results in different models
Other recent research concentrated on modified versions of the problem, where a number of surprising positive results have been obtained. Cook and Krajíček (2007) showed that (p-)optimal proof systems for tautologies exist if we allow just one bit of non-uniform advice. This result generalizes to arbitrary languages (Beyersdorff et al. 2011), but does not translate into optimal algorithms or acceptors. Hirsch et al. (2012) showed that optimal acceptors exist in a heuristic setting where we have a probability distribution on the complement of the language, but it is open whether this translates into optimal heuristic proof systems. Still another positive result was obtained by Pitassi and Santhanam (2010) who show that there exists an optimal quantified propositional proof system under a weak notion of simulation.
4. Relations to bounded arithmetic
Another interesting relation is to weak first-order arithmetic theories, so-called bounded arithmetic. Propositional proof systems are known to enjoy a close relationship to suitable theories of bounded arithmetic, e.g. extended Frege systems EF correspond to the theory . This correspondence has two facets: 1) proofs of first-order statements in can be translated into polynomial-size EF proofs and 2) every proof system for which can prove the consistency is simulated by EF. Therefore, from the point of view of , there exists an optimal propositional proof system, namely EF. Likewise, from the point of view of , there exists a complete disjoint NP-pair (the canonical pair of EF) etc.
5. So, do they exist?
In general, the question whether optimal proof systems exist is wide open; however, most researchers seem to conjecture a negative answer. Confirming such a negative answer seems out of reach with current techniques as this would imply a separation of complexity classes. On the other hand, while a positive answer would have interesting consequences (optimal problems for promise classes), these would not be as dramatic as e.g. a collapse of the polynomial hierarchy and therefore would not seem to be in sharp conflict with beliefs of complexity theorists. Thus, we will probably not see the answer to the question soon; however, research on this topic will hopefully continue to uncover interesting connections between complexity and logic.
Virginia Vassilevska Williams stunned the world of computer science by presenting the first improvement to the matrix multiplication constant in twenty years (later it was found that a more modest progress had been obtained independently and slightly earlier by Andrew James Stothers). The current world record is held by François Le Gall, who showed that by perfecting the methods of Vassilevska Williams. For an exposition of this line of work, check out my recent lecture notes. For the full details, I recommend Le Gall’s paper and the journal version of Stothers’ thesis (with his advisor A. M. Davie). The recent progress heavily builds on classic work by Coppersmith and Winograd. Briefly, they came up with a basic identity known as the Coppersmith–Winograd identity. Applying Strassen’s laser method with their own ingenious construction (relying on Salem–Spencer sets), they obtained the bound . Applying their method to the tensor square of the basic identity, they obtained the improved bound . That’s where things had been standing since 1990, until Stothers managed to perform the computations for the fourth tensor power, obtaining the bound in 2010. A year later (but independently), Vassilevska Williams analyzed the eighth tensor power and obtained the bound . Further progress was obtained by Le Gall, who analyzed the sixteenth and thirty-second tensor powers, obtaining the current world record stated above. Although taking ever higher tensor powers improves the bound on , the improvements are diminishing, and it seems safe to conjecture that taking the th tensor power does not yield the conjectured as . However, how can we be certain? Perhaps the improvements slow down, but like a slowly divergent series, eventually go all the way down to ? In the rest of the blog post, we describe a recent result of Andris Ambainis and myself, which shows that the best bound that this method can produce is , for any value of . In fact, our result allows for a wider class of methods which utilize the Coppersmith–Winograd identity, and hint to a new technique which can potentially lead to better algorithms. Very recently, Le Gall was able to use our methods to show that the best bound that can be obtained by taking an th tensor power of the Coppersmith–Winograd identity is , and so the current analysis of the identity is quite tight. Read the rest of this entry »
Matrix multiplication has become a popular topic recently. The main goal in this area is determining the value of the matrix multiplication constant , which is the infimum over all such that two complex matrices can be multiplied using arithmetic operations (addition, subtraction, multiplication, and division; arbitrary complex constants can appear as operands). Sloppy authors often define as a minimum instead of an infimum, but it is not clear that any algorithm exists. Indeed, given the common belief that , a classic result of Ran Raz which gives a lower bound of , assuming all the constants used are small, suggests that there is no algorithm (though there could be an asymptotically optimal algorithm, say one which runs in time ).
In this blog post we describe a result due to Coppersmith and Winograd that implies that a certain class of techniques provably cannot yield an optimal exponent, i.e. an algorithm, namely all algorithms which result from an invocation of Schönhage’s asymptotic sum inequality. This class includes Strassen’s original algorithm and all algorithms hence up to Strassen’s laser method, used in the celebrated algorithm of Coppersmith and Winograd, which corresponds to infinitely many invocations of the asymptotic sum inequality, and so is not subject to this limitation. The proof proceeds by showing how any identity (to which the asymptotic sum inequality can be applied) can be improved to another identity yielding a better bound on .
This week on “Speedup in Computational Complexity” we’re going to learn how to write an optimal solver for SAT. Thanks to Leonid Levin we know that a very partial answer to “Are there familiar computational problems with no best algorithm?” is “Well, computing a satisfying assignment for a boolean formula does have a best algorithm, that’s for sure!”. In fact we’ll explore several variations of an idea by Levin all of which provide us with computational problems that each have a best algorithm. One particular variation, by Claus-Peter Schnorr, applies to the class of self-reducible problems.
A word of warning before we start: The below constructions only work in some models of complexity. One of the models in which the results will not apply is the Turing Machine model. I will mention the model requirements as we go along but if you’d like a more detailed discussion of this topic, I refer you to Gurevich’s paper in the references.
Without further ado let’s jump straight into Levin’s neat little trick, performed by a combination of an interpreter and a program enumerator.
A wonderful sequence of values
The program that we’ll design in this section takes an input x and runs infinitely, outputting an infinite sequence of values. Our program will output a new number in the sequence every k steps for some constant k. The sequence produced will turn out to be quite a wonderful characterization of x (if you love computational complexity). I’ll use the name iseq(x) for the infinite sequence generated on input x.
To design our program – let’s call it iseqprog – we’ll need two other programs to start from: A program enumerator and an interpreter for the enumerated programs.
The program enumerator, progen, takes as input a pair (i,x) and returns the initial configuration of the program with index i on input x. We’ll expect this operation to be constant-time when either i=0 or we already called progen on (i-1,x). In other words: progen is more like a method of an object (with internal state) which expects to be called with inputs (0,x), (1,x), (2,x),… and is able to process each item in such a call sequence in constant-time.
The interpreter we’ll need cannot be any old interpreter. In these modern times we can expect a certain service level. The interpreter should work like a slot machine in the arcades: Whenever I put in a new coin I continue my game with three more lives. In other words, when I give the interpreter the configuration of program p after t steps on input x, it returns an updated configuration representing the state of program p after t+1 steps on input x. It also tells me if p terminated in step t+1 and, if so, the return value of p on x. All of this happens in constant time. After all, the interpreter only needs to simulate one single step of p on x.
Comment: Almost any old interpreter can be used for Levin’s construction, but the exposition would become more complex.
Now I’ll describe the computation of iseqprog on input x. The computation proceeds in rounds, and each round consists of a number of stages. There is an infinite number of rounds. The number of stages in each round is finite but not constant across rounds.
Round 1 has only 1 stage. In this first stage of the first round, iseqprog runs progen on (0,x) and gets back the initial configuration of program 0 on input x. iseqprog then uses the interpreter to interpret just 1 step of program 0 on input x. If program 0 happens to terminate on input x in that first step, iseqprog immediately outputs program 0’s output on input x. Regardless of whether the interpretation of program 0 terminated, iseqprog itself does not terminate; it is on its way to generate an infinite sequence. If the interpretation of program 0 on input x did not terminate in its first step, iseqprog outputs the value 0 before continuing, providing us with a signal that it’s still live and running. This concludes the first (1-stage) round of iseqprog’s computation on x.
The computation continues in an infinite sequence of rounds. In each round, iseqprog calls progen once, adding one new item to the set of program configurations it has accumulated during the previous rounds. Each of these program configurations is interpreted for a number of steps. Every time the interpreter has executed one step of a program i, iseqprog outputs one value. The output value will be 0 or program i’s output on x. Whatever program you may think of, iseqprog will eventually generate its output on x (in between a lot of 0’s and many other values).
If we use this shorthand:
- “+i”: means “create the initial configuration for program i on input x, then interpret 1 step on that configuration and output one value”
- “i” means “interpret 1 more step on the stored configuration for program i and output one value”
then we can sum up iseqprog’s first rounds like this:
Round 1: +1
Round 2: 11+2
Round 3: 111122+3
Round 4: 11111111222233+4
Round 5: 111111111111111122222222333344+5
Round 6: 32 1’s, 16 2’s, 8 3’s, 4 4’s, 2 5’s, and one +6
I hope it has become clear why iseqprog should be able to generate a new item of iseq every k steps or less for some constant k. Apart from the administrative work of looking up and saving configurations in some table, each step involves at most one call to the program enumerator and one call to the interpreter. These calls were assumed to be constant-time. The administrative work I wlll simply assume to be constant-time as well. iseqprog cannot work as intended in all complexity models; in particular, it doesn’t work for Turing machines.
Now let’s have a look at the sequence iseq(x) itself. The key observation is that although any individual program does not get much attention from iseqprog, it does get a specific percentage of attention that is not dependent on the input x. For instance, program 3 accounts for of the interpreter calls made by iseqprog regardless of the input x. The percentage is tied only to the program’s index number according to the program enumerator. From this observation we can derive (proof left to the reader) the salient feature of iseq(x):
If program p outputs y on input x in time t, then y appears in iseq(x) at an index less than ct for c depending only on p.
I think this is great! Whatever you want to compute from x, you’ll find it in iseq(x). What’s more: Your answer appears quite early in the sequence – so early, in fact, that you might as well just run through iseq(x) rather than perform the computation itself! That’s why I decided to call iseq(x) a wonderful sequence.
It’s too good to be true…if it wasn’t for two caveats. First, how do you recognize the value that you’re looking for? And second, what about that constant c? We’ll address these two questions below.
Comment: Another caveat is that the above doesn’t apply to all complexity models, in particular to Turing Machines. For most of the common complexity models, I expect that the result will be true if you replace ct by poly(t) where poly is a polynomial depending only on p
I’ll end this section with a simple specialization of the above that is too nice not to mention:
For any function f in P, there is a polynomial p such that
And yes, iseqprog generates a new item of iseq(x) in k steps or less for some constant k!
The optimal solver for SAT
So what good is all this if you cannot recognize the value you’re looking for. Luckily there are some situations where validating a correct answer is simpler than producing it – yes, I’m thinking about SAT. A satisfying assignment for a boolean formula can be validated in linear time. How can we exploit Levin’s idea to create an optimal solver for SAT?
The simplest answer is to modify the program enumerator. Our new program enumerator, call it progenSAT, wraps each program generated by the original program enumerator in a SAT validator. The computation of progenSAT(i,x) will proceed in two phases like this:
Phase 1: Run progen(i,x) and assign its output value to variable y.
Phase 2: If y is a satisfying assignment for the boolean formula x then output y else loop infinitely.
If we plug progenSAT into iseqprog we get a new program iseqprogSAT generating a new sequence iseqSAT(x) on input x.
Like the original iseqprog, our new program iseqprogSAT generates a new item every k steps or less for some constant k. I’m assuming that progenSAT also takes constant time to generate each new program configuration. Let us adapt the key observation about iseq(x) to the sequence iseqSAT(x) (once again, I’ll leave the proof to the reader):
If program p outputs y on input x in time t, and y is a satisfying assigment for the boolean formula x, then y appears in iseqSAT(x) at an index less than c'(t+|x|) for c’ depending only on p.
This is remarkable! This means we have a concrete program that is optimal (up to a constant factor) for solving SAT. As a consequence, The question of P vs. NP boils down to a question about this single program’s running time. Define to be the number of steps program p takes to generate a nonzero value on input x. Now P=NP if and only if there is a polynomial p such that for every satisfiable boolean formula x.
In other words, there may be 1 million US$ waiting for you if you’re able to analyze iseqprogSAT‘s running time in detail.
Notes for the experimentalists
Now we’ll have a look at the other caveat about Levin’s idea: The constant factor. In the 1990’s, under the supervision of Neil Jones and Stephen Cook, I worked on implementing a program enumerator that would get iseqprog to actually terminate on some toy problems. The problem, of course, is that the constant factors involved are so large you’ll be tempted to never use big-O-notation ever again. Let’s assume that your programs are sequences of k different instructions, and that every sequence of instructions is a valid program. Then the index of a program p is roughly . The constant factor c is then approximately i.e. doubly exponential in |p|. So to get an answer from iseqprog the useful programs need to be really short.
Actually I found that iseqprog favours short programs so much that it sometimes fails to find program that actually computes the function you’re looking for. In one case, half of the inputs caused one little program, p’, to give the correct result while the other half of the inputs caused another little program, p’’, to give iseqprog its output. A program that tested the input then continued as either p’ or p’’ was too long to ever get simulated.
It’s actually possible to reduce the constant factor c by a lot, if you’re willing to sacrifice the optimality in asymptotical running time. By revising the strategy used to pick which program to interpret, you wil obtain different tradeoffs between constant factor and asymptotical relation. For instance, consider the variant of iseq(x), call it iseq_triangle(x) obtained by using the following simple strategy in Levin’s construction:
Round 1: +1
Round 2: 1+2
Round 3: 12+3
Round 4: 123+4
Round 5: 1234+5
I’ll postulate the following, leaving the proof to the reader: If program p outputs y on input x in time t, then y appears in iseq_triangle(x) at an index less than .
I once identified a few strategies of this kind but never got around to clarifying in more detail which tradeoffs are possible; or indeed optimal. Could the “triangle” strategy be improved so that the expression above instead would be ? I doubt it, but have no proof. It seems like a small but interesting math exercise.
In one variation of iseqprog the programs are actually enumerated in the order of their descriptive complexity. See the references below for details on that.
Schnorr’s self-reducible predicates
Claus-Peter Schnorr analyzed applications of Levin’s result in a 1976 ICALP paper. In particular, he was interested in defining a class of predicates that do not allow asymptotical speedup. The contrast to the above results should be noticed: It is an actual predicate, a 2-valued function, that does not have speedup.
I have not been able to prove Schnorr’s main result (the paper’s proof is missing a few details) but I’d like to outline his central idea because it is interesting, and maybe one of the readers can be helpful by providing a proof in the comments of this blog post. I have simplified his definition a bit and refer you to the ICALP paper for the general definition, and for his results on graph isomorphism and speedup in the Turing machine space model.
Let us adapt some notation from the previous blog post by Amir Ben-Amram and define the complexity set of a function f to be
In the remainder of this section, all data will be bit strings, and P will designate a binary predicate, i.e. . You may think of SAT as a prime example of the kind of predicates Schnorr analyzes. The decision function for P will be defined by
A function w is a witness function for P if and only if
The idea behind Schnorr’s result is to consider a class of predicates, P for which there is a tight connection between the complexity set and the complexity sets of the associated witness functions:
The class in question is the class of (polynomial-time) self-reducible predicates. The criteria for being self-reducible are a bit complex. I will provide a simplified, less general, version here. P is self-reducible if implies and there is a polynomial-time function mapping a pair of (bit string, bit) to a bit string such that
Theorem (Schnorr, 1976, Theorem 2.4, rewritten): When P is self-reducible, there is an integer k and witness function w for P such that
This theorem is not too hard to prove. To find a witness y for an x, you figure out the bits of y one at a time. It takes rounds in which we test both 0 and 1 as the potential “next bit” of a witness. For the details, I refer you to Schnorr’s paper.
The main theorem of interest to this blog post is Schnorr’s Theorem 2.7. A precise statement of the Theorem requires more technical detail than I’m able to provide here, but its essence is this: For a self-reducible predicate P, the decision problem cannot be sped up by a factor of .
As mentioned above, I’ve not been able to construct a proof based on the ICALP paper, so I’ll leave this a homework to the readers! It certainly seems like all of the necessary constructions have been lined up, but at the place where “standard methods of diagonalization” should be applied I cannot find a satisfactory interpretation of how to combine the big-O notation with the quantification of the variable i. I’d be very interested in hearing from readers that succeeded in proving this Theorem.
Historical notes and references
All papers mentioned below appear in this blog’s bibliography
Leonid Levin introduced the idea in (Levin, 1973). I must admit that I’ve never read the original Russian paper nor its translation in (Trakhtenbrot, 1984), so I rely on (Gurevich, 1988) and (Li and Vitányi, 1993) in the following. The paper presented his “Universal Search Theorem” as a result concerning resource-bounded descriptional complexity. There was no proof in the paper, but he provided the proof in private communications to Gurevich. Levin’s paper uses an advanced strategy for selecting which program to generate in each round. This strategy causes the constant factor associated with a program p to be where K(p) is the prefix complexity of p and for some constant k. This is explained in Section 7.5 of (Li and Vitányi, 1993).
Schnorr’s paper (Schnorr, 1976) is the earliest English exposition on this topic that I know of, and it seems to be the first application of Levin’s idea to predicates rather than functions with arbitrarily complex values. Gurevich dedicated most of (Gurevich, 1988) to explaining Levin’s idea which seems to have been largely unknown at the time. A major topic in Gurevich’s discussion is the complexity models in which Levin’s idea can be utilized. Amir Ben-Amram wrote a clear and precise exposition on Levin’s idea in Neil Jones’s complexity book (Ben-Amram, 1997), in his guest chapter “The existence of optimal programs”.
There have been some experiments with practical implementation of Levin’s idea. (Li and Vitányi, 1993) mentions work from the 1980’s that combines Levin’s algorithm with machine learning. My own experiments (Christensen, 1999) were done without knowledge of this prior and does not use machine learning but focuses on tailored programming languages and efficient implementations.
About the author
I’m a Ph.D. of computer science based in Copenhagen, Denmark. I am currently a Senior System Engineer working on developing highly scalable, distributed systems for Issuu, the leading digital publishing platform (see http://issuu.com/about). My interest in complexity theory was nurtured by Neil D. Jones and I was brought up on his book “Computability and Complexity From a Programming Perspective”. I recently had the pleasure of co-authoring a paper with Amir Ben-Amran and Jakob G. Simonsen for the Chicago Journal of Theoretical Computer Science, see http://cjtcs.cs.uchicago.edu/articles/2012/7/contents.html
Leonid Levin is known for several fundamental contributions to Complexity Theory. The most widely known is surely the notion of “universal search problem,” a concept similar to (and developed concurrently with) NP-completeness. Next, we might cite the proof of the existence of optimal “honest” algorithms for search problems (an honest algorithm uses a given verifier to check its result; expositions of this theorem can be found, among else, here and here). This is an important result regarding the tension between speedup and the existence of optimal algorithms, and will surely be discussed here in the future.
Then, there is a third result, which seems to be less widely known, though it definitely ought to: I will call it The Fundamental Theorem of Complexity Theory, a name given by Meyer and Winklmann to a theorem they published in 1979, following related work including (Meyer and Fischer, 1972) and (Schnorr and Stumpf, 1975). As with the NP story, similar ideas were being invented by Levin in the USSR at about the same time. Several years later, with Levin relocated to Boston, these lines of research united and the ultimate, tightest, polished form of the theorem was formed, and presented in a short paper by Levin and, thankfully, a longer “complete exposition” by Seiferas and Meyer (here – my thanks to Janos Simon for pointing this paper out to me). Seiferas and Meyer did not name it The Fundamental Theorem, perhaps to avoid ambiguity, but I think that it does deserve a name more punchy than “a characterization of realizable space complexities” (the title of the article).
My purpose in this blog post is to give a brief impression of this result and its significance to the study of speedup phenomena. The reader who becomes sufficiently interested can turn to the complete exposition mentioned (another reason to do so is the details I omit, for instance concerning partial functions).
Why this theorem is really fundamental
Some Definitions: An algorithm will mean, henceforth, a Turing machine with a read-only input tape and a worktape whose alphabet is (the machine can sense the end of the tape – so no blank necessary). Program also means such a machine, but emphasizes that its “code” is written out as a string. Complexity will mean space complexity as measured on the worktape. For a machine , its space complexity function is denoted by . A function that is the of some is known as space-constructible.
Note that up to a certain translation overhead, results will apply to any Turing-equivalent model and a suitable complexity measure (technically, a Blum measure).
The Seiferas-Meyer paper makes use of a variety of clever programming techniques for space-bounded Turing machines; one example is universal simulation with a constant additive overhead.
I will argue that this theorem formulates an (almost) ultimate answer to the following (vague) question: “what can be said about optimal algorithms and speedup in general, that is, not regarding specific problems of interest?”
Examples of things that can be said are Blum’s speedup theorem: there exist problems with arbitrarily large speedup; the Hierarchy theorem: there do exist problems that have an optimal algorithm, at various levels of complexity (the type of result they prove is called a compression theorem, which unfortunately creates confusion with the well-known tape compression theorem. The appelation hierarchy theorem may bring the right kind of theorem to mind).
As shown by Seiferas and Meyer, these results, among others, can all be derived from the Fundamental Theorem, and for our chosen measure of space, the results are particularly tight: their Compression Theorem states that for any space-constructible function , there are algorithms of that complexity that cannot be sped up by more than an additive constant. So, even a tiny multiplicative speedup is ruled out for these algorithms – and the algorithm may be assumed to compute a predicate (so, the size of the output is one bit and is not responsible for the complexity).
An important step to this result is the choice of a clever way to express the notion of “a problem’s complexity” (more specifically, the complexity of computing a given function). To the readership of this blog it may be clear that such a description cannot be, as one may naïvely assume, a single function that describes the complexity of a single, best algorithm for the given problem. The good answer is a so-called complexity set. This is the set of all functions for machines that solve the given function (Meyer and Fischer introduced a similar concept, complexity sequence, which is specifically intended to describe problems with speedup).
How can a complexity set be specified? Since we are talking about a set of computable functions here (in fact, space-constructible), it can be given as a set of programs that compute the functions. This is called a complexity specification. The gist of the Theorem is that it tells us which sets of programs do represent the complexity of something – moreover, it offers a choice of equivalent characterizations (an always-useful type of result).
Clearly, if a can be computed in space , it can also be computed in a larger space bound; it can also be computed in a space bound smaller by a constant (a nice exercise in TM hacking – note that we have fixed the alphabet). If and are space bounds that suffice, then does too (another Turing-machine programming trick). So, we can assume that a set of programs represent the closure of the corresponding set of functions under the above rules. We can also allow it to include programs that compute functions which are not space-constructible: they will not be space bounds themselves, but will imply that constructible functions above them are. So, even a single program can represent an infinite family of time bounds: specifically, the bounds lower-bounded (up to a constant) by the given function.
A statement of the theorem (roughly) and consequences
Theorem. Both of the following are ways to specify all existing complexity sets:
- Sets of programs described by predicates (i.e., , where is a decidable predicate).
The last item I find the most surprising. It is also very powerful. For any machine , the fact that is a complexity specification tells us there there is a function (in fact, a predicate) computable in space if and only if . Here is our Compression theorem!
The first characterization is important when descriptions by an infinite number of functions are considered. For example, let us prove the following:
Theorem. There is a decision problem, solvable in polynomial (in fact, quadratic) space, that has no best (up to constant factors) algorithm.
Proof. Let be a program that computes , written so that is just a hard-coded constant. The idea is for the set of to be recursively enumerable. Note that all these functions are constructible, that is, prospective space bounds.
Then, by the fundamental theorem, there is a decision problem solvable in space if and only if is at least one of these functions (up to an additive constant). If some algorithm for this problem takes at least space, then there is also a solution in , and so forth.
Limitations and some loose ends
As exciting as I find this theorem, it has its limitations. Not all the speedup-related results seem to follow from it; for instance, the other Levin’s theorem doesn’t (or I couldn’t see how). Also, results like those given here and here about the measure, or topological category, of sets like the functions that have or do not have speedup, do not seem to follow. In fact, Seiferas and Meyer only prove a handful of “classic” results like Blum speedup, the Compression theorem and a Gap theorem. What new questions about complexity sets can be asked and answered using these techniques?
Another limitation is that for complexity measures other than space we do not have such tight results. So, for example, for Turing-machine time we are stuck with the not-so-tight hierarchy theorems proved by diagonalization, padding etc. (see references in the bibliography). Is this a problem with our proof methods? Or could some surprising speedup phenomenon be lurking there?
[Oct 16, 2012. Fixed error in last theorem]
On the recent progress on matrix multiplication algorithms (guest post by Virginia Vassilevska Williams)September 22, 2012
A central question in the theory of algorithms is to determine the constant , called the exponent of matrix multiplication. This constant is defined as the infimum of all real numbers such that for all there is an algorithm for multiplying matrices running in time . Until the late 1960s it was believed that , i.e. that no improvement can be found for the problem. In 1969, Strassen surprised everyone by showing that two matrices can be multiplied in time. This discovery spawned a twenty-year-long extremely productive time in which the upper bound on was gradually lowered to . After a twenty-year stall, some very recent research has brought the upper bound down to .
Bilinear algorithms and recursion.
Strassen’s approach was to exploit the inherent recursive nature of matrix multiplication: the product of two matrices can be viewed as the product of two matrices, the entries of which are matrices. Suppose that we have an algorithm ALG that runs in time and multiplies two matrices. Then one can envision obtaining a fast recursive algorithm for multiplying matrices (for any integer ) as well: view the matrices as matrices the entries of which are matrices; then multiply the matrices using ALG and when ALG requires us to multiply two matrix entries, recurse.
This approach only works, provided that the operations that ALG performs on the matrix entries make sense as matrix operations: e.g. entry multiplication, taking linear combination of entries etc. One very general type of such algorithm is the so called bilinear algorithm: Given two matrices and , compute products
i.e. take possibly different linear combinations of entries of and multiply each one with a possibly different linear combination of entries of . Then, compute each entry of the product as a linear combination of the : .
Given a bilinear algorithm ALG for multiplying two matrices (for constant ) that computes products , the recursive approach that multiplies matrices using ALG gives a bound . To see this, notice that the number of additions that one has to do is no more than : at most to compute the linear combinations for each and at most for each of the outputs . Since matrix addition takes linear time in the matrix size, we have a recurrence of the form .
As long as we get a nontrivial bound on . Strassen’s famous algorithm used and thus showing that . A lot of work went into getting better and better “base algorithms” for varying constants . Methods such as Pan’s method of trilinear aggregation were developed. This approach culminated in Pan’s algorithm (1978) for multiplying matrices that used products and hence showed that .
Approximate algorithms and Schonhage’s theorem.
A further step was to look at more general algorithms, so called approximate bilinear algorithms. In the definition of a bilinear algorithm the coefficients were constants. In an approximate algorithm, these coefficients can be formal linear combinations of integer powers of an indeterminate, (e.g. ). The entries of the product are then only “approximately” computed, in the sense that , where the term is a linear combination of positive powers of . The term “approximate” comes from the intuition that if you set to be close to , then the algorithm would get the product almost exactly.
Interestingly enough, Bini et al. (1980) showed that when dealing with the asymptotic complexity of matrix multiplication, approximate algorithms suffice for obtaining bounds on . This is not obvious! What Bini et al. show, in a sense, is that as the size of the matrices grows, the “approximation” part can be replaced by a sort of bookkeeping which does not present an overhead asymptotically. The upshot is that if there is an approximate bilinear algorithm that computes products to compute the product of two matrices, then .
Bini et al. (1979) gave the first approximate bilinear algorithm for a matrix product. Their algorithm used entry products to multiply a matrix with a matrix. Although this algorithm is for rectangular matrices, it can easily be converted into one for square matrices: a matrix is a matrix with entries that are matrices with entries that are matrices, and so multiplying matrices can be done recursively using Bini et al.’s algorithm three times, taking entry products. Hence .
Schonhage (1981) developed a sophisticated theory involving the bilinear complexity of rectangular matrix multiplication that showed that approximate bilinear algorithms are even more powerful. His paper culminated in something called the Schonhage -theorem, or the asymptotic sum inequality. This theorem is one of the most useful tools in designing and analyzing matrix multiplication algorithms.
Schonhage’s -theorem says roughly the following. Suppose we have several instances of matrix multiplication, each involving matrices of possibly different dimensions, and we are somehow able to design an approximate bilinear algorithm that solves all instances and uses fewer products than would be needed when computing each instance separately. Then this bilinear algorithm can be used to multiply (larger) square matrices and would imply a nontrivial bound on .
What is interesting about Schonhage’s theorem is that it is believed that when it comes to exact bilinear algorithms, one cannot use fewer products to compute several instances than one would use by just computing each instance separately. This is known as Strassen’s additivity conjecture. Schonhage showed that the additivity conjecture is false for approximate bilinear algorithms. In particular, he showed that one can approximately compute the product of a by a vector and the product of a by a vector together using only entry products, whereas any exact bilinear algorithm would need at least products. His theorem then implied , and this was a huge improvement over the previous bound of Bini et al.
Using fast solutions for problems that are not matrix multiplications.
The next realization was that there is no immediate reason why the “base algorithm” that we use for our recursion has to compute a matrix product at all. Let us focus on the following family of computational problems. We are given two vectors and and we want to compute a third vector . The dependence of on and is given by a three-dimensional tensor as follows: . The vector is a bilinear form. The tensor can be arbitrary, but let us focus on the case where . Notice that completely determines the computational problem. Some examples of such bilinear problems are polynomial multiplication and of course matrix multiplication. For polynomial multiplication, if and only if , and for matrix multiplication, if and only if and .
The nice thing about these bilinear problems is that one can easily extend the theory of bilinear algorithms to them. A bilinear algorithm computing a problem instance for tensor computes products of the form and then sets . Here, an algorithm is nontrivial if the number of products that it computes is less than the number of positions where the tensor is nonzero.
In order to be able to talk about recursion for general bilinear problems, it is useful to define the tensor product of two tensors and : . Thus, the bilinear problem defined by can be viewed as a bilinear problem defined by , where each product is actually itself a bilinear problem defined by .
This allows one to compute an instance of the problem defined by using an algorithm for and an algorithm for . One can similarly define the tensor power of a tensor as tensor-multiplying by itself times. Then any bilinear algorithm computing an instance defined by using entry products can be used recursively to compute the tensor power of using products, just as in the case of matrix multiplication.
A crucial development in the study of matrix multiplication algorithms was the discovery that sometimes algorithms for bilinear problems that do not look at all like matrix products can be converted into matrix multiplication algorithms. This was first shown by Strassen in the development of his “laser method” and was later exploited in the work of Coppersmith and Winograd (1987,1990). The basic idea of the approach is as follows.
Consider a bilinear problem for which you have a really nice approximate algorithm ALG that uses entry products. Take the tensor power of (for large ), and use ALG recursively to compute using entry products. is a bilinear problem that computes a long vector from two long vectors and . Suppose that we can embed the product of two matrices and into as follows: we put each entry of into some position of and set all other positions of to , we similarly put each entry of into some position of and set all other positions of to , and finally we argue that each entry of the product is in some position of the computed vector (all other entries are ). Then we would have a bilinear algorithm for computing the product of two matrices using entry products, and hence .
The goal is to make as large of a function of as possible, thus minimizing the upper bound on .
Strassen’s laser method and Coppersmith and Winograd’s paper, and even Schonhage’s -theorem, present ways of embedding a matrix product into a large tensor power of a different bilinear problem. The approaches differ in the starting algorithm and in the final matrix product embedding. We’ll give a very brief overview of the Coppersmith-Winograd algorithm.
The Coppersmith-Winograd algorithm.
The bilinear problem that Coppersmith and Winograd start with is as follows. Let be an integer. Then we are given two vectors and of length and we want to compute a vector of length defined as follows:
for , and .
Notice that is far from being a matrix product. However, it is related to matrix products:
which is the inner product of two -length vectors,
, , and , which are three scalar products, and
the two matrix products computing and for which are both products of a vector with a scalar.
If we could somehow convert Coppersmith and Winograd’s bilinear problem into one of computing these products as independent instances, then we would be able to use Schonhage’s -theorem. Unfortunately, however, the matrix products are merged in a strange way, and it is unclear whether one can get anything meaningful out of an algorithm that solves this bilinear problem.
Coppersmith and Winograd develop a multitude of techniques to show that when one takes a large tensor power of the starting bilinear problem, one can actually decouple these merged matrix products, and one can indeed apply the -theorem. The -theorem then gives the final embedding of a large matrix product into a tensor power of the original construction, and hence defines a matrix multiplication algorithm.
Their approach combines several impressive ingredients: sets avoiding -term arithmetic progressions, hashing and the probabilistic method. The algorithm computing their base bilinear problem is also impressive. The number of entry products it computes is , which is exactly the length of the output vector ! That is, their starting algorithm is optimal for the particular problem that they are solving.
What is not optimal, however, is the analysis of how good of a matrix product algorithm one can obtain from the base algorithm. Coppersmith and Winograd noticed this themselves: They first applied their analysis to the original bilinear algorithm and obtained an embedding of an matrix product into the -tensor power of the bilinear problem for some explicit function . (Then they took to go to infinity and obtained .) Then they noticed, that if one applies the analysis to the second tensor power of the original construction, then one obtains an embedding of an matrix product into the same -tensor power, where . That is, although one is considering embeddings into the same () tensor power of the construction, the analysis crucially depends on which tensor power of the construction you start from! This led to the longstanding bound . Coppersmith and Winograd left as an open problem what bound one can get if one starts from the third or larger tensor powers.
The recent improvements on .
It seems that many researchers attempted to apply the analysis to the third tensor power of the construction, but this somehow did not improve bound on . Because of this and since each new analysis required a lot of work, the approach was abandoned, at least until 2010. In 2010, Andrew Stothers carried through the analysis on the fourth tensor power and discovered that the bound on can be improved to .
As mentioned earlier, the original Coppersmith-Winograd bilinear problem was related to different matrix multiplication problems that were merged together. The tensor power of the bilinear problem is similarly composed of merged instances of simpler bilinear ptoblems, however these instances may no longer be matrix multiplications. When applying a Coppersmith-Winograd-like analysis to the tensor power, there are two main steps.
The first step involves analyzing each of the bilinear problems, intuitively in terms of how close they are to matrix products; there is a formal definition of the similarity measure called the value of the bilinear form. The second step defines a family of matrix product embeddings in the tensor power in terms of the values. These embeddings are defined via some variables and constraints, and each represents some matrix multiplication algorithm. Finally, one solves a nonlinear optimization program to find the best among these embeddings, essentially finding the best matrix multiplication algorithm in the search space.
Both the Coppersmith-Winograd paper and Stothers’ thesis perform an entirely new analysis for each new tensor power . The main goal of my work was to provide a general framework so that the two steps of the analysis do not have to be redone for each new tensor power . My paper first shows that the first step, the analysis of each of the values, can be completely automated by solving linear programs and simple systems of linear equations. This means that instead of proving theorems one only needs to solve linear programs and linear systems, a simpler task. My paper then shows that the second step of the analysis, the theorem defining the search space of algorithms, can also be replaced by just solving a simple system of linear equations. (Amusingly, the fact that matrix multiplication algorithms can be used to solve linear equations implies that good matrix multiplication algorithms can be used to search for better matrix multiplication algorithms.) Together with the final nonlinear program, this presents a fully automated approach to performing a Coppersmith-Winograd-like analysis.
After seeing Stothers’ thesis in the summer of last year, I was impressed by a shortcut he had used in the analysis of the values of the fourth tensor power. This shortcut gave a way to use recursion in the analysis, and I was able to incorporate it in my analysis to show that the number of linear programs and linear systems one would need to solve to compute the values for the tensor power drops down to , at least when is a power of . This drop in complexity allowed me to analyze the tensor power, thus obtaining an improvement in the bound of : .
There are several lingering open questions. The most natural one is, how does the bound on change when applying the analysis to higher and higher tensor powers. I am currently working together with a Stanford undergraduate on this problem: we’ll apply the automated approach to several consecutive powers, hoping to uncover a pattern so that one can then mathematically analyze what bounds on can be proven with this approach.
A second open question is more far reaching: the Coppersmith-Winograd analysis is not optimal– in a sense it computes an approximation to the best embedding of a matrix product in the tensor power of their bilinear problem. What is the optimal embedding? Can one analyze it mathematically? Can one automate the search for it?
Finally, I am fascinated by automating the search for algorithms for problems. In the special case of matrix multiplication we were able to define a search space of algorithms and then use software to optimize over this search space. What other computational problems can one approach in this way?
Dear Hunter — What a nice idea. And many of your examples below are both new to me and quite interesting. Thanks! And good luck! — manuel
While thinking about your blog, two things occurred to me that might be worth mentioning:
1. If a function f(x) has speedup, then any lower bound on its computation can be improved by a corresponding amount. For example, if every program for computing f(x) can be sped up to run twice as fast (on all but a finite number of integers), then any lower bound G(x) on its run time can be raised from G(x) to 2G(x) (on all but a finite number of integers). For another example, if any program for computing f(x) can be sped up by a sqrt (so that any run time F(x) can be reduced to a runtime of at most sqrt(F(x)), then any lower bound G(x)on its run time can be raised to [G(x)]^2, etc. This is all easy to see.
2. Much harder to see is a curious relation between speedup and inductive inference, which has to do with inferring an algorithm from observation of the sequence of integers that it generates. Theorem: there exists an inductive inference algorithm for inferring all sequences that have optimal algorithms (i.e. have programs that cannot be sped up)! This was quite a surprise (and a breakthrough) for me. Still is. To explain it though, I’d have to explain inductive inference, etc, and this would take me a bit of time. Some day…
Anyway, thanks again for your blog.
Best wishes and warm regards,
Determining the exponent of matrix multiplication, , is one of the most prominent open problems in algebraic complexity. Strassen famously showed that in 1969, and after a sequence of works culminating in work of Stothers and Williams the best current upper bound is . It is believed that indeed , meaning that there is a family of algorithms with running time for every . In this sense, if , matrix multiplication exhibits “speedup”: there is no single best asymptotic algorithm, only a sequence of algorithms having running times , with approaching . In fact Coppersmith and Winograd showed in 1982 that this phenomenon occurs whatever the true value of is (two, or larger than two), a result that is often summarized by saying “the exponent of matrix multiplication is an infimum, not a minimum.”
Despite the algebraic nature of the matrix multiplication problem, many of the suggested routes to proving are combinatorial. This post is about connections between one such combinatorial conjecture (the “Strong Uniquely Solvable Puzzle” conjecture of Cohn, Kleinberg, Szegedy and Umans) and some more well-known combinatorial conjectures. These results appear in this recent paper with Noga Alon and Amir Shpilka.
The cap set conjecture, a strengthening, and a weakening
We start with a well-known, and stubborn, combinatorial problem, the “cap-set problem.” A cap-set in is a subset of vectors in with the property that no three vectors (not all the same) sum to 0. The best lower bound is due to Edel. Let us denote by the “cap set conjecture” the assertion that one can actually find sets of size . It appears that there is no strong consensus on whether this conjecture is true or false, but one thing that we do know is that it is a popular blog topic (see here, here, here, and the end of this post).
Now it happens that the only triples of elements of that sum to 0 are and — triples that are “all the same, or all different.” So the cap set conjecture can be rephrased as the conjecture that there are large subsets of vectors in so that for any in the set (not all equal), there is some coordinate such that are “not all the same, and not all different.” Generalizing from this interpretation, we arrive at a family of much stronger assertions, one for each : let’s denote by the “ conjecture” the assertion that there are subsets of vectors in , of size with the property that for any in the set (not all equal), there is some coordinate such that are “not all the same, and not all different.” Such sets of size in imply size -size sets of this type in by viewing each symbol in as a block of symbols in , so the conjecture is stronger (i.e. it implies the cap-set conjecture). Indeed, if you play around with constructions you can see that as gets larger it seems harder and harder to have large sets avoiding triples of vectors for which every coordinate has “all different.” Thus one would probably guess that the conjecture is false.
One of the results in our paper is that the conjecture is in fact *equivalent* to falsifying the following well-known sunflower conjecture of Erdos-Szemeredi: there exists an such that any family of at least subsets of contains a 3-sunflower (i.e., three sets whose pairwise intersections are all equal).
So the intuition that the conjecture is false agrees with Erdos and Szemeredi’s intuition, which is a good sign.
Now let’s return to the cap-set conjecture in . Being a cap set is a condition on *all* triples of vectors in the set. If one restricts to a condition on only some of the triples of vectors, then a construction becomes potentially easier. We will be interested in a “multicolored” version in which vectors in the set are assigned one of three colors (say red, blue, green), and we only require that no triple of vectors sums to 0 with being red, being blue, and being green. But a moment’s thought reveals that the problem has become too easy: one can take (say) the red vectors to be all vectors beginning with , the green vectors to be all vectors beginning with , and the the blue vectors to be all vectors beginning with . A solution that seems to recover the original flavor of the problem, is to insist that the vectors come from a collection of red, green, blue triples with ; we then require that every red, green, blue triple *except those in the original collection* not sum to 0. So, let’s denote by the “multicolored cap-set conjecture” the assertion that there are subsets of *triples of vectors* from of size , with each triple summing to 0, and with the property that for any three triples in the set (not all equal), .
If is a cap set in , then the collection of triples constitutes a multicolored cap-set of the same size, so the multicolored version of the conjecture is indeed weaker (i.e. it is implied by the cap-set conjecture).
A matrix multiplication conjecture between the two
The SUSP conjecture of Cohn, Kleinberg, Szegedy, and Umans is the following: there exist subsets of *triples of vectors* from of size , with each triple summing (in the integers) to the all-ones vector, and with the property that for any three triples in the set (not all equal), there is a coordinate such that .
The mysterious constant comes from the fact , and it is easy to see that one cannot have multiple triples with the same “ vector” (or , or …). More specifically, “most” triples that sum to the all-ones vector are balanced (meaning that each have weight ), and there can be at most balanced triples, without repeating an vector. So the conjecture is that there are actually subsets satisfying the requirements, whose sizes approach this easy upper bound.
If in the statement of the SUSP conjecture, one replaces “there is a coordinate such that ” with “there is a coordinate such that ” one gets the weaker “Uniquely Solvable Puzzle” conjecture instead of the “Strong Uniquely Solvable Puzzle” conjecture. Here one is supposed to interpret the triples as triples of “puzzle pieces” that fit together (i.e. their 1’s exactly cover the coordinates without overlap); the main requirement then ensures that no other way of “assembling the puzzle” fits together in this way, thus it is “uniquely solvable.” It is a consequence of the famous Coppersmith-Winograd paper that the Uniquely Solvable Puzzle conjecture is indeed true. Cohn, Kleinberg, Szegedy and Umans showed that if the stronger SUSP conjecture is true, then .
Two of the main results in our paper are that (1) the conjecture implies the SUSP conjecture, and (2) the SUSP conjecture implies the multicolored cap-set conjecture.
So by (1), *disproving the SUSP* conjecture is as hard as proving the Erdos-Szemeredi conjecture (which recall is equivalent to disproving the conjecture). Of course we hope the SUSP conjecture is true, but if it is not, it appears that will be difficult to prove.
And by (2), proving the SUSP conjecture entails proving the multicolored cap-set conjecture. So apart from being a meaningful weakening of the famous cap-set conjecture in , the multicolored cap-set conjecture can be seen as a “warm-up” to (hopefully) proving the SUSP conjecture and establishing . As a start, we show in our paper a lower bound of for multicolored cap-sets, which beats the lower bound of Edel for ordinary cap sets.
Returning to “speedup,” the topic of this blog, notice that the SUSP conjecture, as well as the cap-set, the multicolored cap-set, and the conjectures, all assert that there exist sets of size with certain properties, for various constants . In all cases is easily ruled out, and so all one can hope for is a sequence of sets, one for each , whose sizes approach as grows. If the SUSP conjecture is true, then it is this sequence of sets that directly corresponds to a sequence of matrix multiplication algorithms with running times for approaching . This would then be a concrete manifestation of the “speedup” phenomenon for matrix multiplication.