10 de agosto de 2010

Una prueba de que P ≠ NP?

Desde hace unos días Vinay Deolalikar ha creado un gran revuelo en la comunidad científica al liberar un borrador de una prueba de que P ≠ NP. La pregunta de si P es igual o distinto a NP es uno de los problemas no resueltos más importante de las ciencias de la computación (y las matemáticas), por lo tanto, el borrador de Vinay ha tenido a la comunidad científica ocupada tratando de verificar sus 102 páginas.

Por mi parte sólo estoy tratando de seguir las discusiones, no creo ser la persona capacitada para analizar la veracidad o falsedad de las afirmaciones de Vinay, así que aquí dejaré algunos links para quienes estén interesados en seguir el debate.

Sin dudas los posts en el blog de Dick Lipton son los más interesantes:
También hay un intento de ordenar la discusión por medio de una Wiki en el sitio de Michael Nielsen.

A pesar de los problemas marcados, aún no hay un "veredicto" definitivo de la comunidad científica, más allá de alguna apuesta, la mayoría coincide en que la prueba puede ser correcta, o al menos llevar a un razonamiento correcto, con los errores esperables en un borrador tan largo en un problema tan complejo y lo que todos coinciden, es en que es un muy buen trabajo y tiene resultados interesantes, aún si la prueba de P ≠ NP resultase errónea.

Update 11/08/10: Un nuevo post en el blog de Dick Lipton trata de tirar más luz al asunto: La idea es pedirle a Vinay que muestre cómo usar sus resultados para resolver problemas más sencillos, de los cuales ya se conoce la solución. Es una buena manera de entender por dónde viene la mano, ya que el paper en sí tiene muchos detalles técnicos y es difícil de seguir incluso por quienes trabajan a diario en complejidad.

Update 11/08/10 (2): Dejo un artículo de divulgación muy bueno que apareció en la revista Nature: Million-dollar problem cracked?

Update 12/08/10: Un nuevo post en el blog de Dick Limpton detalla cuál parece ser el mayor problema en la prueba, y la respuesta de Vinay Deolalikar.

Update 13/08/10: Dick posteó lo que parece ser un error insalvable en la prueba, un error de interpretación por parte de Vinay en el uso de la teoría de modelos finita: Fatal Flaws in Deolalikar’s Proof?

