🤖 AI

Algebraic Semantics of Governed Execution: Monoidal Categories, Effect Algebras, and Coterminous Boundaries

Este artículo presenta una semántica algebraica mecanizada para la ejecución gobernada, formalizada en 32 módulos de Rocq utilizando árboles de interacción y coinducción, que establece una categoría monoidal simétrica donde la gobernanza se axiomatiza, es composicional y coterminante con la expresividad, garantizando que todos los programas construibles estén gobernados mientras se preserva la completitud de Turing y se excluye la E/S no mediada.

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 estás construyendo un robot complejo que puede pensar, hablar, recordar cosas e incluso salir al mundo a comprar comestibles o llamar a un amigo. Quieres que este robot sea increíblemente inteligente y capaz, pero también necesitas asegurarte de que nunca haga nada peligroso, ilegal o contra las reglas mientras trabaja.

Este artículo presenta una nueva forma de diseñar el "cerebro" y las "reglas" para tal robot. En lugar de simplemente esperar que el robot se comporte bien, los autores han construido una fortaleza matemática alrededor de sus acciones. Lo llaman "Ejecución Gobernada".

Aquí está el desglose de su idea usando analogías simples:

1. El Problema: El "Lejano Oeste" de la IA

Actualmente, intentamos controlar la IA de dos maneras:

El Enfoque del "Filtro": Entrenamos a la IA para que sea educada o filtramos sus respuestas después de que habla. Esto es como intentar detener un grifo que gotea fregando el suelo. No evita que el agua salga; solo intenta limpiarlo más tarde.
El Enfoque de la "Barrera": Ponemos vallas alrededor del robot. Pero a menudo, estas vallas son solo sugerencias o reglas blandas que el robot puede saltar accidentalmente (o intencionalmente).

Los autores argumentan que necesitamos un sistema donde las reglas estén codificadas en la propia estructura de la capacidad de actuar del robot. Si el robot intenta hacer algo sin permiso, literalmente no puede hacerlo.

2. La Solución: El "Taburete de Tres Patas" (El Álgebra)

Los autores crearon un marco matemático llamado Álgebra de Gobernanza. Piensa en esto como un taburete de tres patas que debe estar perfectamente equilibrado para que el sistema funcione. Si falta alguna pata, todo se cae. Las tres patas son:

Seguridad: El robot nunca debe realizar una acción sin un "permiso" (una verificación de gobernanza).
Transparencia: Si el robot sí tiene permiso, las reglas no deben cambiar qué hace, solo que verificó primero. (No debe ralentizar al robot ni cambiar su respuesta, solo asegurar que sea seguro).
Corrección: Las reglas deben ser consistentes. Si dos robots hacen lo mismo, las reglas deben tratarlos exactamente igual.

3. El "Árbol de Interacción": El Proceso de Pensamiento del Robot

Para demostrar que esto funciona, representan el pensamiento del robot como un gigante Árbol.

Las Ramas: Cada vez que el robot piensa, se divide en ramas.
Las Hojas: Las acciones finales (como "Llamar a un amigo" o "Escribir un archivo").
El Tronco: El camino que el robot toma para llegar allí.

En su sistema, cada rama de este árbol debe pasar por una Puerta de Seguridad (el Operador de Gobernanza) antes de poder crecer. Si una rama intenta crecer sin pasar por la puerta, el árbol simplemente se niega a existir.

4. La "Doble Garantía": La Credencial de Identificación y el Vigilante de Seguridad

El artículo introduce un sistema de seguridad inteligente de dos partes:

La Credencial de Identificación (Capacidades): Antes de que el robot incluso comience, recibe una credencial que lista exactamente lo que se le permite hacer (por ejemplo, "Puede leer archivos", "No puede eliminar archivos"). Esta es una lista estática.
El Vigilante de Seguridad (Gobernanza): A medida que el robot se mueve, un Vigilante de Seguridad verifica cada paso. Incluso si el robot tiene una credencial, el Vigilante lo detiene si la acción específica parece sospechosa en ese momento.

El artículo demuestra que ambas cosas deben ocurrir al mismo tiempo. No puedes tener solo la credencial (porque el robot podría confundirse), y no puedes tener solo al vigilante (porque el vigilante podría pasar algo por alto). Trabajan juntos para asegurar que cada acción individual esté tanto autorizada como verificada.

5. El "Límite Coterminante": La Coincidencia Perfecta

Esta es la parte más emocionante del artículo. Los autores demuestran un teorema de "Coincidencia Perfecta".

La Afirmación: En su sistema, todo lo que el robot es capaz de construir es automáticamente seguro.
La Analogía: Imagina una fábrica de juguetes donde los únicos juguetes que puedes construir son aquellos que vienen con un certificado de seguridad. No puedes construir accidentalmente un juguete que sea inseguro. Si no es seguro, la máquina de la fábrica ni siquiera te dejará empezar a construirlo.
El Resultado: La zona "segura" y la zona "posible" tienen exactamente el mismo tamaño. No hay "zona gris" donde un robot pueda hacer algo arriesgado. Si el robot puede expresar un pensamiento o una acción, está garantizado que estará gobernado.

