Theoria conecta prova formal e juízes LLM com verificação auditável

Um artigo publicado em 1º de julho no arXiv apresenta Theoria, uma arquitetura de verificação que fica entre assistentes de prova formal frágeis e juízes LLM opacos. Em vez de exigir Lean ou Coq, Theoria reescreve soluções candidatas em transições de estado tipadas, cada uma exigindo justificativa explícita — uma citação, computação ou fato dado pelo problema — antes que a transição seja licenciada. No HLE-Verified Gold (185 problemas apenas de texto de especialistas), Theoria certifica 105 soluções com precisão estrita de 91,4% (IC 95% Wilson [84,5%, 95,4%]). No GPQA Diamond (n=65), a precisão certificada atinge 97,1% (IC Wilson [85,1%, 99,5%]).

O design principal é o que os autores chamam de invariante de "completude da mudança": toda diferença entre estados de prova consecutivos deve ser contabilizada. Premissas ocultas—a classe de erro mais associada a saídas de LLM que soam confiantes mas estão erradas—aparecem como mutações não licenciadas em vez de passar silenciosamente. Esta é a garantia estrutural que juízes escalares não podem fazer. Uma pontuação de 0,87 não diz nada sobre qual etapa falhou ou por quê.

Em 95 provas envenenadas adversarialmente em 15 domínios, Theoria captura 94,7% dos erros injetados versus 83,2% para julgamento holístico de LLM (p=0,0017), uma lacuna de 11,5 pontos percentuais. A lacuna não é distribuída uniformemente. Para premissas ocultas, Theoria detecta 90,6% versus 62,5% para julgamento holístico — uma delta de 28 pp onde análise formal prediz uma vantagem. Para citações fabricadas, Theoria atinge 100% versus 90%. Para erros aritméticos e aplicação incorreta de teoremas, ambas as abordagens funcionam identicamente. As vitórias da arquitetura rastreiam as classes de erro onde rastreabilidade em nível de estado tem uma vantagem estrutural.

Para estratégias de conjunto, a complementaridade importa. Juízes LLM holísticos alcançam precisão comparável em cobertura equiparada. A sobreposição de Jaccard entre o que Theoria certifica e o que juízes holísticos aprovam é 0,14–0,36 — genuinamente esparsa, não ruído correlacionado. Executar ambos em um pipeline em etapas—Theoria para certificação rigorosa de saídas de alto risco, juízes holísticos para filtragem inicial rápida—não é redundante. Os dois métodos falham em diferentes problemas por design.

Theoria não elimina a compensação de cobertura. De 185 problemas do HLE-Verified Gold, 105 foram certificados; 80 não foram. Assistentes de prova formal cobrem ainda menos da distribuição real de problemas. Uma estimativa recente coloca os melhores LLMs provadores em 13% do PutnamBench resolvido formalmente, versus aproximadamente 83% para LLMs de raciocínio informal. A zona de Theoria é raciocínio informal tornando-se auditável, não prova formal de teoremas disfarçada.

Cada certificação Theoria produz um rastreamento de prova legível por humanos no qual cada etapa pode ser desafiada independentemente após o fato. Esta é a propriedade de trilha de auditoria que equipes orientadas por conformidade não tinham. Uma pontuação de juiz escalar não é um registro. Um rastreamento de transição de estado tipado com justificativas explícitas em cada etapa é. Se esse rastreamento satisfaz revisões regulatórias ou de segurança específicas é uma questão de implantação, mas o artefato agora existe para respondê-la.

Para equipes de plataforma ML enviando pipelines de agentes em contextos de codificação, planejamento ou finanças, a questão prática é onde na pilha inserir o verificador de Theoria. Não é uma proteção em tempo de execução—reescrever soluções em transições de estado tipadas não é uma operação de custo zero. É melhor posicionada como um portão pós-geração para saídas que disparam decisões de alto risco, ou como uma camada de auditoria em modo batch para registros de produção. Equipes já executando avaliações de LLM-como-juiz devem tratar Theoria como uma camada aditiva, não uma substituição, dada a sobreposição de Jaccard de 0,14–0,36.

O código e detalhes de benchmark ainda não estão vinculados publicamente no resumo do arXiv. Fique atento a um lançamento de repositório de Ben Slivinski e Michael Saldivar.