Anthropic: Claude telah mengesahkan secara formal perpustakaan sumber terbuka dalam skala besar

Pada 22 Oktober, Frontier Red Team milik syarikat kecerdasan buatan Anthropic menerbitkan satu kajian yang menunjukkan bahawa model bahasa besar kini mempunyai keupayaan untuk menjana bukti formal secara automatik dalam skala yang lebih luas. Pasukan ini bekerjasama dengan Theorem untuk menjalankan pengesahan formal terhadap sifat keselamatan lebih daripada 100 pustaka sumber terbuka sebenar pada tahap susunan RISC-V berdasarkan model Claude—ini merupakan kali pertama sistem AI melaksanakan pengesahan formal berskala besar terhadap perisian tahap pengeluaran pada tahap susunan. Semasa proses pembinaan bukti, pasukan itu juga secara tidak sengaja mendedahkan beberapa kerentanan keselamatan yang telah lama tidak dikesan. Kaedah eksperimen melibatkan penukaran kes ujian fuzz yang boleh dikompilasi—yang sudah sedia ada dalam Google OSS-Fuzz—kepada spesifikasi formal, dan kemudian mengesahkan input berukuran sehingga 64 MB dalam keadaan terhad seperti: binari statik satu benang, bajet ingatan tetap, arsitektur CPU RISC-V, serta persekitaran operasi Linux.