6. La Prueba de la "Caja Negra"

Los autores no solo escribieron esto; construyeron una enorme máquina de pruebas digitales (usando una herramienta llamada Rocq) con más de 12.000 líneas de código y 454 pruebas matemáticas.

Demostraron que si sigues sus reglas, el robot no puede accidentalmente hacer algo malo.
Demostraron que el robot sigue siendo lo suficientemente inteligente para realizar tareas complejas (es "turingiano", lo que significa que puede resolver cualquier problema que una computadora pueda resolver).
Incluso construyeron un "Libro Mayor" (como un diario a prueba de manipulaciones) que registra cada verificación de permiso y acción, para que si alguien intenta hacer trampa más tarde, el diario pruebe que lo hicieron.

Resumen

Este artículo dice: "Hemos construido una jaula matemática para las acciones de la IA. Dentro de esta jaula, la IA es libre de hacer lo que quiera, pero es físicamente imposible que haga algo inseguro. Las reglas no son solo sugerencias; son las leyes de la física para este sistema específico".

Lo han demostrado matemáticamente, lo han probado con millones de escenarios aleatorios y han mostrado que la versión "segura" de la IA funciona tan rápido como la versión "insegura". Es una forma de hacer que la IA sea poderosa sin hacerla peligrosa.

Resumen Técnico: Semántica Algebraica de la Ejecución Gobernada

Declaración del Problema

Los sistemas actuales de flujos de trabajo de IA, que componen llamadas a modelos de lenguaje con recuperación de datos, ejecución de código y acceso a APIs externas, carecen de un marco formal para la ejecución gobernada. Los enfoques de gobernanza existentes caen en dos categorías:

Enfoques conductuales (por ejemplo, RLHF, IA Constitucional, barreras de seguridad) que filtran o entrenan las salidas del modelo pero no abordan si los efectos estructurales del sistema (llamadas a API, escrituras de archivos) atraviesan una frontera de gobernanza.
Enfoques estructurales que imponen invariantes en la capa de ejecución pero a menudo carecen de pruebas verificadas por máquina o no abordan la composición. Suelen verificar programas individuales en lugar de demostrar que la gobernanza es cerrada bajo los operadores de composición del sistema.

El desafío central es establecer una semántica donde la gobernanza no sea meramente un filtro externo, sino una propiedad intrínseca y composicional del propio modelo de ejecución, asegurando que el conjunto de programas expresables coincida con el conjunto de programas gobernados.

Metodología

El artículo desarrolla una semántica algebraica para la ejecución gobernada, mecanizada en 32 módulos de Rocq (aproximadamente 12.000 líneas de código, 454 teoremas, 0 lemas admitidos). El marco se basa en tres pilares técnicos principales:

Árboles de Interacción (ITrees): Los programas se representan como árboles coinductivos con tres tipos de nodos: Ret (valores puros), Tau (pasos silenciosos) y Vis (eventos visibles). El sistema utiliza el tipo DirectiveE para modelar 14 capacidades externas distintas (por ejemplo, llamadas a LLM, solicitudes HTTP, operaciones de archivos).
Álgebra de Gobernanza: La gobernanza se axiomatiza como un registro paramétrico (GovernanceAlgebra) definido por tres axiomas:
- Seguridad: El operador de gobernanza G asegura que los programas interpretados satisfacen un predicado de seguridad coinductivo (gov safe).
- Transparencia: Bajo condiciones permisivas (cuando todos los controles pasan), la interpretación gobernada es observacionalmente equivalente a la interpretación no gobernada.
- Propiedad: Los manejadores equivalentes producen manejadores gobernados equivalentes.
Categorías Monoidales y Efectos Algebraicos: El marco extiende la categoría de programas (Mashin) con una estructura monoidal simétrica. Restringe el sistema de efectos algebraicos de tal manera que solo se pueden construir manejadores que portan un certificado de seguridad verificado por máquina (GovernedHandler) en el fragmento seguro.

La formalización utiliza coinducción parametrizada (a través de la biblioteca paco) para probar propiedades como gov safe y within caps (límites de capacidad). El sistema se extrae a OCaml e integra como una Función Implementada Nativa (NIF) en el tiempo de ejecución BEAM, con pruebas basadas en propiedades (más de 70.000 entradas aleatorias) que verifican la equivalencia conductual entre la especificación y el tiempo de ejecución.

Contribuciones Clave

1. Álgebra de Gobernanza Paramétrica y Estructura Monoidal

El artículo define un registro GovernanceAlgebra. A partir de los tres axiomas, deriva convergencia, cierre composicional y preservación de objetivos para cualquier sistema que satisfaga estos axiomas.

