Formal Methods Ai.png

A medida que los sistemas autónomos y la inteligencia artificial se vuelven cada vez más comunes en la vida diaria, están surgiendo nuevos métodos para ayudar a los humanos a comprobar que estos sistemas se comportan como se espera. Un método, llamado especificaciones formales, utiliza fórmulas matemáticas que pueden traducirse a expresiones de lenguaje natural. Algunos investigadores afirman que este método se puede utilizar para explicar las decisiones que tomará una IA de una manera que sea interpretable para los humanos.

Los investigadores del Laboratorio Lincoln del MIT querían comprobar tales afirmaciones de interpretabilidad. Sus hallazgos apuntan a lo contrario: las especificaciones formales no parecen ser interpretables por los humanos. En el estudio del equipo, se pidió a los participantes que comprobaran si el plan de un agente de IA tendría éxito en un juego virtual. Cuando se les presentó la especificación formal del plan, los participantes acertaron menos de la mitad de las veces.

«Los resultados son malas noticias para los investigadores que han estado afirmando que los métodos formales otorgan interpretabilidad a los sistemas. Podría ser cierto en algún sentido restringido y abstracto, pero no para nada parecido a la validación práctica de un sistema», dice Hosea Siu, investigador del laboratorio Grupo de tecnología de IA. Los grupos papel fue aceptado en la Conferencia Internacional 2023 sobre Robots y Sistemas Inteligentes celebrada a principios de este mes.

La interpretabilidad es importante porque permite a los humanos confiar en una máquina cuando se utiliza en el mundo real. Si un robot o una IA pueden explicar sus acciones, entonces los humanos podrán decidir si necesitan ajustes o si se puede confiar en que tomarán decisiones justas. Un sistema interpretable también permite a los usuarios de la tecnología (no sólo a los desarrolladores) comprender y confiar en sus capacidades. Sin embargo, la interpretabilidad ha sido durante mucho tiempo un desafío en el campo de la IA y la autonomía. El proceso de aprendizaje automático ocurre en una «caja negra», por lo que los desarrolladores de modelos a menudo no pueden explicar por qué o cómo un sistema llegó a una determinada decisión.

«Cuando los investigadores dicen ‘nuestro sistema de aprendizaje automático es preciso’, preguntamos ‘¿cuán preciso es?’ y ‘¿usando qué datos?’ «Y si no se proporciona esa información, rechazamos la afirmación. No hemos estado haciendo mucho cuando los investigadores dicen que ‘nuestro sistema de aprendizaje automático es interpretable’, y debemos comenzar a someter esas afirmaciones a un mayor escrutinio», dice Siu. .

Perdido en la traducción

Para su experimento, los investigadores intentaron determinar si las especificaciones formales hacían que el comportamiento de un sistema fuera más interpretable. Se centraron en la capacidad de las personas para utilizar dichas especificaciones para validar un sistema, es decir, para comprender si el sistema siempre cumplió con los objetivos del usuario.

La aplicación de especificaciones formales para este fin es esencialmente un subproducto de su uso original. Las especificaciones formales son parte de un conjunto más amplio de métodos formales que utilizan expresiones lógicas como marco matemático para describir el comportamiento de un modelo. Debido a que el modelo se basa en un flujo lógico, los ingenieros pueden utilizar «verificadores de modelos» para probar matemáticamente hechos sobre el sistema, incluso cuándo es posible o no que el sistema complete una tarea. Ahora, los investigadores están intentando utilizar este mismo marco como herramienta traslacional para los humanos.

«Los investigadores confunden el hecho de que las especificaciones formales tengan una semántica precisa con el hecho de que sean interpretables para los humanos. No son lo mismo», dice Siu. «Nos dimos cuenta de que casi nadie estaba comprobando si la gente realmente entendía los resultados».

En el experimento del equipo, se pidió a los participantes que validaran un conjunto bastante simple de comportamientos con un robot jugando a capturar la bandera, respondiendo básicamente a la pregunta «Si el robot sigue exactamente estas reglas, ¿siempre gana?».

Los participantes incluyeron tanto expertos como no expertos en métodos formales. Recibieron las especificaciones formales de tres maneras: una fórmula lógica «en bruto», la fórmula traducida a palabras más cercanas al lenguaje natural y un formato de árbol de decisiones. Los árboles de decisión, en particular, a menudo se consideran en el mundo de la IA como una forma interpretable por humanos de mostrar la toma de decisiones de la IA o los robots.

Los resultados: «El rendimiento de la validación en general fue bastante terrible, con alrededor del 45 por ciento de precisión, independientemente del tipo de presentación», dice Siu.

Con confianza equivocado

Aquellos previamente capacitados en especificaciones formales solo obtuvieron resultados ligeramente mejores que los novatos. Sin embargo, los expertos informaron mucha más confianza en sus respuestas, independientemente de si eran correctas o no. En general, la gente tendía a confiar demasiado en la exactitud de las especificaciones que se les presentaban, lo que significaba que ignoraban los conjuntos de reglas que permitían pérdidas en el juego. Este sesgo de confirmación es particularmente preocupante para la validación del sistema, dicen los investigadores, porque es más probable que las personas pasen por alto los modos de falla.

«No creemos que este resultado signifique que debamos abandonar las especificaciones formales como una forma de explicar los comportamientos del sistema a las personas. Pero sí creemos que se necesita mucho más trabajo en el diseño de cómo se presentan a las personas y en el flujo de trabajo en el que la gente los utiliza», añade Siu.

Al considerar por qué los resultados fueron tan pobres, Siu reconoce que incluso las personas que trabajan con métodos formales no están lo suficientemente capacitadas para verificar las especificaciones como les pidió el experimento. Y es difícil pensar en todos los resultados posibles de un conjunto de reglas. Aun así, los conjuntos de reglas mostrados a los participantes eran breves, equivalentes a no más de un párrafo de texto, «mucho más cortos que cualquier cosa que encontrarías en cualquier sistema real», dice Siu.

El equipo no intenta vincular sus resultados directamente con el desempeño de los humanos en la validación de robots del mundo real. En lugar de ello, pretenden utilizar los resultados como punto de partida para considerar qué puede faltar a la comunidad lógica formal cuando afirma que es interpretable y cómo dichas afirmaciones pueden desarrollarse en el mundo real.

Esta investigación se realizó como parte de un proyecto más amplio en el que Siu y sus compañeros de equipo están trabajando para mejorar la relación entre robots y operadores humanos, especialmente aquellos en el ejército. El proceso de programación de robótica a menudo puede dejar a los operadores fuera del circuito. Con el objetivo similar de mejorar la interpretabilidad y la confianza, el proyecto intenta permitir que los operadores enseñen tareas a los robots directamente, de manera similar a entrenar a los humanos. Un proceso de este tipo podría mejorar tanto la confianza del operador en el robot como su adaptabilidad.

En última instancia, esperan que los resultados de este estudio y su investigación en curso puedan mejorar la aplicación de la autonomía, a medida que se integra más en la vida humana y la toma de decisiones.

«Nuestros resultados impulsan la necesidad de realizar evaluaciones humanas de ciertos sistemas y conceptos de autonomía e IA antes de que se hagan demasiadas afirmaciones sobre su utilidad con los humanos», añade Siu.