Razonamiento automatizado

En informática , en particular en la representación del conocimiento, el razonamiento y la metalógica , el área del razonamiento automatizado se dedica a comprender diferentes aspectos del razonamiento . El estudio del razonamiento automatizado ayuda a producir programas informáticos que permiten a las computadoras razonar de forma completa o casi completa automáticamente. Si bien el razonamiento automatizado se considera un subcampo de la inteligencia artificial , también tiene conexiones con la informática teórica y la filosofía .

Las subáreas más desarrolladas del razonamiento automatizado son la demostración automatizada de teoremas (y el subcampo menos automatizado pero más pragmático de la demostración interactiva de teoremas ) y la verificación automatizada de pruebas (considerada como un razonamiento correcto garantizado bajo supuestos fijos). También se ha realizado un extenso trabajo en el razonamiento por analogía utilizando inducción y abducción . ^{[ 1 ]}

Otros temas importantes incluyen el razonamiento bajo incertidumbre y el razonamiento no monótono . Una parte fundamental del campo de la incertidumbre es la argumentación, donde se aplican restricciones adicionales de minimalidad y consistencia, además de la deducción automatizada más estándar. El sistema OSCAR de John Pollock es un ejemplo de un sistema de argumentación automatizada que va más allá de ser un simple demostrador automático de teoremas.

Las herramientas y técnicas del razonamiento automatizado incluyen la lógica y el cálculo clásicos , la lógica difusa , la inferencia bayesiana , el razonamiento con entropía máxima y muchas técnicas ad hoc menos formales .

En la década de 2020, para mejorar la capacidad de los grandes modelos de lenguaje para resolver problemas complejos, los investigadores de IA diseñaron modelos de lenguaje de razonamiento que pueden dedicar tiempo adicional al problema antes de generar una respuesta ^{[ 2 ]} y arquitecturas neurosimbólicas que utilizan sistemas de razonamiento simbólico para prevenir alucinaciones . ^{[ 3 ] [ 4 ] [ 5 ]}

El desarrollo de la lógica formal desempeñó un papel fundamental en el campo del razonamiento automatizado, que a su vez impulsó el desarrollo de la inteligencia artificial . Una demostración formal es aquella en la que cada inferencia lógica se ha contrastado con los axiomas fundamentales de las matemáticas. Se proporcionan todos los pasos lógicos intermedios, sin excepción. No se recurre a la intuición, aunque la traducción de la intuición a la lógica sea rutinaria. Por lo tanto, una demostración formal es menos intuitiva y menos propensa a errores lógicos. ^{[ 6 ]}

Algunos consideran que la reunión de verano de Cornell de 1957, que congregó a numerosos lógicos e informáticos, fue el origen del razonamiento automatizado o deducción automatizada . ^{[ 7 ]} Otros afirman que comenzó antes con el programa Logic Theorist de Newell, Shaw y Simon de 1955, o con la implementación del procedimiento de decisión de Presburger por Martin Davis en 1954 (que demostró que la suma de dos números pares es par). ^{[ 8 ]}

El razonamiento automatizado, si bien es un área de investigación importante y popular, sufrió un « invierno de la IA » en los años ochenta y principios de los noventa. Sin embargo, el campo se revitalizó posteriormente. Por ejemplo, en 2005, Microsoft comenzó a utilizar tecnología de verificación en muchos de sus proyectos internos y planea incluir un lenguaje de especificación y verificación lógica en su versión de Visual C de 2012. ^{[ 7 ]}

Principia Mathematica fue una obra fundamental en lógica formal escrita por Alfred North Whitehead y Bertrand Russell . Su propósito era derivar todas o algunas de las expresiones matemáticas en términos de lógica simbólica . Principia Mathematica se publicó inicialmente en tres volúmenes en 1910, 1912 y 1913. ^{[ 9 ]} Sucedió a The Principles of Mathematics , un libro de 1903 de Bertrand Russell , en el que Russell había presentado su famosa paradoja y defendido su tesis de que las matemáticas y la lógica son idénticas.

