🤖 AI

Effect-Transparent Governance for AI Workflow Architectures: Semantic Preservation, Expressive Minimality, and Decidability Boundaries

Este artículo presenta una formalización verificada por máquina en Rocq que demuestra que la gobernanza transparente de efectos para los flujos de trabajo de IA puede restringir estrictamente los efectos externos y hacer cumplir los predicados de seguridad sin comprometer la expresividad computacional interna ni la transparencia semántica.

Autores originales: Alan L. McCann

Publicado 2026-05-06

📖 5 min de lectura🧠 Análisis profundo

CC0 1.0

Autores originales: Alan L. McCann

Artículo original dedicado al dominio público bajo CC0 1.0 (http://creativecommons.org/publicdomain/zero/1.0/). ✨ Esta es una explicación generada por IA del artículo a continuación. No ha sido escrita ni avalada por los autores. Para mayor precisión técnica, consulte el artículo original. Leer descargo de responsabilidad completo

Imagina que tienes un asistente de IA brillante y de alta capacidad. Puede escribir código, recordar cosas, llamar a herramientas externas e incluso conversar con otros modelos de IA para resolver problemas complejos. Pero te preocupa: ¿qué pasa si decide hacer algo peligroso, como borrar tus archivos o llamar a un servicio que no debería?

Tradicionalmente, se pensaba que había que elegir entre seguridad y capacidad. Podías dejar que la IA hiciera lo que quisiera (arriesgado) o imponerle restricciones pesadas que podrían impedirle hacer su trabajo correctamente (tonto).

Este artículo introduce una nueva forma de construir sistemas de IA que demuestra que no tienes que hacer ese intercambio. Muestra que puedes colocar una capa de "gobernanza" alrededor de la IA que detiene las acciones malas sin cambiar cómo la IA piensa o resuelve problemas.

Aquí está el desglose usando analogías simples:

1. La idea central: El "Portero" vs. El "Editor"

La mayoría de los métodos de seguridad actuales actúan como un Editor. La IA hace su trabajo, escribe una historia y luego el Editor la lee. Si la historia tiene una palabra mala, el Editor la corta o reescribe la oración.

El problema: El Editor cambia la historia. El proceso de pensamiento original de la IA se altera y el resultado final puede ser diferente de lo que la IA pretendía.

Este artículo propone un enfoque de Portero (llamado "Gobernanza Transparente de Efectos").

Cómo funciona: La IA está en una habitación. Antes de poder abrir una puerta (como acceder a la memoria, llamar a una herramienta o pedirle a un LLM), tiene que mostrar su identificación al Portero.
La magia: Si el Portero dice "Adelante", la IA atraviesa la puerta y hace exactamente lo que planeó. El Portero no cambió el proceso de pensamiento de la IA; solo verificó la identificación.
El resultado: Si se permite que la IA proceda, el resultado es exactamente el mismo que si el Portero no estuviera allí en absoluto. El "cerebro" de la IA permanece intacto.

2. El "Árbol de Interacción" (El plano)

Los autores construyeron un modelo matemático de los flujos de trabajo de la IA usando algo que llaman "Árboles de Interacción".

Analogía: Piensa en un flujo de trabajo de la IA como un árbol. El tronco es la lógica de la IA. Las ramas son las cosas que quiere hacer (como "Llamar a una base de datos" o "Hacer una pregunta").
La "Gobernanza" es un envoltorio alrededor de las puntas de las ramas. Verifica cada rama antes de que crezca. Si una rama no está autorizada, el árbol deja de crecer allí (se "diverge" o gira sobre sí mismo). Si está autorizada, la rama crece exactamente como la IA la diseñó.

3. Siete descubrimientos clave (Los "Siete Pilares")

Los autores utilizaron una computadora para demostrar matemáticamente siete cosas sobre este sistema:

P1 y P2: Sigue siendo súper inteligente. Incluso con el Portero verificando identificaciones, la IA aún puede hacer cualquier cosa que pueda hacer una computadora normal (completa de Turing) y aún puede usar herramientas avanzadas como LLM. La red de seguridad no hizo a la IA "menos inteligente".
P3: La "Frontera de Decidibilidad" (La línea en la arena). El Portero es bueno para verificar reglas estructurales (por ejemplo: "¿Es esto una solicitud de memoria?" "¿Tiene este usuario una insignia de nivel 5?"). Estas son fáciles de verificar instantáneamente. Sin embargo, el Portero no puede predecir si la IA se quedará atrapada en un bucle para siempre o si un problema matemático complejo terminará alguna vez. El artículo demuestra que el Portero se mantiene en su carril: verifica reglas, no preguntas filosóficas profundas sobre el comportamiento futuro de la IA.
P4: Preservación de objetivos. Si se permite que la IA se ejecute, alcanzará su objetivo. Si debía calcular 2+2, seguirá calculando 4. La verificación de seguridad no cambió las matemáticas.
P5: Minimalismo expresivo. El sistema utiliza un conjunto específico de herramientas (Cálculo, Memoria, Razonamiento, Llamada a Herramientas, Observación). Los autores demostraron que si eliminas cualquiera de estas herramientas, la IA pierde un tipo específico de poder. No puedes simplificar el sistema más sin romper su capacidad para realizar trabajos complejos.
P6: El "Portero" es más fuerte que el "Editor". El artículo demuestra que verificar la acción (gobernanza estructural) es estrictamente mejor que solo filtrar la salida (gobernanza de contenido). Un Portero puede detener una acción mala antes de que ocurra. Un Editor solo puede intentar arreglar un mal resultado después de que ocurre, lo cual es menos confiable.
P7: Transparencia semántica (El efecto "Fantasma"). Esta es la parte más importante. En cada ejecución en la que se permite que la IA trabaje, el resultado es observacionalmente equivalente a una ejecución sin gobernanza. Para un observador externo, es como si la capa de gobernanza fuera invisible (un fantasma), excepto por el hecho de que detuvo con éxito las cosas malas.

4. El "Artefacto" (La prueba)

Los autores no solo escribieron esto; lo construyeron dentro de un asistente de pruebas llamado Rocq (una herramienta para verificar matemáticas).

Escribieron 12.000 líneas de código.
Demostraron 454 teoremas.
Admitieron cero errores (0 lemas admitidos).
Esto significa que la computadora ha verificado doblemente su lógica y confirmado que es 100% matemáticamente sólida.

Resumen

Este artículo argumenta que podemos construir sistemas de IA con un "envoltorio de seguridad" que actúa como un guardián estricto. Este guardián detiene las acciones no autorizadas (como hackear o llamadas no autorizadas), pero, crucialmente, no interfiere con el proceso de pensamiento de la IA cuando se permite la acción.

Demuestra que la Seguridad y la Inteligencia no son enemigos. Puedes tener un sistema que esté totalmente gobernado y seguro, y que sin embargo conserve su capacidad completa para calcular, razonar y actuar, siempre que las acciones estén autorizadas. La capa de gobernanza es transparente para el éxito de la IA, actuando solo como un escudo contra efectos no autorizados.

Resumen Técnico: Gobernanza Transparente de Efectos para Arquitecturas de Flujos de Trabajo de IA

Enunciado del Problema

A medida que los sistemas de flujos de trabajo de IA actúan cada vez más en el mundo —consultando Modelos de Lenguaje Grande (LLM), gestionando estado e invocando herramientas externas—, existe una necesidad creciente de mecanismos de gobernanza para prevenir comportamientos inseguros o no autorizados. Una suposición predominante en el campo es que la gobernanza inevitablemente sacrifica capacidad: se cree que las restricciones destinadas a aumentar la seguridad reducen el espacio de comportamientos que un sistema puede exhibir. Este artículo desafía esa suposición formalizando una alternativa arquitectónica donde la gobernanza se impone en la frontera de efectos en lugar de modificar el cálculo interno o el procesamiento posterior de las salidas. La pregunta semántica central abordada es si la gobernanza cambia lo que los programas permitidos calculan.

Metodología

Los autores presentan una formalización verificada por máquina de arquitecturas de flujos de trabajo de IA gobernadas estructuralmente utilizando Árboles de Interacción dentro del asistente de pruebas Rocq 8.19 (anteriormente Coq). El desarrollo consta de 36 módulos, 12.000 líneas de código y 454 teoremas, con cero lemas admitidos.

Formalismo Central

Árboles de Interacción (ITrees): Los programas se modelan como árboles coinductivos sobre un tipo de evento $E$ , definidos como Ret(v), Tau(t) o Vis(e, k). Esto permite la representación de programas recursivos e impuros.
Tipo de Evento Directivo: El sistema define un tipo DirectiveE que contiene constructores para capacidades primitivas: morfismos de cálculo, operaciones de memoria, llamadas a oráculos (LLM), llamadas a herramientas externas y eventos de observabilidad.
Operador de Gobernanza ( $G$ ): La gobernanza se implementa como un envoltorio sobre la interpretación de efectos, siguiendo la tradición de los manejadores de efectos algebraicos. El operador $G(h)$ media cada directiva emitida por un manejador base $h$ . Realiza pre-verificaciones (confianza, permiso, validación de fase) y post-instrumentación (procedencia, observabilidad). Si una verificación falla, la ejecución diverge mediante ITree.spin; si pasa, la directiva se delega al manejador subyacente.
Predicado de Seguridad: La seguridad se define mediante un predicado coinductivo gov_safe utilizando coinducción parametrizada (paco). Este predicado distingue entre eventos exclusivos de gobernanza (que siempre están permitidos) y eventos reales de E/S (que requieren autorización explícita).

Contribuciones y Resultados Clave

El artículo establece siete propiedades principales (P1–P7) que demuestran que la gobernanza y la expresividad computacional son dimensiones ortogonales.

1. Transparencia Semántica (El Teorema Central)

La contribución central es un teorema verificado por máquina que demuestra la transparencia semántica. Para todas las ejecuciones donde las verificaciones de gobernanza tienen éxito, la interpretación gobernada es observacionalmente equivalente (módulo eventos exclusivos de gobernanza) a la interpretación no gobernada.

Implicación: Los programas permitidos calculan exactamente la misma función parcial y producen los mismos valores de retorno alcanzables que lo harían sin gobernanza. La gobernanza restringe la frontera de efectos sin alterar el cálculo interno de los caminos permitidos.

2. Expresividad Gobernada (P1 y P2)

Los autores demuestran que el envoltorio de gobernanza no reduce el poder computacional:

Completitud de Turing Gobernada: El sistema permanece completo en el sentido de Turing bajo gobernanza. Los programas de máquinas de registro pueden traducirse a árboles de interacción gobernados sin pérdida de expresividad.
Expresividad de Oráculo Gobernada: La arquitectura soporta extensiones de oráculo (consultas a LLM) bajo gobernanza, manteniendo la capacidad de modelar flujos de trabajo de razonamiento complejos.

3. Límite de Decidibilidad (P3)

El artículo formaliza un límite estricto entre lo que la gobernanza puede decidir y lo que no puede:

Predicados de Gobernanza: Estos son estructurales, sintácticos, totales y cerrados bajo composición booleana (Y, O, NO). Pueden decidir propiedades como niveles de confianza y clases de capacidades.
Propiedades Semánticas: Las propiedades de los programas, como la terminación, permanecen no triviales e indecidibles por la gobernanza. El artículo demuestra que la gobernanza no puede decidir la terminación, ya que dos programas pueden compartir estructuras directivas idénticas (y por lo tanto pasar las verificaciones de gobernanza) pero diferir en su comportamiento global de terminación. Esto se alinea con el Teorema de Rice aplicado a la frontera estructural.

4. Minimalidad Expresiva (P5)

Los autores demuestran que el conjunto de capacidades primitivas (cálculo, memoria, razonamiento, llamada externa, observabilidad) es mínimamente necesario.

Jerarquía Estricta: Las capacidades forman una cadena estricta: código < código + memoria < código + memoria + razonamiento < código + memoria + razonamiento + llamada.
Necesidad: Eliminar cualquier capacidad primitiva individual reduce estrictamente el poder expresivo del sistema. Por ejemplo, las directivas de memoria son estructuralmente necesarias para la completitud de Turing, y las directivas LLMCall son necesarias para las extensiones de oráculo.

5. Asimetría de Subsumción (P6)

El artículo establece una separación estricta entre la gobernanza estructural y el filtrado a nivel de contenido:

La Estructural Subsume al Contenido: La gobernanza estructural subsume estrictamente el filtrado de contenido. Al mediar los efectos en la frontera de interpretación, la gobernanza estructural previene que ocurran eventos de E/S no autorizados.
El Contenido No Subsume a la Estructural: Los filtros de contenido (por ejemplo, reescritura de salidas) pueden alterar valores pero no pueden prevenir la ocurrencia de un paso de efecto no autorizado. Por lo tanto, el filtrado de contenido por sí solo no implica seguridad de efectos.

6. Preservación de Objetivos (P4)

En todas las ejecuciones donde la gobernanza permite, el sistema preserva los objetivos del programa. Si un programa está diseñado para alcanzar un valor de retorno específico $v$ , y las verificaciones de gobernanza pasan, la ejecución gobernada alcanzará $v$ .

7. Seguridad mediante Denegación (Vivacidad vs. Seguridad)

Cuando una verificación de gobernanza falla, el sistema sacrifica la vivacidad por la seguridad. La ejecución diverge (spin) en lugar de producir un resultado incorrecto. El sistema garantiza que nunca ocurra un efecto no autorizado y que nunca se produzca un valor de retorno "inseguro".

Significado y Alcance

El artículo afirma demostrar que la gobernanza y la expresividad computacional son ortogonales. La gobernanza puede imponerse para restringir la frontera de efectos de los programas sin reducir su expresividad computacional interna ni alterar su semántica en las trazas permitidas.

Límite de Confianza: Las garantías se mantienen con respecto a una Base de Computación Confiable (TCB) que consiste en el núcleo de Rocq, la biblioteca de Árboles de Interacción y la implementación en tiempo de ejecución del operador $G$ . El artículo establece un paralelo con compiladores verificados (CompCert) y núcleos de SO (seL4), señalando que la brecha entre el modelo formal y el tiempo de ejecución desplegado se cierra mediante pruebas (validadas contra más de 70.000 secuencias generadas).
Limitaciones: El teorema de transparencia se aplica solo a ejecuciones permitidas; las ejecuciones denegadas divergen. El modelo abstrae el agotamiento de recursos, la planificación y los comportamientos probabilísticos de los modelos. Los teoremas se aplican a la arquitectura abstracta e intérprete, no a garantías de extremo a extremo en binarios compilados.

Este trabajo extiende desarrollos mecanizados anteriores (McCann [2026b, 2026e]) añadiendo transparencia semántica, minimalidad expresiva y un límite de decidibilidad formal, proporcionando una base rigurosa para la "gobernanza transparente de efectos" en sistemas de IA.