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