Un potente ordenador muestra capacidad de razonamiento en demostraciones matem¨¢ticas

Los ordenadores son muy r¨¢pidos cuando se trata de ejecutar c¨¢lculos matem¨¢ticos. Pero a la hora de encontrar soluciones creativas para complicados problemas matem¨¢ticos, nada ha podido vencer a la mente humana, hasta ahora. Un programa de ordenador hecho en el Argonne National Laboratory (EE UU) ha presentado una demostraci¨®n matem¨¢tica que ser¨ªa considerada creativ¨¢ si se le hubiera ocurrido a un ser humano. La m¨¢quina ha puesto, por vez primera, un pie en las matem¨¢ticas puras, un campo descrito a menudo como una forma de arte m¨¢s que como una ciencia.

Algunos investigadores se?alan que las consecuencias de este avance son profundas, al mostrar lo poderosos que pueden llegar a ser los ordenadores al razonar, por s¨ª solos, reproducir los destellos de razonamiento l¨®gico o incluso de genio de las mejores mentes humanas.Anteriormente, los ordenado res hab¨ªan dado soluciones a hip¨®tesis matem¨¢ticas pero f¨¢ciles de resolver. En esta ocasi¨®n, la diferencia es que la m¨¢quina ha resuelto una hip¨®tesis que dej¨® sin respuesta a algunos de los mejores matem¨¢ticos durante 60 a?os. Y lo ha logrado con un programa dise?ado para razonar, no para resolver un problema espec¨ªfico. El programa es muy diferente de los de ajedrez, por ejemplo, dise?ados para manejar un ¨²nico problema: los movimientos de una partida'.

"Es un signo de poder, de capacidad para razonar", se?ala Larry Wos, jefe del proyecto del ordenador inteligente en Argonne, logrado por su colega William McCune. Wos vaticina que este ¨¦xito puede marcar el principio del fin de la investigaci¨®n matem¨¢tica tal y como se realiza ahora, ya que, a la larga, puede liberar a los matem¨¢ticos para que se centren en descubrir nuevas hip¨®tesis.

El resultado tambi¨¦n podr¨ªa poner en cuesti¨®n la noci¨®n de razonamiento creativo por la posibilidad de que los ordenadores tomen un camino paralelo para alcanzar las mismas conclusiones que los grandes pensadores humanos. Puede ser que, dado que nadie sabe c¨®mo razonan los humanos, el enorme estallido de creatividad que aparentemente surge como un chispazo de las mentes de los genios sea producto de una labor febril y oculta a nivel inconsciente, similar a la de un ordenador.

Stanley Burris, matem¨¢tico en la Universidad de Waterloo (Canad¨¢), afirma que este resultado ha supuesto "el primer avance verdadero en la demostraci¨®n automatizada de teoremas" y demuestra que "la frontera que separa lo mec¨¢nico de lo creativo es muy delgada".

Sin aplicaciones

Robert Boyer, un cient¨ªfico de computaci¨®n de la Universidad de Texas en Austin, dice: "Creo que es el resultado en la demostraci¨®n automatizada de teoremas m¨¢s notable en los ¨²ltimos 30 a?os y es claramente una forma de razonamiento inform¨¢tico". Pero a?ade, "no quiero concederle excesiva importancia". Es mejor, afirma, pensar en un ordenador "tan s¨®lo como un colega m¨¢s, que a veces sirve de ayuda, pero a menudo, no".Las demostraciones de McCune est¨¢n relacionadas con una hip¨®tesis que "no tiene aplicaciones", se?ala. Su programa de ordenador ha demostrado que un conjunto de tres ecuaciones es equivalente a un ¨¢lgebra de Boole, ese conjunto de normas, conocido por generaciones de estudiantes, que rige las asociaciones, los complementos y las intersecciones entre conjuntos.

