A matemática 'chata' que poderia salvar a programação por vibe de si mesma
wired ·
Uma nova onda de startups, incluindo &Truth e Harmonic, está aproveitando a IA generativa para automatizar a verificação formal, um rigoroso processo matemático usado para provar a correção do software. Essa abordagem visa tornar o método tradicionalmente trabalhoso prático para uso mais amplo, potencialmente economizando tempo e custos significativos em comparação com os esforços manuais de engenharia. Embora empresas como Apple e Amazon já utilizem a verificação formal para componentes críticos de segurança, sua adoção generalizada ainda é limitada por altos custos, restrições de recursos e preocupações sobre a desaceleração da inovação. Críticos argumentam que a verificação formal não é uma solução mágica e pode criar uma confiança injustificada, observando que testes robustos ainda são necessários para detectar erros do usuário e problemas de hardware. Apesar do ceticismo de alguns especialistas da indústria que veem o processo como difícil e incompleto, defensores acreditam que ele é essencial para proteger sistemas de IA contra ciberataques. A tecnologia está atualmente em estágio de prototipagem, com desenvolvedores experimentando ferramentas assistidas por IA para definir comportamentos de programas e verificar código usando motores matemáticos. À medida que a demanda cresce, a indústria enfrenta questões sobre modelos de precificação, preferências dos clientes e financiamento sustentável para esforços de verificação de código aberto.
wired