Theorist Toolbox: Tools for Agent Based LLM-assisted economic theory Research

Sintesi Tecnica: Theorist Toolbox – Un Protocollo Verificato per la Teoria Economica Assistita da LLM

1. Definizione del Problema
Il documento affronta un'asimmetria strutturale nella ricerca economica: mentre gli economisti empirici ereditano strumenti condivisi (pacchetti, archivi di replicazione, guide), i teorici spesso lavorano in isolamento, affidandosi alla propria disciplina individuale piuttosto che a un'infrastruttura condivisa. Con i Large Language Models (LLM) ora capaci di produrre derivazioni matematiche non banali, il vincolo primario per la teoria assistita da macchine si è spostato dalla produzione alla fiducia. Gli LLM possono generare dimostrazioni fluide e sicure, ma errate (ad esempio, confondendo le aspettative ex-ante con le proprietà ex-post, o scambiando le cancellazioni per il bilancio di bilancio). Il problema centrale è come utilizzare gli LLM per la teoria economica senza fidarsi del loro output, specificamente in domini in cui la verifica formale tramite assistenti alla dimostrazione (come Lean) non è ancora uno standard.

2. Metodologia: Il Protocollo "Verification-First"
L'autore propone un protocollo "verification-first" (verifica prima di tutto), istanziato in tre metodi riutilizzabili (competenze di Claude Code) che differiscono lungo un unico asse: l'intensità e la fonte della verifica esterna. Tutti e tre i metodi utilizzano lo stesso modello base (Claude Opus 4.8) ma variano nel loro apparato di verifica:

• Metodo 1: Passaggio Disciplinato Singolo. Un singolo modello genera una dimostrazione completa sotto una stretta disciplina di scrittura (assenza di lacune retoriche, giustificazione esplicita dei segni, distinzione tra affermazioni provate e congetturali). La verifica è limitata alla coerenza interna e all'auto-segnalazione dei limiti.
• Metodo 2: Coppia Avversaria. Un workflow avversario in cui Claude Opus 4.8 propone un risultato e un secondo modello indipendente (OpenAI Codex/gpt-5.5) agisce come un verificatore ostile tentando di confutare l'affermazione. Un autore umano effettua il triage dei risultati, distinguendo tra veri controesempi e falsi positivi. Questo metodo include controlli Monte Carlo numerici.
• Metodo 3: Progetto Multi-Agente. Un workflow di ricerca strutturato ispirato al "co-matematico IA" (Zheng et al., 2026). Decompone il problema in flussi di lavoro (letteratura, dimostrazione, codifica) con un "cancello di revisione" permanente. Opera in "modalità rigorosa", richiedendo che ogni lacuna sia contrassegnata con tag \unproven{}. Un cancello di revisione deve approvare i sotto-obiettivi prima che siano conteggiati come completati. Questo metodo incorpora il Metodo 2 come componente per controlli rigorosi.

3. Il Testbed (Esempio Applicativo)
Il protocollo è valutato su un singolo problema di meccanismo del design aperto, stratificato sul modello di inflazione dei voti (grade inflation) di Gans–Kominers (2026).

• Contesto: Il modello tratta la performance dello studente come $P_{ic} = a_i - d_c + \epsilon_{ic}$, dove $a_i$ è l'abilità e $d_c$ è la difficoltà del corso. Lo stimatore dell'eigengrade recupera l'abilità utilizzando un Laplaciano del grafo delle iscrizioni.
• La Lacuna: Sebbene gli eigengrade raggiungano la neutralità strategica, essi non internalizzano l'esternalità informativa: ogni decisione di iscrizione o di valutazione influenza la precisione della stima dell'abilità di tutti (governata dalla traccia della pseudoinversa del Laplaciano, $tr(L^+)$).
• La Domanda: È possibile progettare un meccanismo per internalizzare questa esternalità (prezzando la "resistenza effettiva" del grafo) per indurre la segnalazione veritiera o l'iscrizione efficiente, dati i vincoli del bilancio di bilancio e l'assenza di un numerario monetario per gli istruttori?