15 comentarios:

  1. tienes alguna idea de que es "finite model theory"? aparentemente es parte de logica, y tiene como subcampo a la complejidad de Kolmogorov. Segun me cuentan otras personas, muchas clases de complejidad estan completamente caracterizadas por esta logica.

    ResponderEliminar
  2. Pues no, sólo lo que acabo de leer en la Wikipedia. Según el summary que aparece acá, permite una caracterización lógica de las clases de complejidad (supongo que ese tipo de caracterización ha de ser la que usó Vinay en su paper).

    ResponderEliminar
  3. Está mucho más claro en la wiki en español: Teoría de modelos. En el segundo párrafo habla de los finite model theories.

    El resumen es el último párrafo:
    La teoría de modelos se preocupa de lo que se puede probar con sistemas matemáticos dados, y cómo estos sistemas se relacionan entre sí. Se preocupa particularmente de qué sucede cuando tratamos de extender algún sistema agregando nuevos axiomas.

    Las teorías finitas dice que difieren mucho de las infinitas tanto en las técnicas usadas como en los problemas estudiados, pero nos da una idea sobre de qué estamos hablando (lo mismo, pero finito).

    No sé si es de mucha ayuda, pero al menos es una aproximación.

    ResponderEliminar
  4. Realmente por lo poco (por no decir infimo) que pude entender de la "prueba", en particular esto de finite model theory es una de las cosas que me confunde. Segun las wikis que hablan sobre ello, parece tener que ver con computabilidad/Godel/Turing, ya que habla de las implicancias que pueda tener para "provability" o "inconsistency" el agregado o quitado de axiomas. En el problema que nos compete, sabemos que hay computabilidad, pero estamos distinguiendo complejidad (P vs. NP). Ergo, no entiendo un pomo la "prueba".

    ResponderEliminar
  5. Por otro lado, y para generar un poco de revuelo en el blog. YO TAMBIEN DUDO DE LA PRUEBA.

    Viendo este video reflexiono que un teorema tan difícil llevo 300 años para probarse, y eso hizo que la ciencia avance muchísimo, por los "para-esfuerzos" por probar ese teorema. El mismo que lo probo ahora siente pena de haberlo hecho, obvio, cual es su objetivo ahora??

    Realmente pensamos que este problema que nos compete puede ser probado en menos de 40 años?? (contando desde que Cook probo SAT es NP-Completo) Y en adicion, el cambio a la Theoretical Computer Science puede ser muy groso si realmente la prueba se comprueba. Justamente como dice Scott Aaronson: "If P != NP is proved, then to whatever extent theoretical computer science continues to exist at all, it will have a very different character." A pesar de lo que Cook le responde "But Scott, most of us complexity theorists aren’t working on proving P not= NP. The topics appearing in complexity conferences (derandomization, cryptographic security, inapproximability of NP-hard problems, proof complexity …)
    will likely remain at least as relevant after P not= NP is proved.".

    Yo creo que si efectivamente el problema queda "cerrado", a pesar que se podria "en teoria" seguir desarrollando metodos mas rapidos para resolver el TSP o se mejorarian los ataques a algoritmos criptograficos (con la consiguiente mejora de ellos para evitar ser atacados), el impetu no seria el mismo. El mismisimo Deolalikar tendria que sentir "miedito" de haber resuelto el problema, y leyendo las lineas que le mando a los revisores lo noto tan soberbio que seguramente no reparo en revisar el mismo a ver si tenia algun error, como los que aparentemente ya encontraron los demas expertos (en solo unos dias, en 100 paginas!! -- que para nosotros en este blog quiza son mas de 1000, por el background que tendriamos que leer para entenderlo). De hecho, el solo hecho de combinar tantas áreas diferentes para intentar solucionar el problema, y evitar los detalles técnicos en el paper como el autor asume, lleva a pensar en una clara posibilidad de "haberse olvidado de algo", teniendo en cuenta el alto nivel de abstraccion teórica que seguramente hay que tener para entender la prueba (dado el limite de 7 conceptos que uno puede tener en la cabeza a la vez).

    En fin, dudo de la prueba, aunque obviamente el "intento de prueba" es uno de los tantos grandes avances, como mencione casi al comienzo, que se dieron y se seguirán dando gracias a los para-esfuerzos por resolver el problema.

    Se hizo muy largo, entiendo si no quieren responder, o también acepto preguntas por partes particulares que no se entiendan bien.

    Saludos
    Alejandro

    ResponderEliminar
  6. Lo que yo entiendo.... bueno, "entiendo", con comillas incluídas, es que la teoría de modelos sirve para determinar propiedades en estructuras algenraicas y entidades matemáticas en general.

    Según Dick Lipton (primer post) la prueba es así: Hace una caracterización de P usando la teoría de modelos finita. Luego usa un teorema de 1986 que dice

    "En estructuras ordenadas, una relación se define por una fórmula de primer orden más el operador Least Fixed Point (LFP) si y sólo si ésta es computable en tiempo polinomial"

    Entonces toma SAT y crea una estructura ordenada que lo codifica, y dice que si P=NP entonces SAT tendría que cumplir ciertas propiedades de acuerdo al teorema anterior. Luego la prueba muestra de que SAT no cumple con dichas propiedades, por lo que se deduce que P≠NP.

    ResponderEliminar
  7. Leyendo el blog de Dick Lipton (un hasta hace poco fervoroso creyente de que P=NP) veo que los tipos que trabajan en estos temas están muy entusiasmados con la prueba (más allá de Scott y las, para mí, soberbias (i.e. no técnicas) objeciones al paper). Lo que dice en el último post es que quizá se necesite un poco más de trabajo pero que parece estar yendo en la dirección correcta.

    O sea, tu objeción la veo más en línea con las objeciones de Scott, las cuales, a mi entender, no son un buen argumento.

    ResponderEliminar
  8. PD: Mi primer comentario va en respuesta a tu primer comentario y el segundo al segundo :) (ven, para eso estaba bueno el difunto Wave) :P

    ResponderEliminar
  9. Desde ya que no tengo ningún argumento solido, no puedo entender para nada esa prueba, a pesar que desde un alto nivel entiendo mas o menos lo mismo que vos posteaste.
    Obviamente que es mas una cuestión de escepticismo, al mejor estilo Scott Aaronson. De todas formas, yo creo que los que están entusiasmados y tienen esperanzas que la prueba este bien, tampoco tienen argumentos sólidos (como tenerlos si todavía no terminaron de revisarla?), digamos que ellos intuyen lo contrario a mi simplemente por lo mismo que yo, "corazonada". (y perdón por compararme con todos esos capós, es simplemente para dar a entender mi idea :) )
    Lo que pienso es que hay dos opciones:
    La dirección puede ser la correcta, pero seguramente la formulación la tendrá que pulir, considerar casos especiales, dar mas detalles de la codificación, o incluso alguien tendrá que revisar ese teorema de 20 y pico de años, que anda a saber si es correcto en el caso general.
    Por otro lado, quizá ni siquiera la dirección es la correcta, quizá esta bueno plantear esas relaciones entre topología algebraica y lógica/computabilidad, y quizá el tipo hasta creo una nueva rama de investigación, por eso no digo que la prueba en si sea inútil, todo lo contrario, pero dudo que realmente pruebe lo que aclama haber probado.

    De todas formas, esta bueno el solo hecho que ya se este discutiendo, como dijo uno por ahí, le dio un poco de publicidad a esta rama. jeje

    ps: esto contesta mas que nada el segundo post, con una referencia al primero... :)

    ResponderEliminar
  10. Aca esta un link con al wiki del proyecto

    http://michaelnielsen.org/polymath1/index.php?title=Deolalikar's_P!%3DNP_paper

    explica bien cual es la estrategia utilizada y los problemas.

    ResponderEliminar
  11. Ah, bien, entendí. Probablemente tengas razón y haya un montón de errores a ser corregidos. Yo la verdad que ni siquiera he leído el borrador (voy a tratar de hacerlo cuando vuelva de las vacaciones, probablemente sin éxito, veremos), pero me gustó la postura que tomó Dick Limpton de no juzgar el paper hasta no haberlo entendido (bueno, él se puede dar ese lujo ya que eventualmente lo entenderá) y por el contrario no me gustó la apuesta de Scott (en un nuevo post incluso dice que ya ganó la apuesta).
    Mi intuición (no de haber leído el paper sino haber leído a quienes lo leyeron), es que probablemente haya muchos errores (lo que es normal por la longitud del paper) y quizá alguno de ellos no es salvable.

    ResponderEliminar
  12. Agregué un nuevo Update al post con un link a la explicación de Dick del mayor problema que parece tener la prueba, y la respuesta de Vinay.

    ResponderEliminar
  13. " ... (voy a tratar de hacerlo cuando vuelva de las vacaciones, ... "
    Vos tambien estas en Grecia? :p

    O seguis jugando al ping-pong y al bowling? Dale, decile a tu mujer que te deje y pegale una mirada, igual vas a salir asustado como yo!!

    ResponderEliminar
  14. Jaja, sigo meta ping-pong y tenis :) Me propuse en estas vacaciones no tocar nada referente al trabajo (aunque este blog esta demasiado cerca), de todas maneras mi gran análisis probablemente sea un "no entiendo nada". Creo que hay un background muy grande a incorporar y no creo que tenga el tiempo para hacerlo (entro en mi ultimo año de doctorado y tengo muchas cosas que quiero hacer aún, relacionadas a mi tesis) :)

    ResponderEliminar
  15. creo que la comunidad cientifica, y la humanidad en general, deben enfocarse en este campo. Cuando la ciencia descubra los secretos de la paradoja EPR, el mundo que conocemos va a cambiar definitivamente, será un antes y un despues.
    Al margen de las nuevas y extremadamente formidables aplicaciones que le darán al uso de la teletransportación de información, surgirán nuevos descubrimientos relacionados que abrirán un nuevo horizonte a la raza humana.


    saludos.
    Yacteka

    ResponderEliminar