Riepilogo Tecnico: Metaprogrammazione Governata per Sistemi Intelligenti

1. Enunciato del Problema

I sistemi AI moderni, inclusi i Modelli Linguistici di grandi dimensioni (LLM) e gli agenti autonomi, sintetizzano sempre più strutture eseguibili a runtime. Questi sistemi generano flussi di lavoro, piani di chiamata degli strumenti e codice auto-modificante. Nelle lingue omiconiche classiche (ad es. Lisp) e nelle lingue a stadi (ad es. MetaOCaml), la transizione da una rappresentazione di codice (dati) a un programma eseguibile è gestita da primitive come eval o run. Queste transizioni sono tradizionalmente illimitate: qualsiasi rappresentazione valida può immediatamente diventare codice in esecuzione.

Nel contesto di sistemi intelligenti governati—che richiedono confini espliciti degli effetti, controllo delle capacità e auditabilità—questa transizione illimitata crea una vulnerabilità critica. Se un sistema può generare un nuovo programma che aggira i vincoli di governance del originale, l'intero modello di governance è compromesso. Il documento identifica questo come una "via di fuga per la metaprogrammazione": un sistema governato a livello di esecuzione ma non governato a livello di generazione del codice è fondamentalmente insicuro.

2. Metodologia Principale: Riclassificazione di eval

Il contributo metodologico centrale del documento è la riclassificazione di eval (o la transizione dalla forma all'esecuzione) da una primitiva linguistica a un effetto governato.

Gli autori propongono un framework chiamato Metaprogrammazione Governata, basato sui seguenti pilastri:

• Forme Macchina: Le rappresentazioni dei programmi sono trattate come valori di prima classe (mappe di dati strutturati) piuttosto che come stringhe opache o bytecode.
• Manipolazione Pura delle Forme: Tutte le operazioni su queste forme (ispezione, trasformazione, composizione, differenziazione) sono classificate come computazione pura. Non emettono direttive e non possiedono capacità di eseguire I/O o invocare modelli.
• Materializzazione come Allocazione di Autorità: La transizione da una forma macchina a una macchina eseguibile è definita come materializzazione. Questo non è mera computazione; è l'allocazione di autorità eseguibile (il potere di invocare modelli, eseguire I/O e consumare risorse). Di conseguenza, la materializzazione è classificata come un effetto governato.
• Ispezione Strutturale: Prima che la materializzazione sia permessa, un sistema di governance esegue un'ispezione strutturale decidibile della forma. Questa ispezione analizza i requisiti di capacità, la conformità alle policy, l'autorizzazione del modello e le stime delle risorse.

3. Semantica Operativa Formale

Il documento formalizza il sistema utilizzando due giudizi distinti per imporre il confine tra computazione pura ed esecuzione governata:

1. Valutazione Pura della Forma ($\Gamma \vdash pure\ e \Downarrow v$):

   • Opera su valori di forma.
   • Emette zero direttive ($Dir(e) = \emptyset$).
   • Include la costruzione di quote, la valutazione di splice, la navigazione e la trasformazione.
   • Garantisce che nessuna sequenza di operazioni pure possa produrre una macchina autorizzata.

2. Materializzazione Governata ($\Gamma; \Pi; \sigma \vdash materialize(v_f) \rightsquigarrow \langle Machine, d \rangle$):

   • Prende una forma, un contesto di policy ($\Pi$) e un insieme di capacità ($\sigma$).
   • Richiede un registro di decisione di governance ($d$) per ogni esito (approvazione o rifiuto).
   • Emette esattamente una direttiva governata.
   • Il sistema di governance ispeziona la struttura della forma per verificare:
     • Contenimento delle capacità ($CapSet(f) \subseteq \Pi.allowed\ caps$).
     • Autorizzazione del modello.
     • Conformità strutturale alla policy.
     • Limiti delle risorse.

4. Contributi Chiave

Il documento presenta cinque contributi principali:

1. Riclassificazione di eval: Una caratterizzazione precisa della materializzazione come allocazione di autorità, spostandola da una primitiva a un effetto governato.
2. Forme Macchina: Un tipo di dato concreto per la rappresentazione strutturata dei programmi con costrutti per quote, splice e reflection.
3. Semantica Formale: Una definizione del sistema utilizzando due giudizi (valutazione pura e materializzazione governata) che separa rigorosamente la manipolazione dei dati dall'esecuzione.
4. Proprietà Verificate da Macchina: Tre proprietà fondamentali sono verificate formalmente in Rocq:
   • Purezza della Manipolazione delle Forme: Le operazioni sulle forme non emettono direttive.
   • Il Teorema del Non-Aggiramento: Nessuna sequenza di operazioni pure può causare direttamente l'esecuzione.
   • Preservazione del Confine: L'aggiunta di capacità di metaprogrammazione non divide i confini di espressività e governance (rimangono coincidenti).
5. Auto-Modifica Governata: Un meccanismo concreto che permette alle macchine di proporre modifiche strutturali a se stesse tramite un registro di evoluzione, soggetto alla stessa ispezione di governance della generazione di codice esterna.

5. Implementazione e Risultati

Il design è implementato in MashinTalk, un linguaggio specifico di dominio per flussi di lavoro AI che compila in bytecode BEAM (macchina virtuale Erlang).

• Architettura di Sistema: L'implementazione consiste in tre moduli: Form (costruzione e manipolazione), FormInspector (controlli di governance) e FormMaterializer (compilazione governata).
• Verifica: Le proprietà fondamentali sono meccanizzate in Rocq (precedentemente Coq) con 26 teoremi e 662 righe di codice, con zero lemma ammessi. Questi teoremi si integrano con una formalizzazione esistente di 454 teoremi su 36 moduli.
• Test: Una suite di test di 51 test unitari convalida la correttezza funzionale e le proprietà di governance. Tutti i test superano.
• Prestazioni: Sui processori Apple serie M, la costruzione della forma richiede <1 µs e l'ispezione strutturale richiede <100 µs per macchine tipiche. L'overhead è trascurabile rispetto alla compilazione in bytecode BEAM.

6. Significato e Affermazioni

Il documento afferma di chiudere la "via di fuga per la metaprogrammazione" nei sistemi intelligenti governati. Senza questo meccanismo, un sistema governato a livello di esecuzione rimane vulnerabile perché non può governare la generazione di nuove strutture eseguibili.

Gli autori sostengono che nei sistemi AI che sintetizzano la propria struttura eseguibile, l'allocazione dell'autorità eseguibile deve essere:

1. Visibile: La transizione dai dati al codice è un evento distinto e osservabile.
2. Mediata: Deve passare attraverso un interprete di governance che ispeziona la struttura.
3. Registrata: Le decisioni sono registrate in un registro append-only (il registro di evoluzione).

Il documento riconosce esplicitamente i limiti:

• Teorema di Rice: L'ispezione strutturale è decidibile ma non può ragionare sul comportamento semantico. La governance garantisce la mediazione, non la correttezza semantica del programma generato.
• Ambito: L'argomento sulla preservazione del confine è architetturale; una prova completa di conservatività riguardo agli insiemi di firme degli effetti è rimandata a lavori futuri.
• Applicabilità: Il design è specifico per linguaggi con strutture di confine degli effetti (come MashinTalk); la sua applicabilità ai linguaggi di scopo generale è una domanda aperta.

In conclusione, il documento stabilisce che eval non è meramente una funzione computazionale ma un evento di allocazione di autorità. Trattandolo come un effetto governato, i sistemi intelligenti possono sintetizzare e modificare in sicurezza le proprie strutture eseguibili senza compromettere i propri modelli di governance.