Verificación del agente

Los fundamentos teóricos de los agentes artificiales (inorgánicos) surgieron a mediados del siglo XX, con el establecimiento de la cibernética y la inteligencia artificial . El artículo de Oliver Selfridge de 1958, «Pandemonium: A Paradigm for Learning», fue una importante contribución teórica temprana para el establecimiento de la arquitectura orientada a agentes. Las implementaciones prácticas de agentes para aplicaciones del mundo real comenzaron a generalizarse en la década de 1990, tras la introducción del modelo de software de creencia-deseo-intención (BDI) y la programación orientada a agentes . Los agentes puramente digitales se implementaron en la infraestructura informática para fines como la monitorización, mientras que los agentes conectados a sensores y actuadores del mundo real se utilizaron cada vez más en sistemas de control industrial . ^{[ 1 ] [ 4 ] [ 5 ]}

Aunque el concepto de agentes artificiales estuvo entrelazado con los primeros estudios de inteligencia artificial desde el principio, los primeros agentes carecían de capacidades de razonamiento de propósito general, a menudo solo tenían una lógica simple de tipo " si... entonces... ". Incluso un dispositivo tan simple como un termostato , que tiene un sensor y un medio para actuar, puede considerarse un protoagente en este sentido. Verificar el comportamiento de un sistema simple de un solo agente no suele ser especialmente difícil, pero puede ser diferente cuando varios agentes simples coexisten en el mismo sistema. El trabajo de Craig Reynolds sobre los boids demostró que un comportamiento relativamente complejo e "inteligente" puede surgir de varios de estos agentes simples que trabajan juntos en un sistema multiagente (MAS). Para la década de 1990, incluso el comportamiento de un sistema de un solo agente podía ser a veces bastante complejo; de acuerdo con el modelo de software de Creencia-deseo-intención , los agentes podían tener creencias que podían evolucionar con el tiempo. Se introdujeron cada vez más agentes controlados por modelos de árboles de decisión bastante grandes , que presentaban nuevas vulnerabilidades a los ataques adversarios . Se hacía cada vez más evidente que los métodos tradicionales de verificación de software tenían limitaciones para probar dichos agentes, o incluso para el tipo de agentes más primitivos cuando se desplegaban como parte de un MAS. ^{[ 4 ] [ 3 ] [ 1 ]}

Fue el uso de agentes para sistemas de control industrial, a veces asociado con la robótica , lo que impulsó la verificación de agentes. Las pruebas informales podrían ser aceptables para agentes digitales utilizados, por ejemplo, para supervisar si cada ordenador de una organización cuenta con la licencia adecuada. Sin embargo, ante el creciente potencial de que agentes defectuosos provoquen fallos que podrían causar un gran incendio en una planta química, una operación médica fallida o incluso un accidente aéreo, se consideró urgente desarrollar métodos fiables para verificar el comportamiento de dichos agentes. La Fundación para Agentes Físicos Inteligentes se creó en 1996. Desde finales de los 90, un número creciente de científicos de la industria y la universidad comenzó a trabajar en el problema, publicando artículos sobre la verificación de sistemas de uno y varios agentes. Gran parte de este trabajo demostró cómo las técnicas de verificación formal, como la comprobación de modelos, podían utilizarse para garantizar que los sistemas basados ​​en agentes cumplieran con sus especificaciones. Una revisión sistemática de 2018, que abarcó 231 estudios, concluyó que la comprobación de modelos era la técnica más común para la verificación de agentes, siendo la demostración de teoremas el segundo método de verificación formal más utilizado. En las dos primeras décadas del siglo XX, los agentes controlados por IA se hicieron más comunes, siendo Siri y Alexa ejemplos bien conocidos. Pero dichos agentes aún carecían de capacidades de razonamiento general y no planteaban nuevos problemas apremiantes para la verificación de agentes. ^{[ 6 ] [ 4 ] [ 3 ] [ 1 ]}

La llegada de los LLM generó un enorme potencial para el uso de agentes artificiales, ya que los agentes basados ​​en ellos podrían tener capacidades cognitivas de propósito general. Los agentes que utilizan LLM (y ocasionalmente modelos que no son LLM ) presentan una vulnerabilidad similar a los ataques adversarios que aquellos que utilizan modelos de árboles de decisión. El mayor alcance de las acciones de los agentes LLM ha creado nuevos desafíos para su verificación, que van más allá de los que presentan los agentes clásicos. Por ejemplo, la red neuronal del LLM le otorga dominios infinitos , un desafío particular para las técnicas tradicionales de verificación formal. Los académicos comenzaron a estudiar los problemas relacionados con la verificación de agentes LLM a partir de 2018. El despliegue de dichos agentes comenzó a acelerarse a finales de 2023 tras la disponibilidad de la API de "llamada a funciones" de OpenAI, y especialmente después de la introducción por parte de Anthropic , a finales de 2024, del Protocolo de Contexto de Modelo (MCP), una forma estandarizada para que los agentes LLM adquieran conciencia contextual y actúen en el mundo mediante la llamada a diversas herramientas externas. El rápido despliegue de agentes LLM tras el lanzamiento de MCP ha hecho que la tarea de verificación de agentes reciba mayor atención tanto en el ámbito académico como en el sector privado. En 2024 y 2025 se fundaron varias startups centradas en la verificación de agentes LLM en Europa y Estados Unidos para satisfacer la creciente demanda. ^{[ 2 ] [ 4 ] [ 3 ] [ 7 ]}