Estructura Monoidal: Se demuestra que la categoría Mashin admite una estructura monoidal simétrica con coherencia verificada de pentágono, triángulo y hexágono.
Preservación de la Gobernanza: Crucialmente, cada composición tensorial (composición independiente paralela/secuencial) preserva la gobernanza. Las pruebas son computacionales en lugar de coinductivas porque los morfismos estructurales son puros.

2. Efectos Algebraicos Gobernados

A diferencia de los sistemas estándar de efectos algebraicos donde cualquier manejador es válido, este marco restringe el álgebra de manejadores.

Manejadores Gobernados (GovernedHandlers): Solo los manejadores agrupados con una prueba de que su interpretación satisface gov safe pueden habitar el tipo GovernedHandler.
Sin Efectos Ambientales: Un teorema demuestra que los programas en el conjunto de capacidades vacío emiten únicamente directivas de observabilidad. No pueden realizar llamadas a LLM, solicitudes HTTP u otros efectos a menos que estén explícitamente autorizados por el conjunto de capacidades.

3. Composición Indexada por Capacidad y Garantía Dual

Los programas se agrupan con límites de capacidad verificados por máquina (CapMorphisms) validados por una red de confianza.

Composición: Los operadores de composición secuencial, tensorial y de rama preservan los límites de capacidad.
Garantía Dual: Un teorema central establece que para cualquier programa, los límites de capacidad (lo que el programa puede hacer) y la seguridad de gobernanza (lo que el programa tiene permitido hacer) se cumplen simultáneamente. Las capacidades estáticas acotan los efectos potenciales, mientras que la gobernanza dinámica asegura que cada efecto pase una verificación antes de la ejecución.

4. La Frontera Coterminante

El resultado culminante del artículo define la relación entre expresabilidad y gobernanza dentro del modelo formal:

Expresables (E): Programas construibles a partir de cuatro morfismos primitivos (code, reason, memory, call).
Gobernados (G): Programas donde la interpretación a través de G satisface gov safe.
Resultado: $E = G$ . Todo programa expresable está gobernado bajo interpretación, y todo programa gobernado es la imagen de un programa expresable.
Implicaciones: La completitud de Turing se preserva dentro de la gobernanza. La E/S no mediada está estructuralmente excluida del fragmento gobernado. La denegación de gobernanza se modela como divergencia coinductiva segura (no terminación), asegurando que nunca se produzca un resultado inseguro.

Resultados y Verificación

Verificación Formal: Todo el marco está mecanizado en Rocq con cero lemas admitidos.
Extracción de Tiempo de Ejecución: El código OCaml extraído se ejecuta como una NIF en el tiempo de ejecución BEAM.
Pruebas: Las pruebas basadas en propiedades con más de 70.000 entradas aleatorias mostraron cero desacuerdos entre la especificación de Rocq, la NIF extraída y el intérprete Elixir.
Rendimiento: La ruta de ejecución gobernada no añade sobrecarga medible (mediana de 0,23 ms frente a 0,24 ms para la ejecución no gobernada).
Semántica de Trazas: El marco deriva propiedades a nivel de traza, demostrando que la ejecución gobernada produce trazas "bien gobernadas" donde cada evento de E/S está precedido por una verificación de gobernanza aprobada. Estas trazas se mapean a un libro mayor a prueba de manipulaciones mediante encadenamiento de hashes.

Significado y Afirmaciones

El artículo afirma proporcionar el primer marco mecanizado que combina interpretación restringida por gobernanza, efectos algebraicos acotados por capacidad y un teorema de expresabilidad/gobernanza coterminante sobre un modelo de ejecución basado en árboles de interacción.

Gobernanza Estructural vs. de Contenido: El trabajo se distingue de los enfoques conductuales (que filtran salidas) al imponer gobernanza estructural (mediación de efectos). El Teorema 3.3 establece que la gobernanza estructural proporciona garantías que los controles orientados a la salida no pueden replicar dentro de este modelo formal.
Parametricidad: El GovernanceAlgebra es paramétrico; los teoremas derivados se cumplen para cualquier sistema que satisfaga los tres axiomas, no solo para la instancia específica Mashin.
Composicionalidad: El marco demuestra que la gobernanza es cerrada bajo todos los operadores de composición del sistema, abordando una brecha en trabajos anteriores que verificaban programas individuales pero no su composición.
Limitaciones: Los autores señalan que el producto tensorial es secuencialmente independiente (no verdaderamente concurrente), la cadena de hashes depende de un hash inyectivo abstracto (requiriendo trabajo adicional para hashes criptográficos concretos) y el propio envoltorio NIF no está formalmente verificado. La frontera coterminante se establece específicamente para el modelo de ejecución de cuatro primitivas.

En resumen, el artículo argumenta que al axiomatizar la gobernanza como una estructura algebraica sobre árboles de interacción, se puede lograr un sistema donde la gobernanza es coterminante con la expresabilidad: si un programa puede escribirse en el sistema, está estructuralmente garantizado que estará gobernado.