La máquina de Gelernter

A mitad del siglo XX, con la IA todavía en pañales, no fueron pocos quienes dedicaron sus esfuerzos a intentar crear máquinas inteligentes, máquinas que pudieran hacer tareas de forma parecida a como las realizamos los seres humanos. Los juegos de mesa, como las damas o el ajedrez, fueron una temática recurrente en estos intentos. Por ejemplo, Arthur Samuel inventó una máquina que jugaba razonablemente bien a las damas y que aprendía de cada partida para mejorar su juego, hasta el punto de llegar a ganar a su creador con relativa frecuencia y quedar en posiciones realmente decentes en campeonatos. Pero hoy no vamos a hablar de juegos de mesa, sino que nos vamos a parar en uno de esos intentos de creación de IA que tiene que ver con las matemáticas: la máquina de Gelernter.

La máquina de Gelernter

Herbert Gelernter era un físico que trabajaba en IBM que hacia 1960 creó una máquina con capacidad para deducir teoremas de la geometría euclídea elemental, la Geometry Theorem Prover (GTP), esto es, la Demostradora de Teoremas de Geometría. La GTP funcionaba de atrás a adelante, es decir, a partir del teorema a demostrar el programa iba construyendo diagramas de resultados intermedios hasta llegar a axiomas o a teoremas conocidos. La idea era la siguiente:

Se parte de un conjunto finito de axiomas, \mathbb{A}, y de un conjunto (también finito) inicial de lemas y teoremas. Para cualquier otro teorema T, cuyas hipótesis fueran H_1, \ldots , H_k y cuya conclusión fuera C, lo que se hace es partir del objetivo, C, y construir subobjetivos que lleguen a C mediante la aplicación de alguno de los axiomas o resultados iniciales. Después damos un nuevo paso hacia atrás para cada uno de esos subobjetivo, encontrando sub-subobjetivos, y así sucesivamente. Si en algún momento una parte del diagrama termina en un conjunto de resultados entre los que se encuentran únicamente algunas de las hipótesis del teorema y axiomas y resultados conocidos, entonces se dice que el teorema T está probado.

Es fácil adivinar que la cantidad de casos posibles a estudiar crece enormemente en cada paso del razonamiento, y también que gran parte de ellos pueden desecharse por ser caminos que no nos llevan a ninguna demostración. Para ayudar a GTP a enfocar mejor el problema, Gelernter añadió la posibilidad de comprobar numéricamente algún caso particular del teorema en cuestión, desechándolo en el caso de que estos casos particulares fallaran. Al parecer esta funcionalidad proporcionó a GTP una gran capacidad para encontrar demostraciones conocidas de teoremas relacionados con la geometría euclídea.

Pero lo más sorprendente no fue eso, sino que la máquina consiguió encontrar una elegante y tremendamente ingeniosa demostración de un teorema, conocido como pons asinorum, de la que el creador no tenía constancia.

El teorema tiene una enunciado bien sencillo:

Los ángulos opuestos a los lados iguales de un triángulo isósceles son iguales.

Es decir, si tenemos un triángulo isósceles donde el lado desigual es la base, como éste

entonces los ángulos \alpha y \beta son iguales.

La demostración habitual de este resultado suele realizarse dibujando la altura sobre el lado desigual, dividiendo así el triángulo en dos mitades simétricas, con lo que se ve claramente que esos dos ángulos son iguales. Pero la demostración encontrada por GTP no necesitó del trazado de ninguna línea. El razonamiento de GTP fue más o menos el siguiente:

Consideramos el triángulo inicial, \triangle ABC, y el triángulo resultante de reflejar éste en un espejo, \triangle ACB

Como los dos triángulos tienes los lados iguales, entonces dichos triángulos con congruentes (lado-lado-lado), esto es, son el mismo triángulo, por lo que los ángulos que se forman en la base son iguales.

Parece una demostración muy evidente, pero no está de más recordar que la encontró una máquina, un programa y que, aunque la demostración no era desconocida para la geometría (ya Pappus en el 300 a.C. la había encontrado) sí que lo era para el creador de la máquina.

¿Significaba esto que la máquina era inteligente (signifique ese término lo que signifique)? Bueno, puede ser, la máquina encontró una demostración por sí misma, ya que el creador de dicha máquina no conocía dicha demostración…

…al menos conscientemente. Gelernter no pudo dejar plasmadas de forma consciente todas las pautas necesarias para encontrar dicha demostración, pero sí es cierto que lo podía haber hecho inconscientemente. Es decir, podría ser que Gelernter tuviera ocultos, de forma inconsciente, los mecanismos necesarios para formar dicha demostración y la máquina simplemente se dedicó a extraer dicho conocimiento. Tiene sentido, ¿verdad? Las operaciones realizadas por el programa no podían salirse de las ideas que impregnaban al programa en si, y esas ideas estaban en su creador, aunque él no tuviera conciencia de las mismas.

Por ello parece que la opción más verosímil es pensar que la máquina de Gelernter, por desgracia (o por suerte, quién sabe), no podía considerarse como un especialista en geometría, como llamaríamos a una persona que se dedicara al mismo trabajo que ella, sobre todo teniendo en cuenta que el hecho de encontrar esta demostración fue un caso aislado. Otro tema hubiese sido todo esto si la máquina de Gelernter hubiese continuado encontrando demostraciones ingeniosas y (relativamente) originales de resultados geométricos, pero no fue el caso. Una lástima (¿o un alivio?).


