Anthropic Meluncurkan Perpustakaan Verifikasi Formal Skala Besar Claude

Perusahaan kecerdasan buatan Anthropic, melalui Frontier Red Team, merilis penelitian pada 22 Oktober yang menyatakan bahwa model bahasa besar kini dapat secara otomatis menulis bukti formal dalam skala yang lebih besar. Tim bekerja sama dengan Theorem, menggunakan Claude untuk membuktikan sifat keamanan lebih dari 100 perpustakaan open-source nyata di tingkat perakitan RISC-V, menandai pertama kalinya AI digunakan untuk verifikasi formal skala besar pada perangkat lunak produksi di tingkat perakitan. Selama proses penulisan bukti, ditemukan kerentanan yang belum terdeteksi selama bertahun-tahun. Eksperimen ini mengubah pengujian fuzz yang dapat dikompilasi yang sudah ada di Google OSS-Fuzz menjadi spesifikasi, di bawah asumsi biner statis satu utas, anggaran memori tetap, CPU RISC-V, dan Linux, di mana untuk input kurang dari 64 MB, program harus keluar dengan normal dan tidak memicu kesalahan keamanan memori atau kegagalan pernyataan. Setelah memperbaiki masalah, Claude membuktikan sifat di atas untuk 239 titik masuk dari 123 perpustakaan OSS-Fuzz, dengan bukti untuk instruksi RISC-V yang telah dikompilasi, sekitar 180 juta baris Rocq, dan diperiksa oleh kernel Rocq. Halaman tersebut menyatakan bahwa ini tidak berarti bahwa perpustakaan tersebut tidak memiliki kerentanan, masalah yang tersisa mungkin terletak di komponen yang tepercaya atau di luar ruang lingkup bukti. Tim juga meminta Claude untuk memformalkan RFC 1950 dan membuktikan bahwa implementasi zlib dalam kernel Linux sesuai dengan spesifikasi tersebut di tingkat biner x86; menggunakan Rust untuk menulis interpreter yang mencakup sebagian besar subset Python, proporsi program yang dihasilkan secara acak yang konsisten dengan perilaku CPython adalah 99,95%. Dalam 36 tugas verifikasi kecil, Opus 5.5 membuktikan bahwa setengah dari token yang diperlukan sekitar 40% lebih sedikit dibandingkan dengan Opus 5.