Structural Enforcement of Statistical Rigor in AI-Driven Discovery: A Functional Architecture

Resumo Técnico: Imposição Estrutural de Rigor Estatístico na Descoberta Impulsionada por IA

Definição do Problema
Sistemas de Cientista de IA, que utilizam Modelos de Linguagem de Grande Escala (LLMs) para gerar, implementar e avaliar hipóteses científicas, enfrentam duas ameações críticas à integridade estatística:

1. Testes Múltiplos Não Controlados: Quando sistemas automatizados testam milhares de hipóteses, a aplicação ingênua de um limiar de significância fixo (ex: $\alpha = 0,05$) leva a uma inflação massiva da Taxa de Descoberta Falsa (FDR - False Discovery Rate). Sem correção, a maioria das "descobertas" relatadas pode ser espúria.
2. Vazamento de Dados e P-valores Enviesados: Em arquiteturas híbridas onde os LLMs geram código Python, há o risco de o código gerado acessar inadvertidamente dados de validação durante a fase de otimização. Isso produz p-valores artificialmente baixos que tornam qualquer correção estatística subsequente (como o controle de FDR) sem sentido, pois os p-valores subjacentes são enviesados.

Métodos existentes de controle de FDR online (ex: LORD++) fornecem garantias matemáticas, mas estes dependem de suposições (como a independência de p-valores futuros em relação a decisões passadas e a validade dos p-valores em si) que implementações de software padrão podem violar silenciosamente.

Metodologia: Uma Arquitetura de Defesa em Profundidade
Os autores propõem uma arquitetura funcional que impõe rigor estatístico através de duas camadas complementares: uma eDSL (Linguagem de Domínio Específico Embarcada) de nível macro em Haskell e um andaime declarativo de nível micro apoiado por isolamento ao nível do Sistema Operacional (SO).

1. Nível Macro: O Monad de Pesquisa (Haskell)

   • Função: Esta eDSL impõe o protocolo LORD++ estruturalmente. Ela trata o nível de significância como um "orçamento de erro" (riqueza-$\alpha$).
   • Mecanismo: Utilizando um transformador StateT sobre um monad ExceptT, o sistema percorre o estado estatístico (riqueza, tempos de descoberta, carimbos de data/hora) através de cada operação.
   • Imposição: É estruturalmente impossível testar uma hipótese sem atualizar o estado. O sistema de tipos garante que os limiares sejam calculados baseando-se apenas em informações passadas (previsibilidade), impedindo que o código "espie" p-valores futuros. Se ocorrer uma violação de protocolo (ex: um carimbo de data/hora não sequencial), a computação é interrompida imediatamente.

2. Nível Micro: Andaime Declarativo e Sandboxing ao Nível do SO

   • Função: Esta camada garante que os p-valores fornecidos ao Monad de Pesquisa sejam não enviesados e que o código gerado pelo LLM não acesse dados de validação.
   • Mecanismo: O orquestrador Haskell gera um invólucro (harness) Python rígido antes que o LLM escreva qualquer lógica de domínio. Este invólucro:
     • Impõe a Separação de Dados: A função optimize do LLM recebe apenas a divisão de exploração de dados. A divisão de validação é carregada exclusivamente pelo invólucro durante a fase de validação.
     • Padroniza Testes: O invólucro executa um teste de permutação de inversão de sinal pareado em perdas por exemplo retidas, garantindo que os p-valores nulos sejam superuniformes.
     • Isolamento ao Nível do SO: A etapa de otimização roda dentro de um namespace de usuário e de montagem (mount namespace) não privilegiado do Linux. O diretório de dados dentro deste namespace é uma visão que contém apenas a divisão de exploração. Consequentemente, o arquivo de validação está fisicamente ausente do sistema de arquivos visível para o código de otimização, tornando o vazamento de dados impossível, independentemente das tentativas de caminho de arquivo do código.

3. Cadeia de Verificação Formal
   Para preencher a lacuna entre a teoria matemática e a implementação de ponto flutuante, os autores construíram uma cadeia verificada:

   • Formalização em Lean 4: O teorema LORD++ é formalizado em Lean 4, derivando o orçamento de erro e provando o controle de FDR marginal e total. Esta formalização identifica quatro condições necessárias para uma implementação:
     • (H1) P-valores uniformes/superuniformes.
     • (H2) Previsibilidade de limiares.
     • (H3) Independência de p-valores futuros em relação a decisões passadas.
     • (H4) Não-negatividade do processo de riqueza.
   • Verificação SPARK/Ada: A condição aritmética (H4) é verificada usando SPARK/Ada. A atualização da riqueza é implementada usando multiplicação em vez de subtração para garantir a não-negatividade sob erros de arredondamento IEEE 754. A ferramenta GNATprove verifica que o invariante de riqueza se mantém para todos os passos, resolvendo 30 condições de verificação sem o uso de sorry (alegações não provadas).

Resultados Principais

• Estudo de Simulação: Em uma simulação de Monte Carlo de 2.000 hipóteses, uma abordagem ingênua resultou em uma FDR empírica de 41% contra um alvo de 5%. A arquitetura proposta de LORD++ via monad controlou a FDR em 1,1%, demonstrando correção eficaz.
• Estudos de Caso (Conjunto de Dados Wine):
  • Ao utilizar um teste t de validação cruzada falho (que infla a significância devido a dobras sobrepostas), o sistema relatou três descobertas falsas.
  • Ao utilizar o teste de permutação estruturalmente imposto em divisões disjuntas, o sistema identificou corretamente que nenhuma das hipóteses era significativa, evitando falsos positivos enquanto mantinha a capacidade de detectar efeitos reais quando os dados eram suficientes (demonstrado em um benchmark maior de make_moons).
• Avaliação Adversária: Em um teste de segurança onde um LLM foi explicitamente instruído a localizar e ler dados de validação, o sandbox ao nível do SO alcançou uma taxa de vazamento de 0,00%. O arquivo de validação estava fisicamente inacessível ao processo de otimização, enquanto uma linha de base baseada apenas em prompt resultou em uma taxa de vazamento de 100%.

Significância e Alegações
O artigo afirma apresentar a primeira cadeia verificada do teorema à implementação de ponto flutuante para um procedimento de FDR online. Sua significância reside em:

• Imposição Estrutural: Ir além de "pedir" ao LLM para ser cuidadoso, tornando os erros estatísticos estruturalmente impossíveis via sistemas de tipos e isolamento de SO.
• Rigor Formal: Fornecer uma prova verificada por máquina (Lean 4) do teorema de controle de FDR e uma implementação aritmética verificada (SPARK) que considera erros de arredondamento IEEE 754, garantindo que as garantias matemáticas se sustentem na prática.
• Defesa em Profundidade: Abordar tanto a contabilidade estatística (macro) quanto a integridade dos dados (micro) necessárias para a descoberta científica autônoma.

Os autores observam que, embora a arquitetura previna o vazamento de dados e a inflação de FDR, ela não garante a correção semântica da lógica de domínio específica gerada pelo LLM (ex: se o LLM escolher uma estratégia de otimização cientificamente infundada). No entanto, ela reduz significativamente a superfície de dano de tais erros, garantindo que mesmo experimentos falhos não produzam alegações estatísticas espúrias.