Provas matemáticas e verificação formal podem ajudar a garantir a segurança e a controlabilidade de sistemas avançados de IA?

Em seu novo artigo, Max Tegmark e Steve Omohundro descrevem uma maneira possível de garantir o desenvolvimento seguro de inteligência artificial avançada, incluindo inteligência artificial geral (AGI).

Tegmark é físico, cosmólogo e pesquisador de IA e, como presidente do Future of Life Institute, foi um dos iniciadores da carta aberta que, em março, pedia uma pausa de pelo menos seis meses no desenvolvimento da IA. Omohundro também é físico e pesquisador de IA, além de fundador e CEO da Beneficial AI Research, uma startup que visa desenvolver IA útil e segura.

A ideia central do artigo é projetar sistemas de IA para que os comportamentos críticos sejam comprovadamente compatíveis com especificações matemáticas formais que codificam valores e preferências humanas. Isso forçaria os sistemas de IA a executar apenas as ações que são matematicamente comprovadas, seguras e benéficas para os seres humanos – porque a cada passo eles teriam que fornecer uma prova matemática de segurança que poderia ser verificada antes de permitir uma ação.

Os autores argumentam que as abordagens atuais que se concentram no alinhamento dos objetivos da IA com os valores humanos não fornecem, por si só, proteção contra o uso indevido da IA. Em vez disso, dizem eles, é necessária uma mentalidade de segurança que construa segurança “tanto nos AGIs quanto na infraestrutura física, digital e social com a qual eles interagem”.

Verificação de software e hardware como rede de segurança

A proposta tem várias componentes:

  • Sistema comprovadamente compatível (PCS): Sistema comprovadamente que atende a certas especificações formais.,
  • Hardware comprovadamente compatível (PCH): Hardware comprovadamente atendendo a certas especificações formais.
  • Código de Prova (PCC): Software que sob demanda produz provas de que atende a certas especificações formais.
  • Contrato demonstrável (PC): hardware seguro que controla a ação verificando a conformidade com a especificação formal.
  • Meta-contrato demonstrável (PMC): Hardware seguro que controla a criação e atualização de outros contratos demonstráveis.

Juntos, eles impossibilitariam que os sistemas de IA violassem as principais propriedades de segurança. As provas garantiriam conformidade até mesmo para IA superinteligente, dizem os pesquisadores. Em vez de modelos individuais de IA que, esperançosamente, atendam aos nossos requisitos, o método se baseia em uma rede de segurança sequencial na qual as provas devem ser fornecidas em cada etapa.

Os riscos existenciais devem ser interrompidos a cada passo

Os autores usam um cenário específico de bioterrorismo de um artigo de pesquisa sobre as quatro categorias de riscos catastróficos de IA para ilustrar como sua abordagem pode ser aplicada:

Um grupo terrorista quer usar IA para liberar um vírus mortal sobre uma área densamente povoada. Ele usa IA para projetar o DNA e a casca de um patógeno, bem como as etapas para produzi-lo. Ele contrata um laboratório químico para sintetizar o DNA e incorporá-lo à casca da proteína. Ele usa drones controlados por IA para espalhar o vírus e IA nas redes sociais para espalhar sua mensagem após o ataque.

Com a abordagem proposta para sistemas comprovadamente seguros, tal ataque poderia ser evitado em todos os estágios: IAs de design bioquímico não sintetizariam projetos perigosos, GPUs não executariam programas de IA inseguros, fábricas de chips não venderiam GPUs sem verificação de segurança, máquinas de síntese de DNA não operariam sem verificação de segurança, sistemas de controle de drones não permitiriam voos de drones sem verificação de segurança, e os bots sociais não manipulariam a mídia.

Pesquisadores veem obstáculos técnicos, mas esperam progresso

Os autores reconhecem que, para realizar plenamente essa visão, obstáculos técnicos significativos devem ser superados. O aprendizado de máquina provavelmente seria necessário para automatizar a descoberta de algoritmos compatíveis e as provas correspondentes. Avanços recentes no aprendizado de máquina para a prova automatizada de teoremas dão motivos para otimismo sobre o rápido progresso, dizem os pesquisadores.

Mas, mesmo além de considerações como como especificar formalmente “não deixe a humanidade ser extinta”, ainda há uma série de desafios não resolvidos, mas simples e muito bem especificados, cuja solução já traria grandes benefícios para a segurança cibernética, blockchain, privacidade e infraestrutura crítica no médio prazo, disseram eles.