Logic Theorist (LT) fue el primer programa desarrollado en 1956 por Allen Newell , Cliff Shaw y Herbert A. Simon para "imitar el razonamiento humano" en la demostración de teoremas y se demostró con cincuenta y dos teoremas del capítulo dos de Principia Mathematica, demostrando treinta y ocho de ellos. ^{[ 10 ]} Además de demostrar los teoremas, el programa encontró una demostración para uno de ellos que era más elegante que la proporcionada por Whitehead y Russell. Después de un intento fallido de publicar sus resultados, Newell, Shaw y Herbert informaron en su publicación de 1958, The Next Advance in Operation Research :

"Actualmente existen en el mundo máquinas que piensan, aprenden y crean. Además, su capacidad para realizar estas tareas aumentará rápidamente hasta que (en un futuro previsible) el abanico de problemas que puedan resolver sea tan extenso como el que ha abarcado la mente humana." ^{[ 11 ]}

Ejemplos de demostraciones formales

Demostrador del teorema de Boyer-Moore (NQTHM)

El diseño de NQTHM estuvo influenciado por John McCarthy y Woody Bledsoe. Iniciado en 1971 en Edimburgo, Escocia, se trataba de un demostrador de teoremas totalmente automático construido con Pure Lisp . Los aspectos principales de NQTHM fueron:

1. el uso de Lisp como lógica de trabajo.
2. la dependencia de un principio de definición para funciones recursivas totales.
3. el uso extensivo de la reescritura y la "evaluación simbólica".
4. una heurística de inducción basada en el fallo de la evaluación simbólica. ^{[ 16 ] [ 17 ]}

Luz HOL

Escrito en OCaml , HOL Light está diseñado para tener una base lógica simple y limpia, y una implementación despejada. Es esencialmente otro asistente de prueba para la lógica clásica de orden superior. ^{[ 18 ]}

Rocq

Desarrollado en Francia, Rocq es otro asistente de demostración automatizado que puede extraer automáticamente programas ejecutables a partir de especificaciones, ya sea en formato Objective CAML o código fuente Haskell . Las propiedades, los programas y las demostraciones se formalizan en el mismo lenguaje, denominado Cálculo de Construcciones Inductivas (CIC). ^{[ 19 ]}

El razonamiento automatizado se ha utilizado con mayor frecuencia para construir demostradores automáticos de teoremas. Sin embargo, a menudo, los demostradores de teoremas requieren cierta guía humana para ser efectivos y, por lo tanto, generalmente se clasifican como asistentes de demostración . En algunos casos, dichos demostradores han ideado nuevos enfoques para demostrar un teorema. Logic Theorist es un buen ejemplo de esto. El programa encontró una demostración para uno de los teoremas de Principia Mathematica que fue más eficiente (requiriendo menos pasos) que la demostración proporcionada por Whitehead y Russell. Los programas de razonamiento automatizado se están aplicando para resolver un número creciente de problemas en lógica formal, matemáticas y ciencias de la computación, programación lógica , verificación de software y hardware, diseño de circuitos y muchos otros. El TPTP (Sutcliffe y Suttner 1998) es una biblioteca de tales problemas que se actualiza de forma regular. También hay una competencia entre demostradores automáticos de teoremas que se lleva a cabo regularmente en la conferencia CADE (Pelletier, Sutcliffe y Suttner 2002); Los problemas para la competición se seleccionan de la biblioteca TPTP. ^{[ 20 ]}

• Aprendizaje automático automatizado (AutoML)
• Demostración automatizada de teoremas
• Razonador semántico
• Análisis de programas (informática)
• Aplicaciones de la inteligencia artificial
• Esquema de la inteligencia artificial
• Casuística • Razonamiento basado en casos
• razonamiento abductivo
• Motor de inferencia
• razonamiento de sentido común

• Taller internacional sobre la implementación de lógicas
• Ciclo de talleres sobre temas con éxito empírico en razonamiento automatizado.