El problema fue planteado por primera vez. en los a?os treinta por el matem¨¢tico Herbert Robbins, quien trabaj¨® en, el asunto durante un tiempo y luego lo transmiti¨® a uno de los m¨¢s famosos expertos en l¨®gica matem¨¢tica de este siglo,-Albert Tarski, de la Universidad de Stanford. Tarski, ya fallecido, trabaj¨® en el problema, le dedic¨® un libro y lo plante¨® a colegas.

Burris dice que Tarski le present¨® el problema a principios de los a?os setenta. Mientras tanto, los expertos en computaci¨®n intentaban descubrir s¨ª pod¨ªan hacer que las m¨¢quinas razonasen. Wos empez¨® a trabajar en el razonamiento automatizado en los a?os sesenta, y los investigadores estaban divididos respecto a c¨®mo abordar este asunto.

Algunos cre¨ªan que la clave era explicar c¨®mo razonan las personas y despu¨¦s crear programas que imitasen el proceso. Wos discrepaba. "Nadie sabe c¨®mo razonan los humanos", afirma. "Cuando preguntas a los matem¨¢ticos que han demostrado un teorema c¨®mo lo han hecho, te contestan: 'Bueno... di un mont¨®n de vueltas por casa y estuve leyendo algunos peri¨®dicos y pensando...". .

Conclusiones l¨®gicas

Wos y sus compa?eros siguieron otro diferente,. "No nos preguntamos qu¨¦ hace la gente cuando piensa, sino que nos planteamos c¨®mo explicar a un ordenador de qu¨¦ trata un determinado problema, c¨®mo conseguir que llegue a conclusiones que se derivan inevitables y l¨®gicamente de hip¨®tesis y que, a partir de ah¨ª, demuestre teoremas".Empezaron a escribir programas en los que el ordenador supon¨ªa que una hip¨®tesis era falsa y a continuaci¨®n examinaba las conclusiones. Si encontraba una contradicci¨®n, era una prueba de que la hip¨®tesis era verdadera. El ordenador tambi¨¦n supon¨ªa que la hip¨®tesis era verdadera y se gu¨ªa los mismos pasos, buscando contradicciones que demostrasen que era falsa..

Para evitar que la m¨¢quina se perdiese en largas comprobaciones, los investigadores a?ad¨ªan estrategias, como pasar por alto todos los supuestos que contuviesen m¨¢s de cien s¨ªmbolos. Wos explica: "Yo era jugador de p¨®ker y de bridge. Un buen embaucador utiliza estrategias, descubre cu¨¢l es la debilidad de uno y la ataca. No se limita a intentar enga?arte aleatoriamente

Los programas de Wos pronto fueron capaces de encontrar demostraciones de problemas matem¨¢ticos-b¨¢sicos. "A veces, pod¨ªamos hacer los problemas mejor que los estudiantes y, en algunas ocasiones, muy de vez en cuando, mejor que los profesores", dice. Durante m¨¢s de 16 a?os, se dedic¨® a problemas de libros de texto de matem¨¢ticas y los matem¨¢ticos sol¨ªan decirle: "?Por qu¨¦ haces lo que ya sabernos? ?Por qu¨¦ no nos das algo nuevo?". En 1979, Wos conoci¨® el problema de Robbins e intent¨® solucionarlo con programas cada vez m¨¢s avanzados pero sin ¨¦xito. McCune se uni¨® al grupo en 1984.

El pasado 2 de octubre, McCune introdujo la hip¨®tesis de Robbins en un nuevo programa de razonamiento automatizado que hab¨ªa escrito, llamado EQP (demostrador de ecuaciones) y salieron resultados sorprendentes. McCune intent¨® que el ordenador perfeccionase la demostraci¨®n, arranc¨® el programa el 15 de noviembre y diez d¨ªas despu¨¦s lo logr¨®.

McCune ha comprobado su demostraci¨®n por ordenador y a mano; independientemente lo han hecho Burris y, por su lado, Mark Sticke1, del Instituto de Investigaci¨®n de Standford.

Copyright. The New York Times