From categorized neural architectures to subexponential proof theory

1. Il Problema e il Contesto

Il lavoro si colloca all'intersezione tra l'apprendimento automatico (in particolare il categorical deep learning) e la logica lineare.

• Contesto: Esistono approcci che utilizzano la teoria delle categorie per descrivere semanticamente le architetture neurali (composizione, backpropagation, condivisione dei pesi). Parallelamente, la logica lineare e le sue varianti (come la logica con subesponenziali) offrono strumenti potenti per modellare la gestione delle risorse (uso lineare, duplicazione, cancellazione).
• Il Problema: La maggior parte dei lavori esistenti parte da una logica preesistente per cercare una semantica o per vincolare le architetture. Il paper si pone una domanda inversa e fondamentale: è possibile partire da una famiglia di architetture neurali organizzate in modo categorico, analizzare il loro comportamento sulle risorse (memoria differenziata, contesto), ed estrarre automaticamente una disciplina logica appropriata?
• Obiettivo: Costruire un "nucleo portante di teoremi" per il programma Architettura Neurale $\to$ Categoria $\to$ Logica, focalizzandosi specificamente sul comportamento sensibile alle risorse (resource-sensitive).

2. Metodologia

L'autore propone una pipeline costruttiva in quattro fasi:
$$\text{Famiglia di Architetture} \longrightarrow \text{Architettura Categorizzata} \longrightarrow \text{Firma Subesponenziale} \longrightarrow \text{Teoria della Dimostrazione}$$

A. Categorizzazione delle Architetture (Sezione 2)

