Byron Cook, cientista distinto da Amazon AWS, defende o conceito de “razão automatizada.” O termo “razão” é uma metáfora comum na tecnologia de inteligência artificial (IA) atual, frequentemente usada para descrever as saídas abrangentes geradas por modelos de IA considerados como “razonadores”, como o o1 da OpenAI ou o R1 da DeepSeek AI. No entanto, outro tipo de raciocínio está se consolidando silenciosamente nas aplicações mais avançadas, possivelmente mais próximo do que entendemos por raciocínio real.
Cook argumentou que a “razão automatizada”, também conhecida como “IA simbólica” ou, de maneira mais elaborada, “verificação formal”, representa uma área de estudo que remonta aos primórdios da inteligência artificial. Ele afirmou que essa disciplina está se fundindo rapidamente com a IA generativa para dar origem a uma nova e empolgante hibridação, às vezes chamada de “IA neuro-simbólica”, que combina o melhor da razão automatizada com grandes modelos de linguagem.
Recentemente, Byron Cook apresentou um discurso sobre a razão automatizada no Simpósio de Serviços Financeiros da AWS, realizado em Nova York. Independentemente do termo utilizado, razão automatizada refere-se a algoritmos que buscam declarações ou assertivas sobre o mundo que podem ser verificadas como verdadeiras por meio da lógica. A premissa básica é que todo o conhecimento está rigorosamente fundamentado por aquilo que pode ser logicamente afirmado.
Cook explicou: “A razão pega um modelo e nos permite falar com precisão sobre todos os dados que ele pode gerar.” Ele apresentou um breve trecho de código que ilustra como a razão automatizada consegue essa validação rigorosa. Um loop de instrução em um código de computador pode ser previsto — com certeza — em algum momento da sua execução, baseado nas condições estabelecidas em suas declarações. Dessa forma, a pergunta “Esse loop pode rodar indefinidamente?” pode ser respondida por meio de uma análise lógica.
Utilizando um exemplo, Cook explicou que, com duas variáveis, X e Y, sendo Y um número inteiro positivo e X maior que Y, Y é continuamente subtraído de X, reduzindo seu valor. Eventualmente, ao subtrair Y de X, o valor de X se tornará menor que Y. Nesse momento, as condições do loop foram violadas e, portanto, o loop será encerrado. A simplicidade da afirmação — de que, eventualmente, X será menor que Y — pode ser inferida logicamente sem a necessidade de executar exaustivamente o loop de código em si. Esse é, possivelmente, o aspecto mais importante da razão automatizada, um princípio ao qual Cook se referiu repetidamente: a razão automatizada pode responder perguntas fundamentais de maneira lógica, sem depender de tentativas e erros exaustivas.
“É isso que é IA simbólica,” disse Cook. “Encontramos argumentos, passo a passo, e podemos verificá-los mecanicamente com a base da lógica matemática para assegurar que cada declaração é verdadeira. Em seguida, a razão automatizada é a busca algorítmica por argumentos dessa forma.” Essas soluções passo a passo remontam ao início da IA, nos anos 1950. De fato, em 1959, um dos melhores maquinários da IBM, o 704, executou uma forma de razão automatizada para provar todos os teoremas do famoso Principia Mathematica de Whitehead e Russell.
Cook contou que, desde então, houve muitos avanços na área. “As ferramentas continuam a ficar notavelmente melhores” por meio de novos algoritmos. Segundo ele, a AWS está utilizando a razão automatizada há uma década em tarefas do mundo real, como garantir a entrega dos serviços da AWS conforme os acordos de nível de serviço (SLAs) ou validar a segurança de redes. Traduzir um problema em termos que possam ser avaliados logicamente, como o loop de código, é tudo o que é necessário.
Por exemplo, em segurança de redes, muitas vezes é necessário lidar com declarações que são absolutamente verdadeiras ou absolutamente falsas, explicou Cook, o que significa que podem ser testadas da mesma forma que o loop de código para determinar automaticamente se as condições são atendidas ou não. “Quando observamos as perguntas que os clientes da AWS fazem, eles usam muitas palavras como ‘para todos’, ‘sempre’ e ‘nunca’,”, disse Cook, como por exemplo, “Meus dados estão sempre criptografados em repouso e durante a transmissão?” Essas são declarações universais, que abrangem conjuntos muito grandes, se não infinitos, afirmou ele.
Cook observou que não é possível testar exaustivamente nenhuma política para conhecer tais absolutos. Ele ilustrou dizendo que “o número de vidas do sol que seriam necessárias para testar exaustivamente todos os possíveis pedidos de autorização precisaria de 92.686 dígitos para ser escrito” – em outras palavras, não é prático. Com a razão automatizada, a ferramenta IAM Analyzer da AWS, que está disponível gratuitamente há quatro anos, “pode resolver o mesmo problema em segundos,” disse Cook. “Essa é a proposta de valor da razão e da lógica matemática em comparação com testes exaustivos.”
Cook argumentou que o poder da razão automatizada significa que ela se tornará cada vez mais “uma forma de superinteligência artificial.” Ele explicou: “Durante algum tempo, tivemos uma forma de superinteligência artificial, se é que você quiser, que apenas falava JSON.” A razão automatizada foi utilizada para “resolver conjecturas matemáticas abertas,” que são as coisas que “geram manchetes,” disse ele. “Estamos resolvendo em milissegundos, segundos ou horas, problemas que os humanos não conseguiriam resolver em cem vidas.”
Outros usos na AWS incluem a verificação da correção de códigos de código aberto desenvolvidos pela AWS e até mesmo “provar a correção da porta de entrada da AWS,” significando avaliar se deve permitir ou não pedidos de acesso à AWS que chegam dos clientes com a frequência de dois bilhões de vezes por segundo. Cook mencionou que todas essas aplicações — o AIM Analyzer, a verificação de código, a autorização de acesso da AWS e diversos outros ferramentas e serviços — dependem de uma infraestrutura interna de razão automatizada na AWS chamada Zelkova, que pode traduzir políticas em fórmulas matemáticas.
Cook citou que grande parte do impulso para a razão automatizada e Zelkova veio da indústria de serviços financeiros. Ele mencionou que têm tido parcerias frutíferas com empresas como Goldman e Bridgewater, dizendo que a tecnologia ajudou as equipes desses clientes a “implantar mais rapidamente e, de fato, economizar muito dinheiro.” O futuro da razão automatizada envolve a sua fusão com a IA generativa, uma síntese referida como neuro-simbólica.
De maneira básica, é possível traduzir termos em linguagem natural para fórmulas que podem ser rigorosamente analisadas usando lógica por meio da Zelkova. Assim, a IA generativa pode ser uma forma de um indivíduo não técnico formular seu objetivo em termos informais e em linguagem natural, permitindo que a razão automatizada implemente isso rigorosamente. As duas disciplinas podem ser combinadas para proporcionar a indivíduos que não são lógicos acesso a provas formais, em outras palavras.
Cook forneceu um exemplo prático da abordagem híbrida: a verificação da veracidade de chatbots. “Em um chatbot, você tem perguntas e respostas, e deseja saber se é verdade?” Cook explicou que a razão automatizada permite avaliar declarações de acordo com a lógica formal. Um exemplo disso é uma oferta da AWS, atualmente em prévia, chamada Verificações de Raciocínio Automatizado, que pode pegar a saída em linguagem natural de um chatbot e convertê-la em lógica formal que pode ser verificada.
Cook usou um exemplo em que uma pessoa interage com um chatbot de empréstimo bancário, perguntando quanto tempo deve levar para receber a aprovação de um pedido de empréstimo. O chatbot responde com uma série de declarações, como “1 dia útil para aprovação.” A razão automatizada trabalha para verificar se essas respostas do bot são verdadeiras.
“Nos bastidores, o que estamos fazendo é pegar o texto em linguagem natural, estamos mapeando-o para a lógica matemática, provando ou negando a correção das declarações, e, em seguida, fornecendo testemunhas para que você, como cliente, possa puxar esse log do argumento, confirmando que a propriedade é verdadeira, mas de uma forma que poderia ser auditada,” explicou Cook.
Ele afirmou que a razão automatizada se tornará ainda mais importante na era da IA gerencial. “A direção em que estamos indo é que ouvimos cada vez mais sobre agentes; no gráfico de hype, isso é meio que o novo, novo surgimento,” disse ele. “Se você vai permitir que a linguagem natural seja convertida em ações que fazem decisões de uma única porta em seu nome, com seu dinheiro, sua reputação, sua carreira, seu código, essa correção será absolutamente primordial.”
Cook argumentou que a IA gerencial consiste em muitos sistemas de IA operando em paralelo, e deve ser solucionada da mesma maneira que a razão automatizada tem resolvido outros trabalhos em sistemas distribuídos na AWS. “Por exemplo, no caso do sistema de armazenamento S3 da AWS, a ferramenta interna, Zelkova, foi usada para ‘provar a correção do design dos sistemas distribuídos’,” disse ele.
Cook explicou que o S3 “por baixo dos panos, envolve centenas de protocolos.” Ele afirmou que “se todas as máquinas estiverem falando os protocolos corretamente, você terá uma forte consistência – coletivamente, teremos o resultado correto.” Ele acrescentou que a mesma abordagem de votação em grupo, uma espécie de sabedoria coletiva, pode ser utilizada para verificar as ações dos agentes.
Cook expressou otimismo de que a fusão da razão automatizada com a IA gerativa continue a avançar. “Estou feliz por estar vivo e ser um praticante nesse campo agora,” disse ele. “Porque essas vertentes realmente estão se reunindo muito rapidamente.”
Para aqueles que desejam explorar mais sobre o assunto, uma boa partida é o post introdutório de Cook sobre razão automatizada de 2021.
Referência: [link da matéria]
Posts relacionados:
Bartender virtual pode te auxiliar na preparação de cocktails; entenda como a inteligência artificial atua
Em busca do trabalho ideal? A nova IA do Google pode te auxiliar – e o melhor, é gratuita!
A IA pode auxiliar humanos em missões espaciais no futuro, afirmam pesquisadores.
Modelos mais avançados da OpenAI apresentam mais alucinações do que os anteriores.