Fuentes:

  • Gödel, Escher, Bach. Un eterno y grácil bucle, de Douglas R. Hofstadter.
  • Roger Penrose’s Gravitonic Brains. A Review of Shadows of the Mind by Roger Penrose, de Hans Moravec.
  • Robots, After All, de Hans Moravec.
  • Artificial Intelligence: A Modern Approach, de Stuart Russell y Peter Norvig.
  • Artificial Intelligence and Symbolic Mathematical Computation en Google Books.

Los textos de Moravec y el de Russell y Norvig son pdfs que tengo por aquí, pero no recuerdo de dónde los descargué.


Esta es mi segunda aportación a la Edición 3,141 del Carnaval de Matemáticas, que en esta ocasión organiza DesEquiLIBROS.


Share

13 comentarios

  1. Trackback | 25 abr, 2012

    La máquina de Gelernter

  2. Vallejo | 25 de abril de 2012 | 11:47

    Vótalo Thumb up 0

    Aunque no tenga mucho que ver, en el 96, Will McCune encontró una demostración de una conjetura mediante deducción automática (es decir, la encontró el ordenador con un demostrador automático diseñado por su equipo). No es tan gráfico como la geometría pero es interesante. Me parece que fue la primera vez en la historia que una máquina hizo una demostración de un teorema nuevo de manera deductiva.

  3. Trackback | 25 abr, 2012

    Bitacoras.com

  4. Christian | 25 de abril de 2012 | 13:04

    Vótalo Thumb up 0

    Interesante.

  5. Fractalon | 25 de abril de 2012 | 18:56

    Vótalo Thumb up 0

    Existen algunos ejemplos interesantes más, como la demostración del teorema de los cuatro colores o del teorema de Kepler.

  6. gaussianos | 25 de abril de 2012 | 21:56

    Vótalo Thumb up 0

    Fractalon, creo que esos ejemplos son más bien aplicación de los ordenadores a la demostración de ciertos resultados. La máquina de Gelernter generaba “ella sola” las demostraciones. Creo que hay diferencia.

  7. Trackback | 26 abr, 2012

    La máquina de Gelernter

  8. Octavio | 26 de abril de 2012 | 04:02

    Vótalo Thumb up 0

    También está el trabajo de Doron Zeilberger. En

    http://www.math.rutgers.edu/~zeilberg/mamarim/mamarimhtml/collatz.html

    muestra un programa en Maple que reprodujo unos teoremas relacionados con la conjetura de Collatz de matemáticos humanos y descubrió muchísimos más (y los escribió en lenguaje comprensible para humanos).

    Igual están los de TheoryMine (http://theorymine.co.uk) que usan un demostrador automático para vender teoremas, y que garantizan que son originales y no triviales. Dicen, pero no he comprado uno para averiguarlo.

  9. Vallejo | 26 de abril de 2012 | 10:37

    Vótalo Thumb up 0

    Lo de Will McCune (QEPD, me enteré cuando quise documentar mi comentario) es una máquina de inferencia, no una herramienta para evaluar millones de combinaciones (como en la “demostración” de la coloración de mapas). De hecho, genera lemas y los utiliza como apoyo para sus demostraciones, alguno de esos resultados intermedios pueden ser más cortos y elegantes que el mismo teorema a demostrar.
    Aparte, no hace falta comprártelo, si os interesa el tema, tiene para descargar el demostrador OTTER con el que probó la conjetura que no había sido demostrada antes. Por otra parte, en el 96-98 se realizaba una competición de demostradores automáticos (no sé si continuó después), y hay demostradores muy potentes como Waldmeister (del Max Plank Institute) o el demostrador FIESTA (del LSI de la UPC)… Me parece que, al aparecer en publicaciones de reconocimiento mundial, se puede acceder a ellos sin comprarlos. Lo único es que hay que conocer la sintaxis para expresar los axiomas.

  10. Pastafrola | 27 de abril de 2012 | 19:32

    Vótalo Thumb up 0

    Un sistema axiomático claramente tampoco puede salirse de los límites implícitos impuestos por sus axiomas, y sin embargo puede generar la totalidad de los teoremas demostrables (en dicho sistema, claro).

    No hay que subestimar el poder de las técnicas combinatorias para lograr resultados nuevos y complementar la limitadísima capacidad de la mente humana.

  11. Trackback | 2 may, 2012

    La máquina de Gelernter

  12. Marian | 18 de mayo de 2012 | 03:05

    Vótalo Thumb up 0

    Un excelente ejemplo del poder de la manipulación a nivel sintáctica! Y también de los problemas con los que se encuentra un programa al intentar resolver cualquier tarea de esta índole de una manera muy naive.

  13. Trackback | 26 jul, 2012

    Gaussianos cumple 6 años de vida - Gaussianos | Gaussianos

Escribe un comentario

Puedes utilizar código LaTeX para insertar fórmulas en los comentarios. Sólo tienes que escribir
[latex]código-latex-que-quieras-insertar[/latex]
o
$latex código-latex-que-quieras-insertar$.

Si tienes alguna duda sobre cómo escribir algún símbolo puede ayudarte la Wikipedia. Utiliza la Vista Previa antes de publicar tu comentario para asegurarte de que las fórmulas están correctamente escritas.