A Linear Temporal Logic of Frequencies on Series of Events

1. Il Problema

Il lavoro nasce dalla necessità di monitorare e controllare sistemi complessi (come i classificatori di Machine Learning) in tempo reale, garantendo che le loro uscite rispettino vincoli specifici, in particolare riguardo all'equità algoritmica.
Il problema centrale affrontato è la mancanza di un quadro logico formale in grado di:

• Esprimere le proprietà di frequenza di serie di eventi finite.
• Confrontare direttamente le frequenze osservate (empiriche) con una distribuzione teorica ideale (target) all'interno di una singola struttura di valutazione.
• Prevedere la probabilità di futuri eventi basandosi su dati parziali e su un'ipotesi di frequenza globale desiderata.

Sebbene esistano logiche temporali estese con funzionalità di conteggio o probabilità (come LTL con conteggio, CTL, PCTL), nessuna di queste formalizza esplicitamente la relazione tra un'osservazione parziale e una distribuzione target in un'unica struttura logica, né adotta un approccio "retrospettivo" (guardando al passato) per valutare le frequenze in un punto specifico della serie.

2. Metodologia

Gli autori introducono LTLF (Linear Temporal Logic of Frequencies), un nuovo sistema logico temporale lineare. La metodologia si basa sui seguenti pilastri:

• Semantica Kripke-style su serie finite: La logica è definita su modelli composti da un insieme finito di mondi (istanti temporali) ordinati linearmente.
• Struttura del modello: Un modello $M$ è una tupla $(W, R_e, F_\Omega, a)$, dove:
  • $W$ è l'insieme finito dei mondi (esperimenti).
  • $R_e$ è una relazione di accesso lineare (riflessiva, transitiva, antisimmetrica e fortemente connessa).
  • $F_\Omega$ è un insieme di assegnazioni compatibili con una misura di probabilità empirica definita su uno spazio campionario $\Omega$.
  • $a$ è l'assegnazione specifica che rappresenta l'osservazione "reale" o corrente.
• Approccio Retrospettivo: A differenza della maggior parte delle logiche temporali che guardano al futuro, LTLF valuta le formule guardando al passato (fino all'istante corrente $t_m$) per calcolare le frequenze relative.
• Operatori Modali Sensibili alla Misura: Vengono introdotti cinque nuovi operatori modali quantificati da valori razionali $q \in \mathbb{Q}_{[0,1]}$:
  1. $\Box_q$ (White Box): Dipendente dall'osservazione e dal tempo. Esprime che, fino al tempo corrente, la formula è stata verificata con frequenza relativa $\ge q$.
  2. $\blacksquare_q$ (Black Box): Indipendente dall'osservazione specifica, ma dipendente dal tempo. Esprime che esiste almeno un'assegnazione compatibile con la distribuzione target $F_\Omega$ tale che la frequenza osservata potrebbe essere $\ge q$. Serve a verificare la compatibilità con il target.
  3. $\circ_q$ (Circle): Dipendente da osservazione e tempo. Esprime la probabilità condizionata che, dato il totale $n$ di esperimenti previsti, la formula si verifichi almeno $q \times n$ volte.
  4. $\triangleright_q$ (Next): Esprime la probabilità che un evento si verifichi al passo successivo ($t_{m+1}$), dato che l'osservazione corrente è compatibile con la distribuzione target.
  5. $\star_q$ (Star): Indipendente dal tempo e dall'osservazione specifica. Esprime che, secondo la distribuzione target $F_\Omega$, esiste un mondo in cui la formula è vera con frequenza $\ge q$ (essenzialmente lega l'operatore alla probabilità teorica $\mu_\Phi$).

3. Contributi Chiave

Il contributo principale del paper è la definizione di un linguaggio formale che colma il divario tra ragionamento logico formale e osservazione empirica. I contributi specifici includono:

