¿Qué es el razonamiento automatizado?
El razonamiento automatizado es el campo de las ciencias de la computación que intenta garantizar lo que un sistema o programa hará o no hará nunca. Esta garantía se basa en pruebas matemáticas. Las personas resuelven numerosos problemas lógicos en matemáticas, ciencias y cálculo por medio de estrategias lógicas, como los teoremas y las deducciones. El razonamiento automatizado utiliza computadoras que emplean las mismas herramientas para resolver retos complejos. Las herramientas de razonamiento automatizado intentan responder a preguntas sobre un programa (o una fórmula lógica) por medio de técnicas matemáticas conocidas. Las herramientas ayudan a comprobar qué hay de cierto en una declaración o expresión.
¿Qué problemas puede resolver el razonamiento automatizado?
Los científicos y los desarrolladores de software utilizan el razonamiento automatizado para demostrar dos cosas. Primero, demuestran que el diseño o la implementación de un sistema obedecen a sus especificaciones. En segundo lugar, demuestran que funciona de la manera en que se pretendía.
El razonamiento automatizado hace esto mediante la producción de pruebas en lógica formal respaldadas por teoremas matemáticos o verdades conocidas. El razonamiento automatizado utiliza métodos matemáticos de verificación algorítmica basados en la lógica para producir pruebas de seguridad o corrección de todos los comportamientos posibles.
El razonamiento automatizado también se puede utilizar para demostrar que los sistemas utilizados para configurar redes, permitir el acceso a la red o conceder permisos, o para mantener la seguridad y privacidad de los datos funcionan según lo previsto.
Cuando utiliza el razonamiento automatizado, primero presenta al sistema un enunciado del problema. Luego, el sistema de razonamiento automatizado calcula y valida las suposiciones de acuerdo al enunciado del problema. El software hace esto hasta agotar todas las opciones.
Ejemplo de problema para el razonamiento automatizado
Para entender mejor el razonamiento automatizado, considere el enunciado del problema ¿Los gatos son animales terrestres? y las siguientes afirmaciones:
- Los gatos son mamíferos
- Los mamíferos son animales terrestres
El sistema de razonamiento automatizado evalúa si el enunciado del problema es correcto. En concreto, utiliza la deducción lógica. En este caso, los gatos son mamíferos y los mamíferos son animales terrestres. Por lo tanto, verificaría que los gatos son animales terrestres.
Limitaciones del razonamiento automatizado
El razonamiento automatizado no hace predicciones ni generalizaciones. Por ejemplo, podemos usar el razonamiento automatizado para producir un argumento como este:
- Los gatos tienen pelo
- Fluffy es un gato
- Así que Fluffy tiene pelo
No podemos usar el razonamiento automatizado para elaborar argumentos como el siguiente:
- Los gatos son mamíferos
- Los gatos son animales terrestres
- Por lo tanto, todos los mamíferos son animales terrestres
Estas aplicaciones son comunes en un demostrador de teoremas, que requiere la orientación humana para realizar tareas de razonamiento deductivo.
¿Cuáles son algunos casos de uso del razonamiento automatizado?
La capacidad del razonamiento automatizado para hacer inferencias lógicas paso a paso es útil en varias áreas. Al utilizar el razonamiento automatizado, puede demostrar las propiedades de seguridad, cumplimiento, disponibilidad, durabilidad y seguridad de las arquitecturas a gran escala.
Estos son algunos otros casos de uso del razonamiento automatizado.
Generación de modelos matemáticos
Científicos, ingenieros y matemáticos resuelven problemas y verifican las demostraciones matemáticas mediante la aplicación de fórmulas algebraicas en aplicaciones científicas. En estas prácticas, utilizan modelos matemáticos que se basan en un buen número de variables para deducir soluciones probables a un problema.
Verificación de hardware
El razonamiento automatizado ayuda a los ingenieros de hardware a crear productos fiables. Les permite descubrir posibles defectos que los métodos de prueba convencionales pasan por alto.
Por ejemplo, los ingenieros de diseño electrónico utilizan rigurosos análisis de razonamiento matemático automatizado para obtener pruebas concluyentes de que un diseño de hardware en particular cumple con sus especificaciones, como los comportamientos o las ejecuciones del sistema.
La verificación muestra que todos los comportamientos posibles del sistema satisfacen las propiedades temporales que componen la especificación. También podría mostrar que cada comportamiento posible de la implementación del sistema es coherente con algún comportamiento de su especificación de alto nivel.
Validación de software
Los desarrolladores de software utilizan el razonamiento automatizado para garantizar que las aplicaciones sean sólidas contra problemas de seguridad no deseados y que el software funcione según lo previsto o diseñado. Al igual que la verificación del hardware, el razonamiento automatizado permite a los desarrolladores validar las medidas de seguridad del software en función de diversas políticas.
Por ejemplo, los ingenieros de Amazon Web Services (AWS) demuestran que el código de arranque es seguro para cada configuración de arranque con un razonamiento automatizado. Otro ejemplo es que demuestran que los datos almacenados y procesados en Amazon Simple Storage Service (Amazon S3) están protegidos. En este ejemplo, se basan en el razonamiento automatizado para la replicación, la coherencia, el escalamiento automático, el equilibrio de carga y otras tareas de coordinación.
Generación de modelos de razonamiento humano
Los informáticos utilizan tecnologías de razonamiento automatizado para configurar el acceso. Para ello, escriben políticas que describen cuándo permitir y denegar las solicitudes de los usuarios para acceder a un recurso. Esto verifica que solo los usuarios previstos tengan acceso al recurso, lo cual es importante para la seguridad y la privacidad del recurso.
Por ejemplo, los informáticos utilizan fórmulas de teorías de satisfacibilidad módulo (SMT) y solucionadores de SMT para demostrar las propiedades de seguridad.
¿Cuáles son algunas de las herramientas y técnicas del razonamiento automatizado?
A continuación, compartimos varios métodos de deducción automatizados que permiten a los sistemas de computación realizar la deducción humana.
Lógica clásica
La lógica clásica es una filosofía matemática que proporciona modelos básicos de razonamiento para programas de razonamiento lógico automatizados. Esta lógica se basa en el principio de que cada proposición tiene un valor de verdad, verdadero o falso, pero no ambos.
Se centra principalmente en la lógica de primer orden, que permite a los matemáticos representar variables desconocidas como x con cuantificadores como hay un en una oración. Por ejemplo, los científicos aplican la lógica clásica en la programación lógica para despejar la x en esta oración: hay un x, ese x es un animal terrestre y x es un mamífero.
Lógica proposicional
La lógica proposicional es un sistema lógico en el que hay proposiciones que pueden ser verdaderas o falsas; la construcción de relaciones entre ellas se llaman argumentos.
La afirmación clásica de un argumento en lógica proposicional es si se da P, entonces se da Q. Por ejemplo, si es sábado, es fin de semana.
El razonamiento automatizado utiliza una técnica llamada resolución SAT. Este razonamiento recurre a herramientas llamadas solucionadores SAT para buscar asignaciones satisfactorias a los argumentos de la lógica proposicional. Esto significa variables que hacen que el argumento sea verdadero.
¿Cuál es la diferencia entre el razonamiento automatizado y la inteligencia artificial?
El razonamiento automatizado es una disciplina específica de la inteligencia artificial (IA) que aplica la deducción lógica a los sistemas de computación.
La IA es una ciencia que enseña a las computadoras a pensar como las personas a la hora de resolver problemas. Los avances recientes en la IA han llevado al avance de varias subdisciplinas, como el aprendizaje profundo, el análisis de datos y el machine learning.
El razonamiento automatizado difiere de otras tecnologías de IA, como el procesamiento de lenguaje natural (NLP), que se centra en entrenar a las computadoras para que entiendan discursos escritos o verbales. En cambio, el razonamiento automatizado utiliza modelos lógicos y pruebas para razonar sobre los posibles comportamientos de un sistema o programa, incluidos los estados a los que puede llegar o nunca alcanzará.
¿Cuál es la diferencia entre el razonamiento automatizado y el aprendizaje profundo?
El razonamiento automatizado demuestra las propiedades de un programa o sistema. Utiliza el programa o sistema en sí, así como un modelo o especificación del sistema en lógica formal.
El aprendizaje profundo hace predicciones basadas en la aplicación de modelos estadísticos a grandes conjuntos de datos.
El aprendizaje profundo es una tecnología avanzada de machine learning que simula el funcionamiento del cerebro humano. Utiliza diferentes modelos de redes neuronales que constan de múltiples capas de neuronas que extraen, comparan y analizan la información relevante. Los científicos de datos utilizan el aprendizaje profundo para aplicaciones complejas, como el procesamiento de datos de cámaras y sensores en vehículos autónomos.
¿El razonamiento automatizado se considera machine learning?
El razonamiento automatizado y el machine learning no son lo mismo. En resumen, el machine learning hace predicciones e inferencias. El razonamiento automatizado proporciona pruebas.
El machine learning es un subconjunto de la IA que entrena a las computadoras para que tomen decisiones con grandes muestras de datos. Por ejemplo, los científicos de datos utilizan el machine learning para entrenar el software bancario a fin de identificar actividades fraudulentas. Utilizan grandes muestras de datos financieros para garantizar que el software identifique con facilidad los patrones anormales basándose en los resultados obtenidos previamente.
En lugar de entrenar el modelo con datos, el razonamiento automatizado permite que el modelo deduzca un resultado basándose en la verdad y la demostración matemáticas.
¿Cómo utiliza AWS el razonamiento automatizado para mejorar las ofertas de servicios?
AWS utiliza el razonamiento automatizado para mejorar varias ofertas de servicios. A continuación, presentamos algunos ejemplos:
- El Revisor de Amazon CodeGuru utiliza el razonamiento automatizado y el machine learning para ayudar a los desarrolladores a identificar las vulnerabilidades del software.
- Amazon Inspector Classic cuenta con una característica de accesibilidad de red que analiza de manera automática las instancias de EC2 para detectar posibles vulnerabilidades de seguridad y configuraciones erróneas.
- El analizador de acceso de AWS Identity and Access Management (IAM) administra los permisos de las cuentas mediante el razonamiento automatizado.
- Reachability Analyzer de Amazon Virtual Private Cloud (Amazon VPC) aplica un razonamiento automatizado para ayudarlo a comprender y visualizar su red de AWS.
Visite Seguridad comprobable para obtener más información sobre el razonamiento automatizado en los servicios de AWS. Utilizamos el razonamiento matemático a fin de ofrecer garantías de seguridad sólidas para sus cargas de trabajo de seguridad.
Para comenzar a beneficiarse de la seguridad de AWS, cree una cuenta hoy mismo.
Siguientes pasos en AWS
Obtenga acceso instantáneo al nivel Gratuito de AWS.
Comience a crear en la consola de administración de AWS.