Bersama mitranya, Theorem, Anthropic menggunakan model AI Claude untuk membuktikan secara matematis bahwa kode perangkat lunak yang sudah ada berfungsi dengan benar. Sasaran mereka adalah 123 pustaka sumber terbuka yang termasuk dalam proyek keamanan Google, OSS-Fuzz. Dalam hitungan minggu, sekitar 180 juta baris kode pembuktian dihasilkan, dan ratusan bug yang luput dari pengujian konvensional juga ditemukan.
Jarak antara “lulus pengujian” dan “terbukti benar”
Saat berbicara tentang pemeriksaan kualitas perangkat lunak, banyak orang akan teringat pada pengujian. Proses ini dilakukan dengan memberikan masukan yang telah disiapkan dan memeriksa apakah hasil yang diharapkan muncul. Namun, pengujian hanya memeriksa “cakupan yang dicoba”. Pengujian tidak memberi tahu bagaimana program akan berperilaku dalam situasi yang belum dicoba.
Di sinilah verifikasi formal berperan. Perilaku program diperlakukan sebagai persoalan matematika, lalu dibuktikan bahwa program selalu berfungsi dengan benar dalam batas kondisi yang telah ditetapkan. Secara teori, metode ini sangat ampuh, tetapi upaya yang dibutuhkan jauh lebih besar. Verifikasi kernel sistem operasi kecil seL4 saja dilaporkan menghabiskan total 20 tahun-orang oleh tim ahli. Tak heran jika penggunaannya selama ini terbatas pada kasus ekstrem, seperti perangkat lunak kendali pesawat penumpang.
Kali ini, Frontier Red Team Anthropic bekerja sama dengan Theorem dan menyerahkan tugas pembuktian tersebut kepada Claude. Mereka tidak meminta Claude menulis kode baru. Sebaliknya, Claude diminta mengubah pengujian untuk mendeteksi crash pada perangkat lunak yang sudah ada menjadi persoalan matematika, menganalisisnya hingga ke kode mesin setelah kompilasi, lalu menyusun pembuktian dalam jumlah besar.
Program terpisah yang “menilai” pembuktian
Tidak meyakinkan jika AI menyatakan “lulus” atas pembuktian yang ditulisnya sendiri. Mekanisme penilaiannya menjadi hal menarik dalam hal ini. Pembuktian yang dihasilkan diperiksa secara otomatis oleh Rocq, program verifikasi independen. Menurut Anthropic, proses ini hampir tidak memerlukan peninjau manusia.
Tim peneliti menyebutnya sebagai pembuatan pembuktian yang “sepenuhnya otonom”. Namun, perangkat yang digunakan untuk pembuktian serta landasan formalnya dibuat oleh manusia di Theorem. Daripada menganggap AI menciptakan segalanya dari nol, gambaran yang lebih tepat adalah AI menyusun pembuktian dalam jumlah sangat besar sekaligus, di atas landasan yang telah disiapkan manusia.
Ratusan bug ditemukan dalam proses pembuktian
Dalam proses menyusun pembuktian, Claude menemukan ratusan bug dan diizinkan untuk memperbaikinya sendiri. Menurut para peneliti, sebagian besar bug hanya muncul dalam kondisi yang sangat terbatas, seperti berkas masukan yang ukurannya luar biasa besar atau akses memori dalam urutan tertentu. Karena itu, tidak mengherankan jika bug tersebut lolos dari pengujian biasa.
Sejumlah contoh konkret juga disebutkan. Dalam verifikasi pembaca PDF yang banyak digunakan, jumlah bug keamanan yang ditemukan dalam satu minggu sama dengan jumlah bug yang biasanya dilaporkan pada perangkat lunak tersebut selama satu tahun. Pada aplikasi lain, ditemukan pula kesalahan logika yang tidak terdeteksi selama lebih dari 10 tahun.
Hal lain yang tak boleh diabaikan adalah apa yang terjadi jika pembuktian tidak berhasil diselesaikan. Anthropic menjelaskan bahwa bug nyata dapat terungkap di tengah proses, sekalipun pembuktiannya gagal. Jadi, pembuktian bukan sekadar proses untuk memperoleh “sertifikat lulus”, melainkan juga berperan seperti wahana eksplorasi yang menggali bug. Metode ini tampaknya lebih cocok melengkapi pengujian biasa daripada menggantikannya.
Jangan salah menafsirkan cakupan “terverifikasi secara formal”
Meski begitu, berbahaya jika “terverifikasi secara formal” diartikan sebagai “bebas dari segala masalah”. Anthropic sendiri mengakui bahwa pembuktian hanya berlaku dalam batas kondisi yang ketat. Asumsi yang digunakan mencakup konfigurasi prosesor tertentu, program yang berjalan dalam satu thread, serta masukan berukuran kurang dari 64 MB. Pustaka di dunia nyata berjalan di berbagai perangkat keras dan konfigurasi.
Biayanya juga tidak ringan. Dalam beberapa kasus, jumlah token yang digunakan untuk setiap pembuktian dilaporkan mencapai ratusan juta. Biaya keseluruhan proyek tidak diumumkan. Di sisi lain, eksperimen tambahan berskala kecil menunjukkan bahwa pembuktian dapat digunakan kembali, dan model yang lebih baru cenderung semakin efisien. Opus 5.5 dilaporkan membutuhkan sekitar 40% lebih sedikit token daripada Opus 5 untuk menyelesaikan separuh dari pembuktian.
Pertanyaannya bergeser dari “bisakah AI menulis program?”
Jika AI dapat menulis kode dan menjamin kebenarannya dengan syarat tertentu, cara mengajukan pertanyaan pun berubah. Bukan lagi “bisakah AI melakukan pemrograman?”, melainkan “bisakah AI membuktikan keamanan kode yang ditulisnya sendiri?” Bagi tim pengembang yang khawatir terhadap keandalan kode buatan AI, pergeseran ini bukan hal sepele. Jika AI dapat memverifikasi kodenya sendiri, beban peninjauan oleh manusia dapat berkurang. Hal ini berpotensi menekan biaya bukan hanya untuk verifikasi, tetapi juga untuk seluruh proses pengembangan.
Anthropic memperkirakan bahwa dalam waktu dekat, verifikasi formal dengan AI akan menjadi metode yang sama lazimnya dengan pengujian biasa. Peta jalan Theorem mencakup perangkat lunak infrastruktur penting seperti glibc, OpenSSL, dan cURL.
Yang penting di sini bukanlah memahami “isi” pembuktiannya, melainkan “asumsi” yang mendasarinya. Dalam lingkungan seperti apa dan dengan masukan seperti apa pembuktian itu dirancang? Di era ketika pemeriksaan pun diserahkan kepada AI, literasi manusia untuk memeriksa asumsi-asumsi tersebut tampaknya akan menjadi benteng terakhir keselamatan.
コメント