Counting Worlds Branching Time Semantics for post-hoc Bias Mitigation in generative AI

Resumen Técnico: CTLF para la Mitigación de Sesgos en IA Generativa

1. Planteamiento del Problema

Los sistemas de Inteligencia Artificial Generativa (IA Generativa) tienen la tendencia inherente de amplificar los sesgos presentes en sus datos de entrenamiento. Aunque existen estrategias de mitigación en tiempo de inferencia (como filtrado de tokens o ensembles de vectores), estas son mayoritariamente empíricas y carecen de garantías formales.

El problema central identificado es la falta de un marco lógico capaz de:

• Razonar sobre series de outputs generados en tiempo real.
• Determinar si una serie actual se desvía de una distribución de probabilidad deseada (ej. equidad de género).
• Predecir la probabilidad de que la serie futura permanezca dentro de límites aceptables.
• Calcular cuántos outputs deben eliminarse (post-hoc) para restaurar la equidad sin reentrenar el modelo.

2. Metodología: La Lógica CTLF y Semántica de Conteo de Mundos

Los autores proponen CTLF (Computational Tree Logic with Counting), una lógica de tiempo ramificado diseñada específicamente para razonar sobre sesgos en series de outputs generativos.

Componentes Clave de la Metodología:

• Semántica de "Contar Mundos" (Counting Worlds Semantics):

  • El sistema modela el proceso de generación como un árbol de mundos posibles.
  • Cada mundo ($w$) representa un resultado posible en un paso específico de la generación.
  • Un camino ($\pi$) representa una secuencia completa de $n$ outputs.
  • Se define una distribución de probabilidad $\Sigma$ que asigna frecuencias esperadas a atributos protegidos (ej. género).

• Operadores Modales Nuevos:
  La lógica introduce operadores que permiten verificar propiedades estadísticas en estados actuales y futuros:

  • $\square_q \phi$: En el estado actual, la propiedad $\phi$ ha ocurrido al menos en una proporción $q$ de los mundos accesibles hacia atrás (historia).
  • $\blacksquare_q \phi$: Existe al menos una secuencia posible (en la distribución definida) donde $\phi$ ocurre con frecuencia $q$.
  • $\bigcirc_q \phi$: Existe una secuencia completa posible donde $\phi$ ocurre con frecuencia $q$.
  • $\triangleright_q \phi$: Dada una distribución, la probabilidad de que $\phi$ ocurra en el siguiente paso es al menos $q$.
  • $\triangledown_q \phi$ y $\dagger_q \phi$: Operadores de camino que verifican si una secuencia completa cumple con la distribución y la probabilidad de completar una secuencia justa desde un punto dado.

• Modelo Formal:
  Se define un modelo $M = (W, W^1, W^n, R_e, R_f, V)$ donde:

  • $W$ es un conjunto finito de mundos (nodos del árbol).
  • $R_e$ es una relación de "hijos" (pasado) y $R_f$ es una relación de "padres" (futuro).
  • $V$ es una función de valoración que asigna atributos (ej. "hombre", "mujer") a cada mundo.

3. Contribuciones Clave

1. Formalización Lógica de la Equidad: Por primera vez, se presenta un marco lógico (CTLF) que permite expresar y verificar propiedades de equidad en series temporales de outputs generativos, más allá de métricas estadísticas estáticas.
2. Predicción Temprana de Sesgo: La lógica permite predecir, en un punto intermedio de la generación ($m < n$), si la serie final excederá un umbral de sesgo aceptable, permitiendo intervenciones preventivas.
3. Estrategia de Mitigación Post-hoc Cuantitativa: El marco no solo detecta el sesgo, sino que calcula formalmente cuántos outputs deben eliminarse para restaurar la distribución deseada. Proporciona un "plan de mitigación" basado en la eliminación de ramas específicas del árbol de posibilidades.
4. Ejemplo Ilustrativo (Generación de Imágenes): Se demuestra la aplicación en un caso de uso de generación de imágenes de ingenieros con un sesgo de género (75% hombres, 25% mujeres). El sistema logra:
   • Identificar en qué paso la proporción se vuelve injusta.
   • Calcular la probabilidad de recuperar la equidad en pasos futuros.
   • Determinar que, si se generan 12 imágenes sesgadas, se deben eliminar todas las imágenes masculinas subsiguientes para obtener un subconjunto equilibrado de 6 imágenes (3 hombres, 3 mujeres).

4. Resultados y Ejemplos

En el ejemplo de la "generación de ingenieros":

• Detección: Si se generan 4 imágenes y la proporción es 3H/1M, el sistema verifica si esto es compatible con una distribución justa futura.
• Predicción: Si en el paso 4 la proporción ya es insostenible (ej. 3H/0M y el objetivo es 50/50), la lógica determina que la probabilidad de completar la serie con equidad es 0.
• Mitigación: El sistema identifica que, para restaurar la equidad en un lote de 12, es necesario eliminar todos los outputs masculinos restantes, resultando en un subconjunto válido de 6 outputs (3H/3M).
• Validación: Se demuestra que las fórmulas de CTLF pueden expresar estas condiciones en diferentes puntos de la serie, ofreciendo certidumbre lógica sobre la necesidad de intervención.

5. Significado e Impacto

• Garantías Formales: Cambia el paradigma de la mitigación de sesgos de un enfoque puramente empírico a uno con garantías lógicas y matemáticas.
• Eficiencia de Recursos: Permite intervenir en el momento exacto en que la generación se vuelve irreversible o dañina, evitando el desperdicio de recursos computacionales en generar outputs que luego tendrían que ser descartados.
• Aplicabilidad Práctica: Los autores están desarrollando una implementación en la caja de herramientas MIRAI. Esta herramienta tomará como entrada un flujo de outputs, una distribución objetivo y un umbral de equidad, devolviendo un certificado de cumplimiento o un plan de mitigación específico (qué outputs eliminar).
• Futuro: El marco es extensible a distribuciones de probabilidad dinámicas (actualización en tiempo real de los pesos de transición) y se integra con cadenas de Markov paramétricas para sistemas adaptativos.

En conclusión, este trabajo establece una base teórica sólida para la supervisión y corrección de IA Generativa en tiempo de ejecución, asegurando que los sistemas no solo generen contenido, sino que lo hagan respetando restricciones éticas y de equidad definidas formalmente.