No mundo silencioso e abstrato da ciência da computação teórica, pesquisadores frequentemente lidam com o problema da equivalência: determinar se duas estruturas diferentes representam, na verdade, a mesma realidade subjacente. Imagine um conjunto de instruções para construir uma máquina. Você poderia escrever as instruções em um parágrafo longo e sinuoso, ou poderia dividi-las em uma lista de tópicos com diagramas. Se ambos os conjuntos de instruções resultarem exatamente na mesma máquina funcionando da exata mesma maneira, eles são equivalentes, mesmo que não se pareçam em nada. Esse conceito é central para um campo chamado raciocínio diagramático, onde processos são desenhados como imagens — caixas conectadas por linhas — em vez de serem escritos como equações. Essas imagens são usadas para modelar sistemas complexos, desde o fluxo de eletricidade até o comportamento de computadores quânticos. No reino da computação quântica, onde as máquinas manipulam informações de maneiras que desafiam a intuição cotidiana, verificar se dois diagramas de circuitos diferentes fazem a mesma coisa é uma verificação de segurança crítica. Se um computador não consegue provar que dois designs são idênticos, ele não pode ser confiado para otimizar ou verificar o hardware que alimentará a tecnologia do futuro.

Uma equipe de pesquisadores da França e da Alemanha introduziu agora um novo conjunto de desafios projetados para testar o quão bem as ferramentas modernas de raciocínio automatizado podem lidar com esse tipo específico de equivalência. O trabalho deles foca em uma família de problemas que chamam de equivalência diagramática, que faz uma pergunta simples: dado dois diagramas de circuito diferentes, eles podem ser transformados um no outro usando um conjunto fixo de regras? Os pesquisadores não apenas fizeram a pergunta; eles construíram uma fábrica para gerar milhares de exemplos únicos e difíceis deste problema. Eles criaram três níveis distintos de dificuldade, variando de uma versão simplificada envolvendo apenas a troca de fios a uma versão complexa que inclui vários tipos de componentes eletrônicos. Para cada nível, eles traduziram os diagramas visuais para uma linguagem que os computadores podem ler, criando um campo de teste rigoroso para os sistemas de prova de teoremas automatizados mais avançados do mundo.

Os pesquisadores começaram definindo as regras do jogo. Em seu sistema, os circuitos são construídos a partir de blocos básicos, ou geradores, que são conectados por fios. Essas conexões podem acontecer de duas maneiras: uma após a outra, como uma corrente, ou lado a lado, como trilhos paralelos. O cerne do problema reside no fato de que o mesmo circuito pode ser desenhado de muitas maneiras diferentes. Assim como uma frase pode ser rearranjada sem mudar seu significado, um diagrama de circuito pode ser torcido, esticado ou reorganizado de acordo com leis matemáticas específicas conhecidas como equações de coerência. O desafio para um computador é olhar para dois diagramas que parecem completamente diferentes e determinar se eles são, de fato, o mesmo objeto sob essas regras. Para tornar isso testável, a equipe criou três variações do problema. A primeira, e mais geral, permite qualquer tipo de componente. A segunda remove todos os componentes, deixando apenas fios que podem ser trocados, transformando efetivamente o problema em uma permutação. A terceira é uma versão simplificada da segunda, usando apenas os blocos de construção mais básicos para criar um quebra-cabeça mais gerenciável, embora ainda difícil.

Para gerar os dados, a equipe escreveu programas de computador que atuam como arquitetos de circuitos. Esses programas começam com uma grade vazia e colocam aleatoriamente componentes e fios. Eles então aplicam uma série de transformações — como torcer um fio ou trocar dois blocos adjacentes — para criar uma segunda versão do circuito que é matematicamente idêntica à primeira, mas que parece diferente. Os programas garantem que os dois diagramas resultantes sejam equivalentes por construção, o que significa que a resposta é sempre "sim", mas o caminho para prová-lo está escondido dentro da complexidade do diagrama. Os pesquisadores geraram milhares desses pares, variando o número de fios de entrada e o tamanho dos diagramas para criar um espectro de dificuldade. Eles então codificaram esses quebra-cabeças visuais em dois formatos padrão usados pela comunidade científica, permitindo que qualquer ferramenta de raciocínio automatizado tente uma solução.

Quando os pesquisadores colocaram esses benchmarks à prova, eles os confrontaram com as principais ferramentas de raciocínio automatizado disponíveis hoje. Eles selecionaram dois sistemas específicos: um que se destaca no tratamento de restrições aritméticas e lógicas, e outro que é uma potência para dedução lógica geral. Os resultados revelaram uma divisão clara de desempenho. O sistema projetado para lidar com restrições aritméticas provou ser significativamente mais capaz, resolvendo a vasta maioria dos quebra-cabeças de dificuldade simples e média. Ele conseguiu verificar a equivalência de circuitos com até vinte fios e centenas de componentes em muitos casos. O sistema de dedução geral, no entanto, teve dificuldades imensas. Ele falhou em resolver quase todos os problemas complexos, ficando travado mesmo em circuitos relativamente pequenos. Os pesquisadores descobriram que a dificuldade do problema era impulsionada por dois fatores principais: o número de fios envolvidos e o número total de conexões no diagrama. À medida que esses números cresciam, a capacidade das ferramentas de encontrar uma solução caía drasticamente.

O estudo destaca um gargalo significativo no campo do raciocínio automatizado. Embora os computadores estejam se tornando cada vez mais poderosos, a combinação específica de raciocínio aritmético e a manipulação de regras estruturais complexas continua sendo um desafio formidável. Os pesquisadores observaram que as ferramentas que tiveram melhor desempenho foram aquelas que podiam entender nativamente as restrições matemáticas que governam os fios, em vez de tentar deduzi-las puramente através de passos lógicos. Isso sugere que, para a equivalência diagramática ser resolvida de forma eficiente, as ferramentas futuras podem precisar integrar o raciocínio aritmético de forma mais profunda em sua lógica central. O trabalho não pretende ter resolvido o problema da verificação de circuitos quânticos, mas forneceu um teste de estresse crucial. Ao oferecer um conjunto padronizado e desafiador de problemas, a equipe deu à comunidade científica uma maneira clara de medir o progresso. Os benchmarks servem como um espelho, refletindo as limitações atuais de nossas ferramentas automatizadas e apontando o caminho para as melhorias específicas necessárias para tornar a verificação de sistemas complexos baseados em diagramas uma realidade confiável.