Uma pesquisadora da Universidade Stanford desenvolveu uma ferramenta de inteligência artificial capaz de concluir um projeto de engenharia em menos de meio dia por menos de quinhentos dólares, um feito que levou cinco meses para três especialistas altamente qualificados realizarem manualmente. Este resultado impressionante, publicado em um artigo recente, está reacendendo o interesse por um campo obscuro da computação conhecido como verificação formal.
Por décadas, desenvolvedores imaginaram usar matemática para provar que seus programas estão livres de erros. Este processo é longo e laborioso, exigindo que engenheiros escrevam declarações precisas sobre os objetivos de seus softwares e convertam seu código em fórmulas passíveis de validação. Embora empresas já realizem testes sofisticados para identificar falhas, poucas investem em verificação formal, capaz de detectar comportamentos ainda mais erráticos.
Agora, uma onda de startups está apostanho que a inteligência artificial tornará a verificação formal de softwares tanto prática quanto essencial. Entre elas está a &Truth, que a pesquisadora Chuyue Sun ingressou em agosto e que foi lançada publicamente na quinta-feira. A startup levantou setenta milhões de dólares de investidores e pretende verificar qualquer linguagem de programação.
A concorrente Harmonic, cofundada pelo executivo Vlad Tenev, anunciou esta semana que seu agente de inteligência artificial focado em matemática oferece suporte para verificação de softwares escritos em linguagem C e projetos de hardware. A empresa está avaliando a tecnologia com potenciais usuários, incluindo fabricantes de chips.
O grande promessa é um futuro onde softwares funcionam de forma mais confiável com menos problemas de segurança. No entanto, se a inteligência artificial conseguirá levar a verificação formal além dos sistemas mais críticos permanece uma questão em aberto.
A tecnologia ainda está em estágio de prototipagem. Embora a demanda seja alta, ainda não está claro quanto os clientes estão dispostos a pagar. Alguns especialistas alertam que a verificação formal não é uma solução mágica e que pode dar falsa sensação de segurança.
Segundo Vitalik Buterin, engenheiro conhecido por criar a criptomoeda Ethereum, a verificação formal não é uma panaceia. Ainda assim, ele e outros defensores acreditam que será uma defesa importante contra sistemas de inteligência artificial que lançam ataques cibernéticos.
Aeronaves da Boeing, servidores da Amazon e mais de dois bilhões e meio de dispositivos Apple ativos contêm pelo menos algum software verificado formalmente, de acordo com divulgações das empresas. O código em questão é tipicamente relacionado à segurança, e vulnerabilidades nele poderiam causar danos graves se exploradas.
Algumas startups também não têm certeza se devem implementar suas ferramentas diretamente para clientes ou através de intermediários. Seu plano geral é usar inteligência artificial para automatizar grande parte do trabalho envolvido na definição de como um programa deve se comportar. Esforços adicionais de automação traduziriam esse código em um formato que ferramentas matemáticas podem usar para verificar se funciona conforme pretendido.
A Proofcraft, uma das poucas empresas que oferece verificação tradicional há muito tempo, afirma que o crescente entusiasmo pelo processo está se traduzindo em uma avalanche de consultas de potenciais clientes. No entanto, executivos da empresa alertam que especificações geradas por inteligência artificial poderiam inspirar confiança injustificada nos resultados.
Fonte: Feed: All Latest
