Tim jaringan Ethereum telah mempublikasikan seri tulisan tamu dari pengembang utama Vyper dengan nama samaran big_tech_sux, yang membahas peran verifikasi formal di era perkembangan pesat kecerdasan buatan.
Penulis menyatakan bahwa kemajuan LLM membuat pembuktian matematis kebenaran program menjadi lebih mudah diakses, dan untuk smart contract yang mengelola miliaran dolar, verifikasi formal secara bertahap menjadi kebutuhan.
AI Mengubah Pendekatan Pemeriksaan Perangkat Lunak
Dalam seri tulisan tersebut dijelaskan bahwa verifikasi formal adalah metode matematis yang memungkinkan pembuktian kebenaran operasi sebuah program untuk semua skenario eksekusi yang mungkin, bukan hanya yang tercakup dalam pengujian.
Sebagai contoh, penulis memberikan fungsi f(x) = x/2, yang dapat dibuktikan secara matematis bahwa hasilnya tidak akan pernah melebihi nilai input.
Menurutnya, metodologi seperti itu mampu menemukan kesalahan yang sangat langka, yang hampir tidak mungkin terdeteksi melalui pengujian biasa.
"Verifikasi formal dapat mengungkap satu kasus dari kuadriliun, yang tidak akan pernah muncul selama pengujian, tetapi justru itulah yang dapat menyebabkan kegagalan katastrofik," catat penulis.
Sementara itu, dia mengakui bahwa hingga baru-baru ini, penggunaan pendekatan ini memerlukan kerja dari tim ahli yang besar, yang membuat model matematis dari program dan melakukan pembuktian yang rumit.
Menurut pengembang, LLM modern secara signifikan menyederhanakan proses ini seiring dengan mendekatnya AGI.
Namun, penulis menekankan bahwa bahkan dengan bantuan AI, verifikasi formal tetap menjadi proses yang rumit dan memerlukan banyak sumber daya. Secara khusus, transformasi kode program ke dalam model formal dapat mengandung ketidakakuratan yang memengaruhi keandalan hasil.
Perkembangan AI Mengubah Keseimbangan antara Serangan dan Pertahanan
Dalam materi tersebut dicatat bahwa perkembangan kecerdasan buatan secara bersamaan meningkatkan efektivitas baik pihak bertahan maupun pihak penyerang.
Penulis mengingatkan kasus di mana model OpenAI yang belum dirilis berhasil menemukan kerentanan zero-day, yang memungkinkan untuk melewati beberapa lapisan perlindungan.
Dalam konteks ini, verifikasi formal, menurut penulis, memungkinkan untuk menggeser keunggulan ke pihak bertahan.
"Sementara penyerang cukup menemukan satu urutan data input untuk meretas sistem, pihak bertahan dapat menggunakan verifikasi formal untuk membuktikan ketahanannya terhadap semua kemungkinan data input," tegasnya.
Oleh karena itulah, untuk perangkat lunak yang sangat kritis, khususnya smart contract yang mengelola miliaran dolar dana pengguna, verifikasi formal menjadi "bukan pilihan, melainkan prasyarat yang diperlukan".
Perlu dicatat bahwa ini melanjutkan diskusi yang sebelumnya dimulai oleh pendiri bersama Ethereum, Vitalik Buterin, mengenai penggunaan AI untuk verifikasi formal kode.
end-content