1. Definizione di ArchZ: Viene definita una categoria $\mathbf{Arch}_Z$ i cui oggetti sono "contesti di risorse tipizzati" (liste finite di coppie $(z, A)$, dove $z$ è un'etichetta di zona e $A$ un oggetto di una categoria di base $\mathbf{Ctx}$). I morfismi sono "blocchi computazionali parametrizzati" definiti a meno di isomorfismo di riparametrizzazione.
2. Struttura Monoidale Simmetrica: Si dimostra che $\mathbf{Arch}_Z$ è una categoria monoidale simmetrica, dove il prodotto tensoriale corrisponde alla concatenazione dei contesti e la composizione alla sequenzialità dei blocchi.
3. Disciplina delle Zone Coerente: Per introdurre la sensibilità alle risorse, si definisce una "disciplina di zona coerente" ($\mathbf{Lic}$). Questa arricchisce la categoria con:
   • Un preordine sulle zone ($\preceq$).
   • Coercizioni tra zone.
   • Famiglie strutturali "autorizzate": discard (cancellazione) per alcune zone e diagonali (duplicazione) per altre.
   • Queste autorizzazioni sono vincolate dalla coerenza categoriale (naturalezza rispetto ai morfismi della categoria di base).

B. Estrazione della Firma Subesponenziale

Dalla disciplina coerente, l'autore estrae una firma subesponenziale $\Sigma_{\mathbf{Lic}} = (Z, \preceq, W, C)$, dove:

• $Z$ è l'insieme delle zone.
• $W$ è l'insieme delle zone che ammettono la regola di indebolimento (weakening/discard).
• $C$ è l'insieme delle zone che ammettono la regola di contrazione (contraction/duplicazione).
• Teorema di Ricostruzione Fedele: Viene dimostrato che le classi $W$ e $C$ estratte coincidono esattamente con le zone per cui la disciplina architetturale ha fornito famiglie di discard e diagonali autorizzate. La logica non è imposta dall'esterno, ma letta dai dati categoriali.

C. Teoria della Dimostrazione Estratta (Sezione 3)

Sulla base della firma estratta, viene definito un calcolo sequenziale tensoriale $T\mathcal{Z}_{\Sigma}$.

• Frammento: Il sistema include solo atomi, unità tensoriale, prodotto tensoriale e le regole strutturali (indebolimento e contrazione) indiciate dalle zone. Non include l'implicazione lineare (mancanza di struttura interna di omomorfismo nella fase attuale).
• Risultato Principale (Eliminazione del Taglio): Viene provato che il calcolo $T\mathcal{Z}_{\Sigma}$ ammette l'eliminazione del taglio (cut elimination). La dimostrazione si basa sulla chiusura del frammento tensoriale rispetto alle derivazioni senza taglio della logica lineare con subesponenziali standard.

D. Correttezza (Soundness) (Sezione 4)

L'ultimo passo è dimostrare che ogni derivazione logica corrisponde a un morfismo valido nell'architettura categorizzata originale.

• Viene definita una classe di diagrammi autorizzati ($\mathbf{Diag}_{\mathbf{Lic}}$) che include le strutture monoidali, le interfacce canoniche e, crucialmente, le famiglie di discard e diagonali autorizzate dalla disciplina.
• Teorema di Correttezza: Ogni derivazione in $T\mathcal{Z}_{\Sigma}$ è interpretata da un morfismo in $\mathbf{Diag}_{\mathbf{Lic}}$. In particolare, l'applicazione di una regola di indebolimento o contrazione nella logica corrisponde esattamente all'uso di un morfismo di discard o diagonale autorizzato nell'architettura.

3. Contributi Chiave

1. Definizione della Categoria $\mathbf{Arch}_Z$: Una formalizzazione categorica rigorosa di blocchi architetturali parametrizzati con etichette di zona.
2. Estrazione Inversa: La dimostrazione che la struttura logica (firma subesponenziale) può essere estratta dai dati architetturali e non deve essere presupposta.
3. Teoremi di Correttezza e Completezza Strutturale:
   • Il calcolo estratto è corretto rispetto ai diagrammi autorizzati dall'architettura.
   • Le regole strutturali della logica corrispondono esattamente alle operazioni di gestione delle risorse (copia/cancellazione) permesse dall'architettura.
4. Eliminazione del Taglio: La prova che il sistema logico estratto gode della proprietà di eliminazione del taglio, garantendo la consistenza e la normalizzazione delle dimostrazioni.
5. Esempi Concreti:
   • Un esempio astratto con tre zone (persistente, rilevante, lineare) che mappa direttamente su comportamenti logici noti.
   • Un esempio di architettura neurale a due blocchi (memoria persistente, contesto recuperato, osservazione corrente) che mostra come la logica estratta rifletta esattamente le politiche di riuso dei dati (es. la memoria persistente può essere duplicata e cancellata, l'osservazione corrente no).

4. Risultati

• Struttura Matematica: È stato stabilito che la categoria delle architetture categorizzate è monoidale simmetrica.
• Corrispondenza Logica: È stato provato che esiste una corrispondenza biunivoca tra le autorizzazioni strutturali dell'architettura (discard/diagonali) e le regole di indebolimento/contrazione della logica estratta.
• Validità: Il sistema logico derivato è "sound" (corretto) rispetto alla semantica categoriale originale.
• Non Vacuità: Gli esempi dimostrano che il programma di estrazione non è puramente teorico, ma produce logiche non banali per piccole reti neurali composizionali.

5. Significato e Impatto

Questo lavoro rappresenta un passo fondamentale verso una teoria unificata delle risorse nelle reti neurali.

• Cambio di Paradigma: Sposta l'attenzione dalla "logica che vincola le reti" alla "logica che emerge dalle reti". Questo è cruciale per comprendere come le diverse parti di un'architettura (es. memoria a lungo termine vs input corrente) impongano vincoli logici intrinseci.
• Fondazione per Estensioni: Sebbene il frammento attuale sia limitato (manca l'implicazione lineare), fornisce la base solida per estensioni future che includano omomorfismi interni o adjunzioni lineari-non lineari.
• Interdisciplinarità: Offre un linguaggio comune per i ricercatori di logica (che possono studiare modelli di subesponenziali derivati da dati reali) e per i ricercatori di deep learning (che possono formalizzare le proprietà di gestione delle risorse delle loro architetture).

In sintesi, il paper dimostra che la "disciplina logica" di un sistema neurale non è un'aggiunta esterna, ma una proprietà strutturale che può essere letta e formalizzata matematicamente partendo dalla sua organizzazione categoriale.