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

Titolo

Semantica a tempo ramificato con conteggio dei mondi per la mitigazione post-hoc dei bias nell'IA generativa.

1. Il Problema

I sistemi di Intelligenza Artificiale Generativa (GenAI) tendono ad amplificare i bias presenti nei dati di addestramento, un fenomeno noto come "amplificazione del bias". Questo è particolarmente critico in ambiti come la generazione di immagini o testo, dove gruppi sottorappresentati nei dataset di training vengono ulteriormente marginalizzati nelle uscite del modello.
Le strategie di mitigazione esistenti operano spesso in fase di inferenza (inference-time) o post-hoc, ma sono prevalentemente empiriche e mancano di garanzie formali. Non esiste un quadro logico rigoroso per:

• Verificare se una serie di output generati rispetti una distribuzione di probabilità desiderata su un attributo protetto (es. genere).
• Prevedere la probabilità che la serie rimanga entro limiti accettabili man mano che nuovi output vengono generati.
• Determinare quantificativamente quanti output devono essere rimossi per ripristinare l'equità (fairness) senza dover riaddestrare il modello (costoso e difficile da scalare).

2. Metodologia: La Logica CTLF

Gli autori introducono CTLF (Counting Worlds Temporal Logic), una logica temporale ramificata (branching-time) ispirata alla Computational Tree Logic (CTL), ma con una semantica specifica basata sul conteggio dei mondi.

Concetti Chiave della Logica:

• Mondi (Worlds): Ogni mondo rappresenta un possibile output del modello in un dato passo del processo di generazione.
• Struttura dell'Albero: Il processo di generazione è modellato come un albero di eventi.
  • $W$: Insieme finito di mondi.
  • $R_e$: Relazione "retrospettiva" (da un evento ai suoi genitori/antecedenti).
  • $R_f$: Relazione "prospettica" (da un evento ai suoi figli/futuri possibili).
• Semantica di Conteggio: Gli operatori logici non si limitano a verificare la verità in un singolo percorso, ma valutano la frequenza o la probabilità di un evento (es. "maschio" o "femmina") rispetto al numero totale di mondi o percorsi accessibili.

Operatori Logici Principali:

La logica estende la sintassi standard con operatori quantificati da una soglia di probabilità $q \in [0,1]$:

1. $\square_q \phi$ (Conteggio Retrospettivo): Allo stato corrente, l'evento $\phi$ è accaduto almeno $q \times m$ volte (dove $m$ è il numero di output finora), basandosi sulla storia reale osservata.
2. $\blacksquare_q \phi$ (Conteggio Potenziale): Esiste almeno un percorso completo coerente con la distribuzione di probabilità $\Phi_\Sigma$ in cui $\phi$ potrebbe essere accaduto $q \times m$ volte.
3. $\bigcirc_q \phi$ (Esistenza di un Percorso): Esiste almeno un percorso completo di output in cui, in qualche punto, $\phi$ si verifica almeno $q \times n$ volte (dove $n$ è la lunghezza totale).
4. $\triangleright_q \phi$ (Probabilità Futura): Data una distribuzione definita, la probabilità che $\phi$ accada al passo successivo è almeno $q$.
5. $\nabla_q \phi$ (Verifica del Percorso Completo): In un percorso completo, $\phi$ si verifica almeno $q \times n$ volte.
6. $\dagger_q \phi$ (Probabilità di Completamento): Data una serie parziale, la probabilità che il completamento della serie rimanga entro la distribuzione desiderata è almeno $q$.

3. Contributi Chiave

• Formalizzazione Logica del Bias: Il paper fornisce il primo quadro formale per ragionare sulle distribuzioni di attributi protetti in serie temporali di output GenAI, permettendo di esprimere proprietà di equità in modo matematicamente rigoroso.
• Strategia di Mitigazione Post-Hoc: La logica permette di calcolare dinamicamente, durante la generazione, se è necessario intervenire. Se la distribuzione corrente devia dalla soglia accettabile, il sistema può determinare esattamente quanti e quali output futuri devono essere scartati (o quali percorsi evitare) per ripristinare l'equità.
• Predizione Tempestiva: A differenza dei metodi puramente reattivi, CTLF permette di prevedere l'evoluzione della serie di output. Se si rileva che un percorso porterà inevitabilmente a un output inaccettabile, il sistema può intervenire prima che l'output venga consegnato all'utente.
• Esempio Concreto (Generazione Immagini): Gli autori dimostrano l'applicazione su un caso di studio di generazione di immagini di "ingegneri" con un dataset di addestramento sbilanciato (75% maschi, 25% femmine). La logica calcola le probabilità di mantenere un rapporto 50/50 man mano che le immagini vengono generate e identifica i punti di intervento per rimuovere gli output sbilanciati.

4. Risultati e Analisi

Attraverso un esempio toy (6 generazioni di immagini con 2 possibili esiti: Maschio/Femmina), il paper dimostra:

• Verifica dello Stato Corrente: È possibile verificare se, al passo $m$, il rapporto tra attributi è ancora entro i limiti di equità (es. $w_{4.7} \models \square_{1/2} M \land \square_{1/2} F$).
• Calcolo della Probabilità di Successo: Si può calcolare la probabilità che la serie completi correttamente (es. probabilità del 50% di raggiungere un equilibrio 3M/3F partendo da uno stato specifico).
• Pianificazione della Mitigazione: Se la distribuzione si sbilancia (es. 3 maschi e 2 femmine al passo 5 in un target 50/50), la logica identifica che la quota per i maschi è esaurita. Di conseguenza, suggerisce di rimuovere tutti i futuri output maschili per ottenere un sottoinsieme equilibrato di 6 elementi.
• Efficienza: L'approccio permette di identificare percorsi "compatibili con $\Sigma$" (distribuzione target) e scartare quelli che violano i vincoli, garantendo che l'output finale sia formalmente verificato come equo.

5. Significato e Implicazioni

• Sicurezza e Fiducia (Trustworthiness): CTLF offre un livello di garanzia formale mancante nelle attuali soluzioni empiriche, cruciale per il deployment sicuro di sistemi GenAI in contesti critici.
• Indipendenza dal Riaddestramento: La metodologia permette di correggere i bias a runtime senza i costi computazionali e temporali del riaddestramento dei modelli fondazionali.
• Futuri Sviluppi:
  • Pesi sulle Transizioni: Estendere la logica per assegnare pesi probabilistici specifici alle transizioni, riflettendo conoscenze pregresse più fini.
  • Distribuzioni Adattive: Implementare un modello in cui la distribuzione di riferimento non è fissa ma viene aggiornata dinamicamente man mano che nuovi output sono osservati (simile alle Catene di Markov Parametriche).
  • Implementazione Software: Gli autori stanno sviluppando un'implementazione nel "MIRAI Toolbox" che accetterà in input un flusso di output GenAI, una distribuzione target e una soglia di equità, restituendo un certificato di conformità o un piano di mitigazione specifico.

In sintesi, il paper propone un ponte fondamentale tra la logica formale e l'etica dell'IA, trasformando la mitigazione del bias da un processo euristico a uno verificabile e calcolabile matematicamente.