Yapay zeka alanında biçimsel doğrulamanın kaçınılmaz bir kullanım alanı olduğu yönündeki yaygın tartışmalara rağmen, bu makale biçimsel yöntemlerin "kusursuz" olduğu varsayımının yanlış olduğunu savunuyor. Yıllar boyunca hem iyi hem de kötü biçimsel kod yazmış olan yazarlar, biçimsel kodun da özensiz olabileceğini ve bunun, süper zekayı "iyi" akıl yürütmeyi pekiştirmek için biçimsellik kullanarak başlatmayı uman herkes için ciddi sonuçları olduğunu vurguluyor. Özellikle, yapay zeka güvenliği bağlamında, düşük maliyetli bir sinyalin hatalardan koruyabileceği fikri, biçimsel yöntemlerin doğasına dair yanlış bir anlayışa dayanabilir.
Makale, bir bilgisayar bilimcisinin Lean kullanarak büyük bir matematik problemini çözdüğüne inandığı, ancak kanıtında "kırmızı alt çizgiler" olduğunu fark ettiği bir hikayeyle bu durumu açıklıyor. Kanıt mühendisliğinde, kanıtlardaki hataların programlardaki hatalardan farklı olarak düzeltilmesinin çok daha zor olduğu ve genellikle teoremin kendisinin temelden yanlış olduğu anlamına geldiği belirtiliyor. Geleneksel yazılımdaki değişiklikler genellikle biçimsel spesifikasyonunu etkilerken, kanıt hataları hedefin ulaşılamaz olduğunu gösterebilir. Bu, kanıt hatalarının hem düzeltilmesinin daha zor olduğu hem de hedefin ulaşılamaz olduğunu ima etme olasılığının daha yüksek olduğu anlamına gelir.
Son olarak, biçimsel modellerin "kanıt-idiomatik" olmayabileceği, yani doğru olsalar bile üzerlerinde bir şeyler kanıtlamanın çok zor olabileceği vurgulanıyor. Bir sistemi modellerken veya bir teorem kanıtlayıcıda kod yazarken, kanıtlayıcının sınırlamaları ve yetenekleri hakkında bilgi sahibi olmak ve buna göre uygulama kararları almak gerekir. Örneğin, bir listede bir yönde indüksiyon yapmak kolayken, diğer yönde zor olabilir. Bu durum, biçimsel yöntemlerin uygulanmasında dikkatli olunması gerektiğini ve "kusursuzluk" yanılgısından kaçınılması gerektiğini gösteriyor.
Biçimsel doğrulamanın kusursuz olduğu yanılgısı, yapay zeka güvenliği ve süper zeka geliştirme çabaları için kritik riskler taşıyor.