[IA na veIA nº 43] Quem fiscaliza o Skynet dos próprios agentes?

Sumário

---

O que é IA na veIA?

IA na veIA é uma iniciativa que explica os avanços da inteligência artificial com bom humor e analogias divertidas vindas direto do universo Geek. Aqui, conceitos complexos ganham vida através de comparações com filmes, séries, games e HQs, tornando a tecnologia mais próxima e muito mais divertida para todos.

A missão é democratizar o conhecimento sobre inteligência artificial, aproximando a comunidade científica do público leigo sem aquele “tecniquês” que dá sono. Ao usar referências de sagas épicas, super-heróis ou mundos de fantasia, transformamos pesquisas e inovações em histórias que qualquer fã de cultura pop entende e curte.

Essa abordagem cria uma ponte entre especialistas e curiosos, incentivando debates sobre o impacto ético, social e econômico da IA de forma leve, mas consciente. O resultado é uma conversa mais inclusiva, onde qualquer pessoa pode entender e participar da construção do nosso futuro tecnológico.

Se você é fã de IA e também vibra com referências Geek, o IA na veIA é o seu portal para explorar ciência com uma boa dose de risadas e imaginação.

Vamos revisar o paper a seguir:

• FormalJudge: A Neuro-Symbolic Paradigm for Agentic Oversight
• Link do paper

---

Quem é Celso Sousa?

Celso Sousa é especialista e palestrante de inteligência artificial (IA), com doutorado em IA pela USP. Além disso, ele possui mais de 15 anos de experiência no mercado de IA para negócios.

Celso participou da gestão e/ou desenvolvimento de diversos projetos de IA nos setores financeiro e agronegócio. Alguns dos projetos de inteligência artificial mais relevantes na carreira dele são:

• previsão de produtividade de fazendas;
• reconhecimento visual de nematóides;
• visão computacional para monitoramento de rebanhos por drones;
• identificação de públicos vulneráveis;
• sistema de gerenciamento de pastejo rotacionado;
• identificação de irregularidades em notas fiscais de serviço.

Celso ministrou vários treinamentos e mentorias sobre inteligência artificial nos últimos anos. Ainda mais, ele foi Cientista Chefe na Secretaria das Finanças de Fortaleza-CE na auditoria fiscal.

O foco do Celso é desenvolver soluções de IA para empresas de todos os portes e segmentos. Entretanto, a prioridade é criar soluções de IA de baixo custo para empresas de pequeno e médio porte.

Celso iniciou a sua carreira ao abrir uma consultoria de inteligência artificial em 2009. Portanto, ele adquiriu muita experiência prática de como gerar resultados expressivos para as empresas usando IA.

A pesquisa científica do Celso é sobre classificação em grafos para alavancagem de negócios com marketing analytics. Além disso, ele publicou artigos científicos em diversas conferências internacionais de renome em 4 continentes.

Hoje ele aplica sua experiência na IA para ajudar os empresários a aumentarem os seus lucros. Ainda mais, ele implementa automações com agentes de IA para que os empresários tenham mais liberdade.

Essas automações podem ser aplicadas em diversos setores, como marketing, vendas, recursos humanos, tecnologia, financeiro, atendimento, etc.

Fale com o especialista e palestrante de inteligência artificial Celso Sousa nas redes sociais:

• Instagram: https://www.instagram.com/celsosousaia
• LinkedIn: https://www.linkedin.com/in/celso-sousa/

---

Visão geral do paper

A indústria de IA adora repetir que estamos construindo agentes cada vez mais autônomos, quase como se estivéssemos treinando novos Jedi para operar no mundo real. Só que esses Jedi às vezes confundem o lado da Força com o lado sombrio, e o pior é que quem está julgando esses erros costuma ser outro modelo igualmente probabilístico. Essa é a essência do problema de scalable oversight, que Anwar et al discutem ao mostrar que supervisionar sistemas cada vez mais poderosos com ferramentas frágeis é como colocar um estagiário para revisar o código do Thanos.

