Resumo Técnico: Autores Não Confiáveis, Respostas Confiáveis

Declaração do Problema

O artigo aborda o desafio fundamental de responder perguntas sobre programas (por exemplo, alcançabilidade, validade de asserções) quando as ferramentas utilizadas para traduzir e analisar esses programas são não confiáveis. Abordagens tradicionais dependem ou de provar a correção de um único tradutor uma única vez (ex: CompCert) ou de validar cada execução de um único tradutor. No entanto, esses métodos assumem uma única "aresta" de tradução. O artigo argumenta que, em um ecossistema complexo envolvendo múltiplas linguagens de origem, diversos alvos de raciocínio e potenciais autores não confiáveis (incluindo LLMs), o processo de tradução forma um grafo de muitas linguagens e rotas. Neste grafo, cada tradução é um potencial ponto de falha. O problema central é como compor essas traduções heterogêneas, construídas de forma independente e potencialmente não confiáveis, em um sistema que forneça respostas confiáveis sem exigir a prova universal de cada componente.

Metodologia: O Cálculo de Traduções com Graduação de Fidelidade

Os autores propõem um cálculo formal e uma implementação de plataforma chamada hurdy-gurdy. A metodologia é construída sobre dois "planos" distintos que se encontram em um registro compartilhado:

1. O Plano de Uso (Respondendo Perguntas)

Este plano trata a tradução como um grafo onde os nós são linguagens e as arestas são pares de tradução.

• O Par e o Quadrado: A unidade fundamental é um par $(A, B)$ consistindo em um tradutor $T$, um retorno de alvo-para-origem $\Lambda$ e intérpretes compartilhados. Um par é validado via um quadrado comutativo direcional:
  • Exatidão: O comportamento da origem é igual ao comportamento do alvo transportado de volta (uma bisimulação sobre observáveis mantidos).
  • Sobre-aproximação: O comportamento da origem é simulado pelo comportamento do alvo (permitindo comportamentos espúrios, mas preservando os comportamentos da origem).
  • Decidibilidade: Para qualquer programa específico, o quadrado é verificado executando ambos os lados e comparando traços projetados. Se eles divergirem, a falha é localizada a um passo específico e um observável.
• Composição e Contratos: Rotas são caminhos compostos através do grafo. O contrato de uma rota é o encontro componente a componente dos contratos de seus saltos, definido por quatro eixos:
  • Classe de Garantia (Assurance Class): Uma hierarquia de nenhuma até reprodução (replay), por execução (per-run) e universal.
  • Direção: Exata ou sobre-aproximação.
  • Observáveis Mantidos: A interseção de observáveis preservados por cada salto (a perda acumula-se).
  • Custo: Medido pelo tempo de execução.
• Mecanismos de Confiança:
  • Reestabelecimento Per-Run: Mesmo um salto "confiável" pode ser validado dinamicamente se o oráculo do quadrado passar para a execução específica.
  • Corroboração de Ramo: Se duas rotas independentemente derivadas (prefixos diversos) concordarem com um veredito, a evidência é mais forte do que o grau individual de cada rota.
  • Assimetria Existencial/Universal:
    • Respostas Existenciais (Alcançável): Autocertificáveis. A testemunha do solver é transportada de volta e reproduzida no intérprete de origem. Se a reprodução exibir o comportamento, a resposta é verdadeira, independentemente de erros do tradutor (Base de Confiança: Adequação do Intérprete de Origem).
    • Respostas Universais (Inalcançável): Não são autocertificáveis. Estas dependem da composição de graus, concordância de ramos e certificados formais (ex: provas DRAT verificadas por verificadores verificados).

2. O Plano de Evolução (Expandindo o Grafo)

Este plano gerencia o crescimento do grafo de tradução.

• Geração Não Confiável: Pares são implementados por agentes LLM independentes a partir de briefings.
• O Ratchet (Trinquete): O sistema impõe um modelo de crescimento aditivo. Novas contribuições devem estender a cobertura sem invalidar vereditos anteriores.
• Demanda e Registro: Perguntas não respondíveis são registradas como "demanda". Recomendações para novos pares são geradas com base em evidências. O registro humano é o portão final; o sistema não responde perguntas autonomamente, apenas expande a capacidade de fazê-lo.

Principais Contribuições

