Sistema de IA acerta 100% em sistemas distribuídos via verificação formal

Um novo sistema de inteligência artificial atingiu um marco na geração de implementações de sistemas distribuídos com verificação formal completa, alcançando 100% de acerto em um conjunto de sete especificações desafiadoras. Os melhores agentes de codificação disponíveis atualmente, como o Codex e o Claude Code, haviam conseguido resolver apenas duas das mesmas sete tarefas.

A descoberta foi detalhada em um artigo científico submetido ao repositório arXiv em maio, representando um salto significativo na capacidade de sistemas de IA produzirem software com garantias matemáticas de correção. O método, chamado de Inductive Deductive Synthesis (IDS), combina a síntese conjunta e incremental de implementação e prova formal, aprendendo com tentativas fracassadas para explorar estratégias promissoras de maneira sistemática.

Sistemas distribuídos são notoriamente difíceis de projetar porque propriedades essenciais, como a consistência entre leituras e escritas, precisam valer sob qualquer possível entrelaçamento de eventos, e não apenas nos casos testados. Enquanto a verificação formal mecanizada pode garantir essa correção, o processo tradicional demanda meses ou até anos de trabalho de especialistas altamente qualificados.

O IDS resolveu as sete especificações em cerca de 6,8 horas e ao custo médio de 106 dólares por especificação, aproximadamente 200 vezes mais rápido do que o esforço humano especializado, segundo os autores, e 17% mais barato do que os melhores agentes de IA disponíveis no mercado. Além da correção formal, o sistema incorpora retroalimentação de desempenho no mesmo ciclo de síntese, produzindo implementações que chegam a ser três vezes mais rápidas do que sistemas verificados publicados anteriormente.

A abordagem representa um avanço concreto rumo a sistemas de IA capazes de construir infraestrutura computacional com garantias matemáticas de correção em relação à especificação formal, algo especialmente relevante para aplicações críticas como serviços financeiros, controle de tráfego aéreo e redes de energia. O trabalho também demonstra que combinar raciocínio indutivo com dedução formal pode destravar patamares de confiabilidade que escapavam tanto a programadores humanos quanto aos sistemas de IA disponíveis até agora.