La verificación formal implica demostrar la corrección de algunos o todos los aspectos de un sistema mediante métodos matemáticos. Estos métodos pueden abarcar desde la prueba formal manual hasta la verificación asistida por demostradores de teoremas automatizados como Isabelle . Para la verificación de agentes, la comprobación de modelos es, con diferencia, el método de verificación formal más utilizado; para los modelos anteriores a LLM, a menudo se complementaba con técnicas que utilizaban lógica de árbol de computación . Otro método común es la demostración de teoremas . La verificación formal proporciona un mayor grado de confianza que los métodos informales, pero no siempre se utiliza, incluso cuando es posible. A veces, una persona u organización que desarrolla agentes de software no tendrá las habilidades necesarias, o puede que no considere que merezca la pena el esfuerzo si el/los agente(s) no tienen la capacidad de causar mucho daño incluso si funcionan mal. Cuando los agentes se implementan en sistemas donde los errores podrían tener graves consecuencias, la capacidad de los métodos de verificación formal para proporcionar certeza matemática tiende a ser muy preferida tanto por los reguladores como por los propios diseñadores. Pero incluso para sistemas de alto impacto, la verificación formal puede ser un desafío. ^{[ 3 ] [ 1 ] [ 6 ]}

Los desarrolladores pueden intentar diseñar sistemas basados ​​en agentes de manera que sea más fácil verificar formalmente más de sus propiedades. Esto se puede lograr tanto diseñando específicamente la estructura del agente del modelo cognitivo central que lo controla, como, en el caso de los LLM u otros modelos fundamentales, modificando el entrenamiento. Un ejemplo del enfoque orientado a la estructura ha sido la introducción de agentes gobernadores o árbitros, que pueden vetar acciones iniciadas por un modelo de toma de decisiones central más complejo. Los agentes gobernadores tienden a ser relativamente simples y, por lo tanto, más fáciles de verificar formalmente. Si bien este enfoque se ha utilizado desde al menos 2009, su perfeccionamiento después de 2018 con el paradigma LLM-as-a-Judge ha hecho que gane importancia. Sin embargo, incluso con estas técnicas, la verificación formal no siempre es factible. El costo computacional involucrado puede ser prohibitivo (ya que podría requerir centros de datos completos de computadoras para funcionar durante varios años). Puede ser que las matemáticas necesarias sean muy difíciles incluso de formular. Por ejemplo, incluso para agentes simples en un MAS, si un número indeterminado de agentes puede unirse al sistema en tiempo de ejecución, el problema generalmente es indecidible, aunque existen soluciones para casos específicos. Más aún en el caso de agentes LLM, aspectos de su verificación pueden ser completamente indecidibles mediante matemáticas formales, o al menos NP-difíciles . En consecuencia, la verificación formal a menudo se complementa con métodos informales. ^{[ 1 ] [ 7 ] [ 8 ] [ 3 ]}

Se pueden utilizar diversos métodos informales para evaluar agentes, siendo la inspección de software y la evaluación heurística algunos de los más informales, pero que a menudo requieren mucha habilidad por parte de los evaluadores para lograr un alto grado de seguridad, excepto en casos triviales donde solo se necesita evaluar una pequeña cantidad de código simple. La disciplina de las pruebas de software incluye otras formas de prueba que, si bien no requieren el rigor matemático de las pruebas formales, a menudo se llevan a cabo de manera relativamente estructurada, por ejemplo, las pruebas funcionales . Sin embargo, para la verificación de agentes, un desafío importante con los métodos informales tradicionales es la dificultad de escribir casos de prueba que cubran todos los escenarios posibles que surgen. Cuando diferentes agentes deben interactuar para lograr los objetivos generales del sistema, el número de permutaciones puede llegar a ser extremadamente alto, incluso si todos los agentes son individualmente bastante simples. Complementar los métodos tradicionales de verificación de software con la verificación en tiempo de ejecución ^{[ nota 1 ]} puede aumentar aún más la confianza en que un sistema basado en agentes cumple con la especificación. ^{[ 11 ] [ 1 ]}