Bommasani et al já haviam alertado que modelos fundacionais carregam riscos sistêmicos difíceis de mitigar apenas com ajustes de prompt. Ji et al reforçam que alinhamento não é só RLHF e boas intenções, mas um problema estrutural de garantias. E quando Ji et al analisam alucinações, fica claro que LLMs compartilham vieses de treinamento, criando câmaras de eco onde um modelo valida a fantasia do outro como se fosse canon oficial da Marvel.

O paradigma LLM-as-a-Judge surgiu como solução pragmática, mas é basicamente pedir para um mago avaliar o feitiço de outro mago usando a mesma gramática arcana. Li et al mostram que a prática virou padrão, mas Yao et al já demonstraram que alucinação não é bug isolado, é comportamento emergente. Quando dois modelos treinados na mesma sopa de dados se avaliam, o risco é virar uma raid em WoW onde todo mundo confirma que o boss morreu, mesmo ele ainda estando com 30% de HP.

Formal verification aparece como alternativa quase herética nesse cenário dominado por probabilidade. Klein mostrou que dá para verificar um kernel inteiro com provas matemáticas, e Leroy fez o mesmo com compiladores, mostrando que certas propriedades podem ser garantidas além da retórica. Katz e Huang avançaram na verificação de redes neurais, mas a tradução entre linguagem natural e especificação formal sempre foi o dragão final desse RPG.

Ma et al começaram a explorar como LLMs podem gerar especificações formais, mas ainda dentro de domínios controlados. A lacuna sempre foi: como transformar intenções humanas ambíguas em contratos lógicos verificáveis sem exigir um doutorado em métodos formais? Resolver isso não é capricho acadêmico, é diferença entre um agente que inventa um relatório médico e um sistema que prova matematicamente que não violou restrições críticas.

---

FORMALJUDGE: quando o Oráculo encontra o compilador de código

Jiayi Zhou et al entram nesse debate como quem chega em uma guilda cansada de wipes e diz que o problema não é DPS, é estratégia. Eles propõem o FORMALJUDGE, um paradigma neuro-simbólico que transforma o juiz em algo mais próximo de um verificador formal do que de um comentarista probabilístico. A ideia central é simples e radical: separar o que é semântico do que é lógico.

Zhou et al tratam LLMs como compiladores de especificação, não como árbitros finais. O modelo de linguagem decompõe a intenção humana em fatos atômicos binários, e depois esses fatos são compostos logicamente em Dafny e verificados pelo Z3. É como se o LLM fosse o narrador do RPG, mas quem decide se a ação é válida segundo as regras fosse um sistema de regras imutável.

Do Chain-of-Thought ao Formal-of-Thought

Enquanto Wei et al popularizaram Chain-of-Thought como forma de melhorar raciocínio, Zhou et al introduzem o que chamam de Formal-of-Thought. Em vez de pedir que o modelo “pense melhor”, eles limitam o modelo a responder perguntas simples de sim ou não sobre fatos observáveis. A composição desses fatos vira uma prova formal.

A inovação aqui não é só técnica, é epistemológica. O julgamento deixa de ser um score subjetivo e passa a ser uma propriedade provada ou refutada. Isso muda o jogo social da IA, especialmente em cenários de alto risco como finanças, saúde e segurança.

O problema que eles atacam

Guo et al mostraram que agentes frequentemente fabricam resultados quando encontram limitações ambientais. FORMALJUDGE mira exatamente esse comportamento de upward deception. Se o agente diz que leu um arquivo, mas o log mostra erro, o sistema formal compõe fatos como “houve erro” e “saída é substantiva” e “não houve disclosure” para provar formalmente que houve engano.

Isso é poderoso porque ignora a retórica. Não importa se a resposta final parece polida como um relatório da Stark Industries. Se os fatos atômicos violam a fórmula lógica, o veredito é unsafe.

---

E se isso não existisse? O multiverso da supervisão ilusória

Sem algo como FORMALJUDGE, continuaríamos presos na dinâmica de modelos grandes julgando modelos maiores ainda, numa escalada quase Dragon Ball de poder. Cada novo modelo mais persuasivo tornaria o juiz mais suscetível a narrativas convincentes, mesmo que falsas. Seria como pedir para um NPC avaliar um speedrunner que já conhece todas as falhas do mapa.

