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, , y de un conjunto (también finito) inicial de lemas y teoremas. Para cualquier otro teorema , cuyas hipótesis fueran y cuya conclusión fuera , lo que se hace es partir del objetivo, , y construir subobjetivos que lleguen a 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 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 y 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, , y el triángulo resultante de reflejar éste en un espejo,

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.