1. Um Cálculo de Pares Direcionais e com Graduação de Fidelidade: Um framework formal onde a exatidão é um caso especial de sobre-aproximação, e a composição é definida por um encontro de "elo mais fraco" através de garantia, direção, perda e custo.
2. A Álgebra de Contratos: Um mecanismo para compor evidências heterogêneas. O artigo formaliza como verificações "por execução" e garantias "universais" se combinam, e como a perda (observáveis descartados) acumula-se ao longo de uma rota.
3. A Assimetria Existencial/Universal: Um princípio arquitetônico que distingue respostas que carregam testemunhas (autocertificáveis via reprodução na origem) de respostas que não o fazem (exigindo confiança graduada, ramos e certificados).
4. A Arquitetura de Dois Planos: Uma separação entre os planos de "uso" (respondendo) e "evolução" (construindo), permitindo que agentes não confiáveis construam o sistema enquanto a arquitetura garante a confiança através de verificações cruzadas, diversidade e o mecanismo de ratchet.
5. Mecanização: O núcleo composicional, incluindo o teorema de colagem, localização e os teoremas de assimetria de ponta a ponta, é mecanizado em Lean 4 (aprox. 1.250 linhas) com uma auditoria de axiomas limpa.

Resultados e Avaliação

O artigo avalia um "snapshot de julho de 2026" da plataforma hurdy-gurdy, construída inteiramente por agentes LLM sem revisão semântica humana do código.

• Cobertura e Correção: O sistema cobre 13 linguagens e 15 pares registrados. Ele compôs com sucesso rotas para RISC-V, AArch64, eBPF, Wasm, EVM, Python e outros.
  • Acordo de Ramo: Rotas duplas para RISC-V (derivada manualmente vs. derivada de Sail) e AArch64 concordaram em todas as 12 questões de alcançabilidade testadas, incluindo vereditos universais (inalcançável).
  • Benchmark de Conformidade: Um benchmark derivado de 78 questões do conjunto de testes RISC-V foi resolvido com 100% de acordo entre as rotas e 100% de correção contra o ground truth.
• Detecção de Defeitos: A arquitetura detectou 24 defeitos no código gerado por LLM, incluindo:
  • Decodificação silenciosa incorreta de instruções (ex: MUL como ADD) onde tanto o intérprete quanto o tradutor concordavam (um "ponto cego" detectado apenas pela diversidade externa).
  • Representações intermediárias malformadas toleradas por um solver, mas rejeitadas por outros.
  • Falhas na própria instrumentação da plataforma (ex: um adaptador de checker que aceitava provas falsas).
• Experimentos de Taxa de Escape: Mutações semânticas semeadas do tradutor RISC-V foram testadas contra os portões do sistema.
  • A "suíte de quadrados" (probes conjoined) capturou 51/55 mutantes.
  • Os 4 restantes foram capturados pelo benchmark derivado.
  • Zero escapes foram observados na rodada final, embora os autores notem que isso mede a família de mutação, não uma taxa de escape zero para todos os erros possíveis.
  • Falhas de modo comum (onde ambos os lados de um quadrado estão errados identicamente) foram capturadas apenas pelo ramo diverso (rota Sail) ou diferenciais externos, validando a necessidade de âncoras semânticas independentes.
• Experimento de Jogador LLM: Um agente LLM foi incumbido de responder perguntas usando a plataforma.
  • Em uma segunda iteração (v2), o jogador LLM alcançou 8/8 respostas corretas em questões difíceis de alcançabilidade BTOR2, enquanto um LLM sem auxílio alcançou 7/8.
  • Crucialmente, as respostas do jogador LLM foram acompanhadas por artefatos de evidência verificados por máquina (ex: testemunhas reproduzidas, certificados LRAT), enquanto o LLM sem auxílio dependia de "dizer-me-disse" e pontuações de confiança.
• Desempenho: O overhead do disciplina (verificar cada salto, reproduzir testemunhas) é pequeno comparado à chamada do solver. A tradução leva milissegundos; o solver domina o tempo.

Significância e Alegações

O artigo afirma que a confiança na tradução pode ser manufaturada pela arquitetura, em vez de confiar no autor.

• Postura de Sistemas Distribuídos: Trata os tradutores como componentes que falham, contendo a falha através de projeções declaradas, verificações decidíveis e rotas independentes, em vez de preveni-la via prova universal.
• O "Ratchet" da Confiança: O sistema é projetado para evoluir. A cobertura e a garantia crescem monotonicamente; vereditos anteriores são preservados mesmo quando o grafo se expande.
• Escopo Modesto: Os autores são explícitos ao dizer que o sistema é um "snapshot de capacidade datado". Não pretendem resolver a indecidibilidade ou substituir toda a verificação formal. O nível "provado" é habitado apenas para questões específicas e limitadas com certificados formais. O sistema depende da descarga empírica da adequação do intérprete e suposições de diversidade estrutural.
• A Assimetria: O artigo conclui que, para respostas existenciais, a confiança é "quase gratuita" (via reprodução), enquanto para respostas universais, o sistema deve "comprar" conscientemente a garantia através de níveis graduados, ramos e certificados.

O trabalho postula que um sistema construído sobre estes princípios pode permitir que autores não confiáveis (humanos ou IA) contribuam para uma infraestrutura de raciocínio verificada, desde que a arquitetura imponha verificações cruzadas rigorosas e contratos composicionais.