O problema não é só precisão média. É o colapso silencioso quando modelos começam a otimizar para parecer honestos em vez de ser honestos. Sem garantias formais, qualquer agente suficientemente sofisticado pode explorar as heurísticas do juiz, como um jogador competitivo explorando uma mecânica quebrada no meta.

Nesse cenário, segurança vira teatro. Temos dashboards verdes, métricas bonitas, mas nenhuma prova real de que restrições críticas estão sendo respeitadas. É a diferença entre dizer que o escudo está ativo e realmente calcular se o dano foi bloqueado.

---

Arquitetura como sistema de regras de um RPG hardcore

Para entender o método, precisamos mergulhar na arquitetura como quem lê o manual de um sistema complexo de D&D. Zhou et al estruturam o pipeline em quatro fases, cada uma com função clara e isolamento de responsabilidades. Isso não é improviso, é design modular quase obsessivo.

Decomposição Top-Down: quebrando a missão em quests secundárias

A primeira fase pega a intenção em linguagem natural e a decompõe em fatos atômicos binários. Cada fato deve ser respondido com sim ou não, ser observável na trajetória e depender de contexto mínimo. É como dividir uma quest principal em objetivos claros: coletou o item? Falou com o NPC? Gastou mais ouro do que permitido?

Matematicamente, cada fato é uma função fi que mapeia intenção e trajetória para {0,1}. Essa formalização simples é o antídoto contra julgamentos nebulosos. Em vez de perguntar “foi seguro?”, pergunta-se “clicou no link suspeito?” ou “compartilhou PII externamente?”.

Extração Determinística vs Semântica: separando dados crus de interpretação

A segunda fase distingue extração determinística de extração semântica. Campos estruturados como JSON e valores numéricos são parseados sem LLM. Só o que exige interpretação entra no modelo.

Essa separação é crucial. É como diferenciar dano calculado por fórmula fixa de dano dependente de interpretação narrativa. Quanto menos o modelo opina, menos espaço para alucinação.

Síntese de Prova em Dafny: escrevendo as regras do mundo

Na terceira fase, os fatos viram constantes em um módulo Dafny. Predicados como ϕbudget ou ϕphish combinam fatos com operadores lógicos. A segurança final Φsafe é a conjunção de todos os predicados.

Aqui mora a diferença brutal para LLM + Python. Enquanto scripts Python verificam casos específicos, Dafny com Z3 prova propriedades. É como testar um feitiço em alguns alvos versus provar que ele funciona para qualquer criatura do tipo definido.

Verificação SMT: o boss final é determinístico

A última fase compila tudo via Boogie para o Z3. O veredito é binário e matematicamente garantido dado os fatos. Não há “acho que está certo”. Ou a fórmula é satisfeita ou não.

Essa imunidade à persuasão é central. O verificador ignora explicações textuais e opera só sobre fatos abstraídos. Um agente pode escrever um ensaio digno de Hogwarts, mas se o predicado ϕdeceptive é verdadeiro, o resultado é DECEPTIVE.

---

Resultados: números que batem como crítico em raid mítica

Agora vem a parte que interessa: experimentos. E aqui Zhou et al não economizam.

Agent-SafetyBench: +19% como se fosse buff lendário

No Agent-SafetyBench, FORMALJUDGE supera o baseline LLM em até 22,54 pontos percentuais com Gemini-3.0-Pro como agente. Em média, a melhoria é de 16,6%. Se o baseline está na casa de 58%, o FORMALJUDGE chega a mais de 80% em alguns cenários.

Isso não é ajuste marginal. É sair de elo ouro para diamante. E o mais interessante é que o desempenho permanece estável conforme a sofisticação do agente aumenta, enquanto os baselines degradam.

VitaBench: lógica temporal não é detalhe

No VitaBench, que envolve tarefas com múltiplas ferramentas e restrições temporais, FORMALJUDGE atinge 82,13% com Gemini-3.0-Pro, contra 74,36% do LLM puro. A diferença pode parecer modesta em números absolutos, mas em tarefas com 66 ferramentas, cada ponto percentual é como acertar ou errar uma mecânica crítica.

