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

Resumo Técnico: Theorist Toolbox – Um Protocolo Verificado para Teoria Econômica Assistida por LLM

1. Definição do Problema
O artigo aborda uma assimetria estrutural na pesquisa econômica: economistas empíricos herdam ferramentas compartilhadas (pacotes, arquivos de replicação, guias), enquanto os teóricos frequentemente trabalham isoladamente, dependendo da disciplina individual em vez de uma infraestrutura compartilhada. Com os Modelos de Linguagem de Grande Escala (LLMs) agora capazes de produzir derivações matemáticas não triviais, a principal restrição para a teoria assistida por máquina deslocou-se da produção para a confiança. Os LLMs podem gerar provas fluentes e confiantes, porém incorretas (por exemplo, confundindo expectativas ex-ante com propriedades ex-post, ou confundindo cancelamentos com equilíbrio orçamentário). O problema central é como utilizar LLMs para a teoria econômica sem confiar em sua produção, especificamente em domínios onde a verificação formal via assistentes de prova (como o Lean) ainda não é o padrão.

2. Metodologia: O Protocolo de Verificação-Primeiro
O autor propõe um protocolo de "verificação-primeiro", instanciado como três métodos reutilizáveis (habilidades de Claude Code) que diferem em um único eixo: a intensidade e a fonte da verificação externa. Todos os três métodos utilizam a mesma base de modelo (Claude Opus 4.8), mas variam em seu aparato de verificação:

• Método 1: Passagem Única Disciplinada. Um único modelo gera uma prova completa sob uma disciplina de escrita estrita (sem lacunas retóricas, justificativa explícita de sinais, distinção entre afirmações provadas e conjecturadas). A verificação limita-se à consistência interna e ao auto-alerta de limitações.
• Método razão: Par Adversarial. Um fluxo de trabalho adversarial onde o Claude Opus 4.8 propõe um resultado e um segundo modelo independente (OpenAI Codex/gpt-5.5) atua como um verificador hostil tentando refutar a afirmação. O autor humano faz a triagem dos achados, distinguindo contraexemplos genuínos de falsos positivos. Este método inclui verificações numéricas de Monte Carlo.
• Método 3: Projeto Multi-Agente. Um fluxo de trabalho de pesquisa estruturado inspirado pelo "co-matemático de IA" (Zheng et al., 2026). Ele decompõe o problema em fluxos de trabalho (literatura, prova, codificação) com um "portão de revisão" permanente. Opera em "modo estrito", exigindo que cada lacuna seja sinalizada com tags \unproven{}. Um portão de revisão deve aprovar os subobjetivos antes que sejam contados como concluídos. Este método incorpora o Método 2 como um componente para verificações rigorosas.

3. O Campo de Teste (Exemplo Prático)
O protocolo é avaliado em um problema de desenho de mecanismos aberto, sobreposto ao modelo de eigengrade de Gans–Kominers (2026) sobre inflação de notas.

• Contexto: O modelo trata o desempenho do estudante como $P_{ic} = a_i - d_c + \epsilon_{ic}$, onde $a_i$ é a habilidade e $d_c$ é a dificuldade do curso. O estimador de eigengrade recupera a habilidade usando um Laplaciano de grafo da rede de matrícula.
• A Lacuna: Embora os eigengrades alcancem neutralidade estratégica, eles não internalizam a externalidade informacional: cada decisão de matrícula ou de nota afeta a precisão da estimativa de habilidade de todos (governada pelo traço da pseudoinversa do Laplaciano, $tr(L^+)$).
• A Pergunta: É possível desenhar um mecanismo para internalizar essa externalidade (precificando a "resistência efetiva" do grafo) para induzir o relato verdadeiro ou a matrícula eficiente, dadas as restrições de equilíbrio orçamentário e a ausência de um numerário monetário para os instrutores?

4. Principais Resultados por Método

• Passagem Única (P1): Produziu um mecanismo de matrícula polido, do lado do aluno, utilizando uma transferência de Groves (em créditos de mensalidade/prioridade) para internalizar a externalidade de matrícula. Identificou corretamente a impossibilidade de equilíbrio orçamentário (Green–Laffont), mas não carregava verificação numérica.
• Par Adversarial (P2): Produziu uma transferência de lado do instrutor do tipo Pigouviana que implementa a graduação profissional em estratégias dominantes. Crucialmente, o verificador adversarial detectou três erros significativos na proposta inicial:
  1. Refutou uma afirmação de neutralidade de incentivos ex-post (mostrando que ela se mantém apenas em expectativa).
  2. Provou que uma transferência de estratégia dominante com equilíbrio orçamentário é impossível (via uma derivada mista não nula).
  3. Corrigiu uma afirmação de que um estimador leave-one-out era necessário para a exatidão do primeiro momento (mostrando que o estimador padrão já possuía essa propriedade).
• Projeto Multi-Agente (P3): Produziu uma suíte de mecanismos "sem dinheiro" no espaço de relatório. Derivou o mesmo núcleo de resistência efetiva que P1, mas na margem intensiva (fidelidade de graduação). O portão de revisão rejeitou um subobjetivo que tentava usar predição de pares (que falhou em elicitar sinais privados) e forçou um resultado de existência condicional (exigindo um box de ação compacto). O output listou explicitamente obrigações não provadas.

5. Três Fenômenos Observados
A comparação das três execuções rendeu três achados transferíveis:

1. Descoberta Convergente: P1 (margem do aluno) e P3 (margem do instrutor), trabalhando de forma independente com enquadramentos diferentes, derivaram exatamente o mesmo objeto matemático: o núcleo de resistência efetiva $\|\Pi L^+ b_e\|^2$. Essa convergência aumentou a confiança de que o objeto é uma característica do problema, não um artefato do modelo.
2. A Verificação Adversarial é Estrutural: O par adversarial (P2) detectou três afirmações falsas que uma passagem única teria publicado. A maquinaria de verificação não foi decorativa; foi essencial para a correção.
3. Polimento Não é Rigor: O output que parecia mais "finalizado" (P1) foi o menos verificado. O output mais "irregular" (P3), coberto de flags e obrigações não provadas, foi o mais confiável porque nomeou explicitamente o que não sabia.

6. Significância e Alegações
O artigo alega oferecer um protocolo para o praticante em vez de um novo teorema ou um escore de benchmark. Sua significância reside em:

• Alterar a Variável de Design: Argumentar que, para a teoria assistida por máquina, a escolha de design crítica não é a capacidade do modelo, mas o aparato de verificação externa.
• Definir um Entregável Realista: O objetivo não é um teorema certificado (o que exige formalização ainda não disponível em economia), mas uma "fronteira de pesquisa disciplinada": um núcleo verificado, mecanismos funcionais, resultados negativos honestos e um registro explícito de questões abertas.
• Transferibilidade Metodológica: O protocolo é desenhado para ser aplicável a qualquer problema de teoria econômica onde se busca assistência de máquina sem permitir "vagueza".

O autor observa explicitamente as limitações: a evidência baseia-se em um único exemplo prático executado por um operador com pares de modelos específicos. Os fenômenos relatados são demonstrações de possibilidade e comportamento, não taxas de sucesso medidas. O artigo conclui que a verificação externa, e não a confiança do modelo, é a salvaguarda necessária para a teoria econômica assistida por máquina.