• Formalizzazione della Compatibilità: La capacità di determinare se una serie di osservazioni parziali è ancora compatibile con una frequenza globale desiderata (es. "è ancora possibile raggiungere una frequenza di 0.5 di 'Testa' dopo aver visto 3 'Croci' consecutive?").
• Nuovi Operatori di Conteggio: L'introduzione degli operatori $\Box, \blacksquare, \circ, \triangleright, \star$ permette di distinguere tra ciò che è effettivamente accaduto ($\Box$), ciò che è possibile secondo un modello ideale ($\blacksquare$), e la probabilità futura condizionata ($\triangleright$).
• Calcolo delle Probabilità di Realizzazione: Il sistema permette di calcolare la probabilità che un'assegnazione osservata porti a una distribuzione finale compatibile con il target, sia nel caso di esiti equiprobabili che indipendenti ma non equiprobabili.
• Predizione A Posteriori: La capacità di stimare la probabilità di un risultato futuro dato che la frequenza globale è stata realizzata (es. "se sappiamo che in 10 lanci ci saranno 5 teste, qual è la probabilità che il prossimo lancio sia testa?").

4. Risultati Principali

Gli autori dimostrano la robustezza di LTLF attraverso una serie di teoremi e problemi risolti:

• Misurazione delle Frequenze: Dimostrazione che $\Box_q$ cattura esattamente la frequenza relativa empirica in un punto della serie.
• Compatibilità con il Target:
  • Viene mostrato come combinare $\Box$ e $\blacksquare$ (o $\circ$ e $\star$) per verificare se un'osservazione parziale è coerente con una distribuzione globale $F_\Omega$.
  • Viene identificata la condizione necessaria e sufficiente affinché un'assegnazione sia compatibile con il target fino a un certo istante $m$.
• Probabilità di Realizzazione:
  • Teorema 5.8 e 5.9: Forniscono formule combinatorie per calcolare la probabilità che un'osservazione parziale possa essere completata per soddisfare la distribuzione target $F_\Omega$. La formula tiene conto del numero di modi in cui i restanti esperimenti possono essere assegnati per rispettare le frequenze target.
• Predizione Futura:
  • Teorema 5.10 e 5.12: Stabiliscono che l'operatore $\triangleright_q$ calcola esattamente la probabilità condizionata che un evento si verifichi al passo successivo, dato che l'assegnazione corrente appartiene all'insieme delle assegnazioni compatibili con il target.
  • Viene dimostrato un rapporto matematico tra la probabilità di compatibilità in un passo $m$ e in $m+1$ (Teorema 5.13/5.14), mostrando come la conoscenza di un nuovo esito aggiorna la probabilità che la serie rispetti il target.

5. Significato e Implicazioni

LTLF rappresenta un avanzamento significativo nella logica temporale e nella verifica formale di sistemi probabilistici:

• Applicabilità al Machine Learning: Il framework è particolarmente rilevante per il monitoraggio dell'equità algoritmica. Permette di verificare se un classificatore sta producendo uscite che si discostano da una distribuzione di equità desiderata, non solo in termini di errore totale, ma nella dinamica temporale delle sue decisioni.
• Flessibilità Espressiva: A differenza di altre logiche quantitative che sacrificano l'espressività per la tracciabilità computazionale, LTLF utilizza un piccolo set di operatori altamente espressivi per catturare proprietà distribuzionali complesse.
• Ponte tra Teoria e Pratica: La logica offre un linguaggio unificato per ragionare su dati reali (osservazioni) e modelli teorici (distribuzioni ideali) simultaneamente, permettendo di rispondere a domande su "cosa è successo", "cosa potrebbe succedere" e "cosa è probabile che succeda" in un unico formalismo.
• Prospettive Future: Il lavoro apre la strada a sistemi di prova (proof systems), analisi di complessità computazionale e l'estensione a logiche temporali ramificate (branching time) per scenari più complessi. Attualmente, gli autori stanno esplorando applicazioni concrete nella mitigazione dei bias nei classificatori ML.

In sintesi, il paper propone un nuovo paradigma logico che trasforma il concetto di frequenza da una semplice statistica descrittiva a una proprietà dinamica e verificabile formalmente all'interno di un sistema temporale.