Wednesday, May 16, 2007

Godel Prize: Natural Proofs. My 2 cents

As several readers mentioned on my last post, the Godel Prize has been announced. The award goes to the authors of a PAPER and the paper can be a conference paper, but it must have appeared in the last 14 years. They should have made it 16 years. The 2007 winners:
Alexander Razborov and Steven Rudich
for the paper
Natural Proofs, Journal of Computing and Systems Sciences, Vol 55, No 1, 1997, pages 24-35. Goto either of their websites for the paper.
This is an excellent paper about limits on proof techniques in circuits. Its been blogged about and been described in a wikipedia entry. Very recently Sivakumar wrote a very nice short description of the concept. Has it changed how we do research? The closest analog is the Baker-Gill-Solovay results on Oracles. The contrast:
  1. Baker-Gill-Solovay showed that techniques that relativize do not suffice to resolve P vs NP. All proofs in recursion theory relativize. Hence we will need more than recursion theory techniques. (Some people disagree with this intepretation. If you are one of them, leave an intelligent comment.) Impact: (1) people got papers for constructing oracles to show that recursion theoretic techniques would not suffice to resolve certain problems, even problems nobody cared about. (2) people began looking more at combinatorial techniques such as circuits since those techniques tend to not relativize. One can argue if this is really true both mathematically and historically. It is possible that the move away from recursion theory to combinatorics was going to happen anyway, or already began. History is messy and hard to put into boxes.
  2. Razborov and Rudich showed that all lower bounds for circuits (except monotone circuits, for which the terms don't really make sense) ``naturalize'' and that such techniques won't suffice to solve several problems in circuits, including P vs NP, under some reasonable assumptions. There has not been a rush to show certain results naturalize. There has not been a mass movement away from circuits towards something else. But there may be at some later time, and in any case the paper is crucial for telling us what we've been doing and what its limitations are.
  3. Both results seemed to hint at independence results. Neither one has lead to any such results. Rudich told me once that they were 6 months away from an independence result. 10 years later he told me they are still 6 months away
  4. ``relativize'' was a natural notion that people already knew about at the time of the BGS paper. ``naturalize'' is a less natural notion that Razborov-Rudich discovered or invented for their paper. However it was a very important notion since it captured what many proofs had in common.

10 comments:

  1. One can prove that a separation result does not relativize by constructing oracles in the presence of which it does not hold.

    But how could one prove that a separation result, or technique, does not naturalize? As I read it, the R&R paper allows the "naturalizer" to make the separating property more specific to make it constructive, or more general to make it large. This gives the naturalizer an enormous advantage. So how will we ever know that a technique is capable of avoiding R&R?

    - Cris Moore

    ReplyDelete
  2. It seems the most likely way to avoid R-R is to make sure that the "largeness" condition is violated. That is, the useful property of Boolean functions that you're studying doesn't hold for a 1/2^{O(n)}-fraction of all Boolean functions, but it does happen to hold for the special family of Boolean functions you're proving lower bounds against (e.g. the family of functions that output "yes" iff the input encodes a satisfiable formula).

    To me, the primary strength of natural proofs is that they indicate the limitations of the probabilistic method for proving circuit lower bounds (the analysis of random choices can allow "largeness" to creep in).

    -ryan williams

    ReplyDelete
  3. "There has not been a mass movement away from circuits towards something else."

    That's absolutely accurate - what there has been, more or less, is stasis.

    But as far as independence results are concerned, weren't there some due to Razborov, following on the Natural Proofs work?

    I think Razborov-Rudich is less interesting for what it says about proof techniques than for what it says about estimating the circuit complexity of a function. See this post by Luca Trevisan.

    ReplyDelete
  4. We are going in circles. Someday in the near future we shall see another paper stating that Finite Model Theory can't solve the P vs. NP dilemma, too.

    Then eventually someone should prove that the language of all proofs that resolve the P vs. NP question is undecidable.

    ReplyDelete
  5. Then eventually someone should prove that the language of all proofs that resolve the P vs. NP question is undecidable.

    That sounds pretty good, since undecidable are nonempty!

    ReplyDelete
  6. Both results seemed to hint at independence results. Neither one has lead to any such results.

    I do not think it's true. Razborov used similar reasoning to show that certain weak theories of arithmetic cannot prove that SAT has no polynomial-size circuits (and hence, cannot provide proofs that "non-uniform NP != P").

    See
    Unprovability of Lower Bounds on the Circuit Size in Certain Fragments of Bounded Arithmetic, in Izvestiya of the Russian Academy of Science, mathematics, Vol. 59, No 1, 1995, pages 201-224.

    http://www.mi.ras.ru/~razborov/ind.ps

    ReplyDelete
  7. Bill,

    Why would 16 be better than 14? Its significance in base 2?

    ReplyDelete
  8. Cris and all,

    :: But how could one prove that a separation result, or technique, does not naturalize?

    The brief germ of my idea was to focus on properties whose associated decision problems are EXPSPACE-hard, and/or involve double-exponential counting. For Boolean or algebraic functions f(x_1,...,x_n), the quest is to find a complexity measure M(f) such that log(M(f)) is a lower bound on circuit/formula size for f, and then show for particular f that M(f) grows faster than exp(poly(n)). In the algebraic case this is most meaningful when f has "low" degree d = poly(n).

    For example, given a polynomial p(x_1,...,x_n) over C, define a monomial m to be "minimal" if m can be written in the form

    m = g_1 p'_1 + g_2 p'_2 + ... + g_n p'_n

    but no proper divisor of m can be written that way. Here p'_i is short for the partial derivative dp/dx_i, and g_1,...,g_n are arbitrary polynomials---the above says that m belongs to the Jacobian ideal Jac(p) of p.

    Finally define M(p) to be the number of minimal monomials for p. There are low-degree p for which M(p) grows as 2^{2^n}, but alas they include ones with linear-sized formulas, thus foreclosing a log(M(p)) circuit lower bound relation. Nevertheless, a hardness predicate H(p) = "M(p) >= h(n)" may have no better decision procedure than brute-force counting M(p), which is "super-natural" when g(n) >> exp(poly(n)). [The second attraction of M(p) was that whenever the ideal (p,q) has no monomials, as happens "generically", M(p*q) = 0, so many *-gates would be "monomial killers"---and you'd have the sharper goal of showing that circuits/formulas for p must have exponential-size sum-gates at the output.

    I've hunted for subtler measures M'(p) for which a log-circuit-size relation might hold. , but...I think nothing like counting connected components of varieties and other "low-level" stuff will work. Anyway, this seems to be a strategy to avoid "naturalizers". My survey of the Mulmuley-Sohoni approach ends with 2 pages on how that may also avoid naturalization.

    ReplyDelete
  9. Typo: "g(n) >> exp(poly(n))" was meant to be "h(n) >> exp(poly(n))", and the "second attraction" ends with a "]" after "output."

    ReplyDelete
  10. Wow, this post got linked to as an authority on describing the contribution of the [Razborov, Rudich] paper by the MAA (http://mathgateway.maa.org/do/ViewMathNews?id=92 -- which can be reached in 2 clicks from http://maa.org).

    ReplyDelete