4. Risultati Chiave per Metodo

• Passaggio Singolo (P1): Ha prodotto un meccanismo di iscrizione lato studente rifinito, utilizzando un trasferimento di Groves (in crediti di iscrizione/priorità) per internalizzare l'esternalità di iscrizione. Ha identificato correttamente l'impossibilità del bilancio di bilancio (Green–Laffont), ma non conteneva alcuna verifica numerica.
• Coppia Avversaria (P2): Ha prodotto un trasferimento pigouviano lato istruttore che implementa la valutazione professionale in strategie dominanti. Fondamentalmente, il verificatore avversario ha colto tre errori significativi nella proposta iniziale:
  1. Ha disproofato una pretesa di neutralità incentiva ex-post (mostrando che essa vale solo in media).
  2. Ha dimostrato che un trasferimento a strategia dominante con bilancio di bilancio è impossibile (tramite una derivata mista non nulla).
  3. Ha corretto l'affermazione che fosse necessario un estimatore "leave-one-out" per l'esattezza del primo momento (mostrando che lo stimatore standard possedeva già tale proprietà).
• Progetto Multi-Agente (P3): Ha prodotto una suite di meccanismi "senza denaro" nello spazio dei report. Ha derivato lo stesso kernel di resistenza effettiva di P1, ma sul margine intensivo (fedeltà della valutazione). Il cancello di revisione ha rifiutato un sotto-obiettivo che tentava di usare la peer prediction (che non aveva elicitato i segnali privati) e ha imposto un risultato di esistenza condizionale (richiedendo un box di azione compatto). L'output elencava esplicitamente le obbligazioni non provate.

5. Tre Fenomeni Osservati
Il confronto tra i tre run ha prodotto tre risultati trasferibili:

1. Scoperta Convergente: P1 (margine studente) e P3 (margine istruttore), lavorando indipendentemente con inquadramenti diversi, hanno derivato esattamente lo stesso oggetto matematico: il kernel di resistenza effettiva $\|\Pi L^+ b_e\|^2$. Questa convergenza ha aumentato la fiducia nel fatto che l'oggetto sia una caratteristica del problema e non un artefatto del modello.
2. La Verifica Avversaria è Portante: La coppia avversaria (P2) ha colto tre false affermazioni che un passaggio singolo avrebbe pubblicato. L'apparato di verifica non era decorativo; era essenziale per la correttezza.
3. La Lucidità Non è Rigore: L'output più "rifinito" (P1) era il meno verificato. L'output più "frastagliato" (P3), coperto di flag e obbligazioni non provate, era il più affidabile perché nominava esplicitamente ciò che non sapeva.

6. Significato e Rivendicazioni
Il documento sostiene di offrire un protocollo per professionisti piuttosto che un nuovo teorema o un punteggio di benchmark. La sua importanza risiede nel:

• Spostare la Variabile di Design: Argomentare che, per la teoria assistita dalle macchine, la scelta di design critica non è la capacità del modello, ma l'apparato di verifica esterno.
• Definire un Risultato Realistico: L'obiettivo non è un teorema certificato (che richiederebbe una formalizzazione non ancora disponibile in economia) ma una "frontiera di ricerca disciplinata": un nucleo verificato, meccanismi funzionanti, risultati negativi onesti e un registro esplicito di domande aperte.
• Trasferibilità Metodologica: Il protocollo è progettato per essere applicabile a qualsiasi problema di teoria economica in cui si cerchi l'assistenza della macchina senza permettere il "parlare a vanvera" (hand-waving).

L'autore nota esplicitamente i limiti: l'evidenza si basa su un singolo esempio eseguito da un unico operatore con accoppiate di modelli specifiche. I fenomeni riportati sono dimostrazioni di possibilità e comportamento, non tassi di successo misurati. Il documento conclude che la verifica esterna, e non la fiducia del modello, è la salvaguardia necessaria per la teoria economica assistita dalle macchine.