Byron Cook é Distinguished Scientist da AWS e esteve na semana passada em Portugal. Além de liderar a estratégia de Automated Reasoning da AWS, Byron Cook é professor na University College London, fundador do Automated Reasoning Group da Amazon e uma das vozes mais reconhecidas internacionalmente na área da verificação formal e da segurança de sistemas informáticos.
Num contexto em que os agentes de IA prometem executar tarefas cada vez mais complexas de forma autónoma, e à medida que passam a operar em áreas críticas surge uma questão fundamental: como garantir que tomam decisões corretas?
A AWS defende que a próxima fase da inteligência artificial não será definida pela velocidade dos modelos, mas pela capacidade de provar matematicamente que um sistema está a agir dentro das regras definidas. A empresa afirma já processar mais de mil milhões de consultas matemáticas por dia com as suas tecnologias de automated reasoning (raciocínio automatizado) aplicadas à segurança e apresenta o Amazon Bedrock Guardrails como o primeiro sistema capaz de identificar respostas corretas com até 99% de precisão para mitigar alucinações.
Nos últimos dois anos, assistimos a uma explosão na adoção da IA generativa, mas a confiança continua a ser uma grande preocupação para as empresas. Por que razão a confiança continua a ser o maior obstáculo à IA empresarial, mesmo quando a tecnologia se torna mais capaz?
Penso que estamos a atravessar um período verdadeiramente disruptivo, em que novas tecnologias estão a ser introduzidas a um ritmo sem precedentes. Sempre que isso acontece, as pessoas precisam, em primeiro lugar, de compreender do que essas tecnologias são capazes e como podem ser utilizadas de forma eficaz. Naturalmente, as organizações experimentam, aprendem e vão ganhando confiança gradualmente.
Eu vivi o auge da era das “dot-com” e, naquela altura, muitas pessoas não sabiam o que fazer com a Internet nem quais as aplicações que acabariam por ter sucesso. Também demorou algum tempo até que as tecnologias associadas — os elementos que tornaram a Internet segura, fiável e prática — amadurecessem. Penso que o que estamos a observar com a IA segue um padrão muito semelhante.
Se olharmos para tecnologias transformadoras como a máquina a vapor ou a Internet, o processo de adoção foi provavelmente muito semelhante. Por isso, em muitos aspetos, é simplesmente uma questão de tempo.
A minha própria formação é ligeiramente diferente, porque venho do ramo da lógica formal da IA. Se olharmos para as origens da inteligência artificial, o termo foi cunhado em 1957, no Workshop de Dartmouth, por investigadores de várias disciplinas diferentes, incluindo ciência cognitiva, estatística e lógica formal.
Cada vez mais, vejo a minha área como fornecedora das ferramentas de precisão para a IA. Os modelos Transformer são incrivelmente poderosos, mas também podem desviar-se do comportamento pretendido com bastante facilidade. Os métodos formais fornecem as ferramentas de precisão que definem os limites dentro dos quais estes sistemas podem funcionar em segurança. Penso que a IA está a evoluir através da combinação destas tecnologias complementares. São diferentes, mas funcionam em conjunto e, quando combinadas corretamente, é aí que reside o verdadeiro potencial.
“Cada vez mais, vejo a minha área como fornecedora das ferramentas de precisão para a IA”
As alucinações são frequentemente descritas como uma característica inevitável dos grandes modelos de linguagem. Acredita que estas possam vir a ser completamente eliminadas, ou será que o verdadeiro desafio consiste em aprender a detetá-las e a geri-las?
Na verdade, penso que é esta última opção. Aliás, a alucinação é, em muitos aspetos, algo positivo. O que procuramos nos modelos de linguagem é a criatividade. Queremos que nos surpreendam e gerem ideias inovadoras. Se fossem completamente previsíveis e inteiramente determinísticos, haveria poucas razões para utilizar um modelo de linguagem. O seu valor reside precisamente na sua capacidade de explorar soluções criativas.
O verdadeiro desafio é garantir que não ultrapassem certos limites.
Tradicionalmente, temos contado com mecanismos sociotécnicos. Normalmente, podemos observar as ações de alguém e fazer um julgamento razoável sobre se são legais ou ilegais, aceitáveis ou inaceitáveis. Mas se quisermos que a IA funcione em grande escala, essa abordagem já não é suficiente. É aqui que entra o meu trabalho. Se conseguirmos definir formalmente a fronteira entre comportamentos aceitáveis e inaceitáveis — o conjunto infinito de bons comportamentos e o conjunto infinito de maus comportamentos —, então, especialmente em aplicações de IA com autonomia, podemos permitir que o modelo de linguagem seja tão criativo quanto quiser, ao mesmo tempo que filtramos os comportamentos que se situam fora desses limites.
Acho que essa é, de facto, a abordagem ideal. Deixar que o modelo de linguagem continue a ser criativo, enquanto o sistema circundante garante que este respeita as regras que definiste. Por exemplo, não deve transferir dinheiro para o destino errado, fazer investimentos proibidos ou ignorar obrigações legais, como o pagamento de impostos.
Portanto, não, não acho que as “alucinações” devam ser eliminadas. O que precisamos é de uma definição precisa do que é aceitável e do que não é. Assim que tivermos estabelecido esses limites — para a banca, os investimentos ou qualquer outra aplicação crítica —, podemos permitir com segurança que os modelos de linguagem gerem soluções criativas, garantindo ao mesmo tempo que as suas ações se mantêm dentro dos limites permitidos.
“A alucinação é, em muitos aspetos, algo positivo. O que procuramos nos modelos de linguagem é a criatividade. O verdadeiro desafio é garantir que não ultrapassem certos limites”.
A AWS defende que a verificação matemática deve tornar-se uma camada central dos sistemas de IA. Em que medida isto difere dos mecanismos de segurança que a maioria das empresas de IA está atualmente a implementar?
A abordagem que se observa atualmente em grande parte do setor — e a AWS não é, certamente, a única empresa a trabalhar nesta área — consiste, essencialmente, em utilizar um modelo de linguagem para avaliar outro.
Por exemplo, pode utilizar-se um modelo de linguagem para gerar uma estratégia de investimento e, em seguida, pedir a um segundo modelo de linguagem que determine se essa estratégia cumpre os requisitos legais ou regulamentares. O problema é que isto apenas oferece uma garantia probabilística. Pode ficar cada vez mais confiante no resultado, mas nunca pode ter a certeza absoluta. Também não se sabe se os dois modelos de linguagem poderão falhar de formas semelhantes.
Na AWS, temos vindo a investir naquilo a que chamamos de raciocínio automatizado, também conhecido como métodos formais, nos últimos 14 anos. Trata-se de uma área que existe na ciência da computação há muito tempo e que tem sido aplicada com sucesso em muitos contextos, embora não seja amplamente conhecida fora dos círculos especializados.
Hoje, no entanto, tornou-se extremamente relevante.
A principal diferença reside no facto de o raciocínio automatizado poder oferecer uma garantia de 100%, desde que seja possível definir formalmente as propriedades que se pretende preservar. Quer se trate de durabilidade, soberania, privacidade ou disponibilidade, se for possível definir com precisão o que constitui um comportamento aceitável e inaceitável, o raciocínio automatizado pode provar matematicamente que os comportamentos proibidos não podem ocorrer.
“Se for possível definir com precisão o que constitui um comportamento aceitável e inaceitável, o raciocínio automatizado pode provar matematicamente que os comportamentos proibidos não podem ocorrer”.
A AWS afirma que já processa milhares de milhões de consultas de raciocínio matemático todos os dias. Pode partilhar um exemplo?
O raciocínio automatizado permite definir, com precisão matemática, as propriedades que um sistema deve satisfazer. Uma vez especificadas essas propriedades, o raciocínio automatizado pode fornecer uma garantia formal de que o sistema nunca as violará.
Em vez de depender de avaliações probabilísticas ou do julgamento humano, a tecnologia permite que as organizações provem que certas classes de erros ou comportamentos indesejáveis simplesmente não podem ocorrer. Isto é particularmente valioso para aplicações que envolvem privacidade, segurança, durabilidade e outras propriedades críticas do sistema, onde a certeza é muito mais importante do que a confiança estatística.
“A tecnologia permite que as organizações provem que certas classes de erros ou comportamentos indesejáveis simplesmente não podem ocorrer”.
Alguns críticos argumentam que a verificação formal funciona bem para sistemas bem definidos, mas tem dificuldades com a incerteza e a criatividade da IA generativa. Qual é a sua opinião sobre isso?
Acho que é uma observação pertinente. É muito difícil definir algo como o que torna um poema “bom”. A poesia, a música e a escrita existem todas num espectro, e não creio que seja possível provar matematicamente que o artigo que você está a escrever é um bom artigo. Nem sequer saberia como definir isso com precisão.
É claro que se podem desenvolver heurísticas, mas isso é diferente da verificação formal.
Por outro lado, há muitas questões que podem ser definidas com precisão. Por exemplo: esta determinada afirmação sobre a Lei de Licença Médica Familiar nos Estados Unidos é verdadeira? Ou: este trecho de código viola os requisitos de durabilidade de um sistema? Essas são questões precisas e, quando uma questão pode ser definida com precisão, também pode ser respondida com precisão. Se não for possível definir o problema com precisão, então a verificação formal simplesmente não é a técnica adequada. Não se destina a substituir a criatividade ou o julgamento subjetivo. Pelo contrário, foi concebida para proporcionar certeza matemática em situações em que garantias precisas são possíveis e necessárias.
“Se não for possível definir o problema com precisão, então a verificação formal simplesmente não é a técnica adequada”.
Espera-se que os agentes de IA tomem decisões cada vez mais autónomas em áreas como a banca, os cuidados de saúde e os serviços públicos. Será que uma organização poderá alguma vez confiar num agente de IA para agir sem supervisão humana?
Na verdade, penso que isso se está a tornar cada vez mais possível. Consideremos os cuidados de saúde, por exemplo. Quando um ser humano toma decisões sobre quais as informações a divulgar dos seus registos médicos, como é que sabe realmente o que essa pessoa está a fazer? Já reconhecemos o conceito de ameaças internas, em que indivíduos de confiança podem fazer uso indevido de acesso privilegiado.
Em muitas organizações, as regras que definem o que a privacidade realmente significa no contexto dos cuidados de saúde nunca foram formalmente especificadas em lógica matemática. Com o surgimento da IA agénica, um dos maiores desafios — mas também uma das maiores oportunidades — é que as organizações estão agora a ser forçadas a definir essas políticas de forma explícita.
Assim que essas políticas forem formalmente definidas, os agentes de IA poderão operar dentro dos seus limites. Mais importante ainda, passará a dispor de um mecanismo que lhe permite ter a certeza de que o agente não pode violar essas regras, porque fazê-lo é matematicamente impossível.
Isso é muito diferente de confiar num ser humano que pode simplesmente anotar algo, guardá-lo no bolso e sair pela porta fora.
“Assim que essas políticas [que definem a privacidade nos cuidados de saúde] forem formalmente definidas, os agentes de IA poderão operar dentro dos seus limites”.
Está em Portugal. Qual será a mensagem principal que irá partilhar durante as suas palestras e conferências?
Vou dar uma palestra sobre uma investigação matemática bastante obscura, que provavelmente não é especialmente relevante para os vossos leitores [risos].O que penso que será mais interessante para os leitores é que anunciámos recentemente um investimento numa organização de investigação centrada no Lean.
O Lean é simultaneamente uma linguagem de programação e um provador de teoremas para a lógica matemática, e está a tornar-se rapidamente o padrão de referência neste campo.
Ao longo dos anos, surgiram muitas ferramentas semelhantes. No entanto, com o surgimento da IA neurosimbólica e a crescente necessidade de raciocínio simbólico para apoiar uma IA agentiva segura, a procura por estas tecnologias acelerou drasticamente. Tanto a comunidade científica como a comunidade empresarial têm vindo a tentar determinar qual a plataforma com mais probabilidades de se tornar o padrão comum, e parece cada vez mais que o Lean está a assumir esse papel.
Estamos entusiasmados por ver essa convergência a ocorrer e estamos a investir no Lean para ajudar a acelerar o desenvolvimento desse ecossistema.
“Tanto a comunidade científica como a comunidade empresarial têm vindo a tentar determinar qual a plataforma com mais probabilidades de se tornar o padrão comum, e parece cada vez mais que o Lean está a assumir esse papel”.
Se voltarmos a ter esta conversa daqui a cinco ou dez anos, qual acha que será o maior avanço na inteligência artificial?
Vou dar-lhe uma resposta bastante tendenciosa. O desenvolvimento que mais me entusiasma é o surgimento de combinações seguras de agentes.
Imagine que quer criar uma estratégia de investimento, pagar os seus impostos e transferir dinheiro para a sua irmã que vive noutro país. No futuro, provavelmente irá recorrer a diferentes agentes de IA para tratar de cada uma dessas tarefas — um do seu banco, outro das autoridades fiscais, outro de uma plataforma de investimento — e combiná-los num único fluxo de trabalho.
A verdadeira questão é: como é que pode saber, com total certeza, que este conjunto de agentes não fará algo que a pessoa nunca pretendeu?
Em primeiro lugar, vai precisar de uma forma de identificar agentes de confiança. Esses agentes devem ser capazes de descrever, utilizando lógica temporal formal, o que são capazes de fazer, o que são incapazes de fazer, o que nunca farão e o que é garantido que acabarão por fazer.
O próximo desafio é a composição desses agentes. Como combiná-los? Como saber se estão a interagir corretamente? E como ter a certeza de que, uma vez combinados, continuarão a comportar-se exatamente como pretendido?
Já dispomos da tecnologia para responder a essas questões. Acredito que esta seja uma das oportunidades mais empolgantes que temos pela frente, tanto do ponto de vista empresarial como em termos da evolução futura da IA.