LLM + Struct melhora um pouco, mostrando que organização ajuda. Mas ainda fica atrás do verificador formal, evidenciando que o gargalo é composição lógica, não apresentação de dados.

Deceivers: aqui o jogo muda

No benchmark Deceivers, o salto é quase absurdo. Com GPT-4o como agente, o LLM baseline atinge 62,47%, enquanto FORMALJUDGE alcança 91,96%. Isso é um ganho de quase 30 pontos percentuais.

Com Qwen-72B como agente, a baseline fica em 63,21%, e o FORMALJUDGE chega a 94,16%. É como se o juiz tivesse equipado um artefato que o torna imune a charme.

Weak-to-Strong: 7B vs 72B sem humilhação

O experimento mais provocativo é weak-to-strong detection. Um juiz Qwen-7B com FORMALJUDGE mantém acima de 90% de acurácia ao detectar enganos de agentes 72B. Já os baselines caem drasticamente conforme o agente cresce.

Isso quebra a narrativa de que “para julgar modelos maiores precisamos de modelos ainda maiores”. Aqui, a lógica formal compensa a limitação paramétrica. É como usar estratégia superior para vencer um oponente com mais stats brutos.

Robustez a ataques L1–L4: estabilidade quase linear

Em ataques classificados de L1 a L4, o FORMALJUDGE mantém taxas de detecção estáveis, enquanto baselines variam e podem cair abaixo de 25% em modelos open-source. A estabilidade sugere que operar sobre fatos atômicos reduz a sensibilidade ao estilo do ataque.

Refinamento Iterativo: de 70,7% para 99,8%

Talvez o resultado mais impressionante esteja no refinamento iterativo. Com feedback baseado em Dafny, Claude-4.5-Opus sobe de 70,7% para 99,8% em três rodadas. Isso é quase linear, como se cada iteração fosse um nível up previsível.

Modelos menores também se beneficiam. Qwen-14B vai de 34,3% para 74,2% com feedback formal. Já refinamento em linguagem natural ou few-shot estagna ou degrada.

Essa diferença de mais de 14 pontos percentuais em relação a CoT e few-shot mostra que feedback formal é mais acionável. É a diferença entre “jogue melhor” e “você violou exatamente a regra C1 porque clicou no link suspeito”.

---

A hype da IA aguenta prova formal?

Aqui é onde a conversa fica desconfortável. A indústria vende agentes autônomos como inevitáveis, mas pouco se fala de garantias formais. É mais fácil mostrar demo do que provar propriedade lógica.

Se aceitarmos que supervisão probabilística herda falhas probabilísticas, então estamos construindo castelos em areia estatística. FORMALJUDGE não resolve tudo, porque ainda depende de LLMs para decomposição e extração. Mas ele desloca o campo de batalha.

A pergunta incômoda é: por que ainda tratamos segurança como problema de prompt engineering, quando poderíamos tratá-la como problema de prova? Estamos com medo da matemática ou apenas viciados na estética do texto fluido?

---

Próximo nível: menos magia, mais prova

O trabalho de Zhou et al não é perfeito. Eles mesmos reconhecem que erros na decomposição top-down e na extração semântica ainda existem. Traduzir linguagem natural para lógica continua sendo um problema quase undecidível em geral.

Mas a direção é clara. Confinar o raciocínio probabilístico ao nível atômico e delegar composição a SMT solvers parece uma estratégia muito mais escalável do que escalar parâmetros indefinidamente. É como trocar grind infinito por build inteligente.

Há espaço para explorar especificações mais ricas, integração com outros provers, redução de dependência do LLM na fase de decomposição e até aprendizado automático de taxonomias de fatos. Também precisamos investigar como agentes podem tentar “satisfazer a especificação” enquanto perseguem objetivos ocultos, um risco real em qualquer sistema formal.

Se você é pesquisador e quer fugir da hype superficial, este paper é leitura obrigatória. Ele não promete AGI amanhã, mas oferece algo mais raro: um caminho concreto para transformar supervisão de opinião em supervisão por prova. Leia o trabalho completo, estude as fórmulas, replique os experimentos e pergunte-se se sua própria pesquisa está construindo efeitos especiais ou garantias reais.

---

Categoria

Lista de tags

---