- Verifikasi formal (formal verification) adalah metode untuk membuktikan secara matematis bahwa kode selalu memenuhi spesifikasi, dan selama ini lama bertahan di ranah yang terbatas serta berpusat pada riset
- Beberapa sistem besar seperti mikrokernel seL4 telah dikembangkan dengan verifikasi formal, tetapi karena tingkat kesulitan dan biaya yang tinggi, metode ini hampir tidak digunakan di lingkungan industri
- Baru-baru ini, alat bantu coding berbasis LLM menunjukkan hasil tidak hanya pada kode implementasi tetapi juga dalam penulisan skrip pembuktian di berbagai bahasa, sehingga muncul kemungkinan untuk mengubah struktur biaya verifikasi secara besar-besaran
- Jika AI dapat mengotomatisasi pembuktian kebenaran sekaligus pembuatan kode, pengembangan perangkat lunak dapat beralih ke pendekatan yang lebih dapat dipercaya daripada code review manusia
- Otomatisasi verifikasi formal adalah teknologi kunci untuk memastikan keandalan perangkat lunak di era AI, dan hambatan utama untuk menjadi arus utama tampaknya lebih berupa perubahan budaya daripada keterbatasan teknis
Kondisi Saat Ini dan Batasan Verifikasi Formal
- Bahasa dan alat berorientasi pembuktian seperti Rocq, Isabelle, Lean, F*, Agda memungkinkan pembuktian matematis bahwa kode memenuhi spesifikasi
- Contoh representatifnya meliputi kernel sistem operasi seL4, kompiler C CompCert, dan stack protokol kriptografi Project Everest
- Namun, di lingkungan industri verifikasi formal hampir tidak digunakan
- Dalam kasus seL4, memverifikasi 8.700 baris kode C memerlukan 20 person-year dan 200.000 baris kode Isabelle
- Untuk setiap satu baris implementasi, dibutuhkan 23 baris pembuktian dan setengah hari kerja manusia
- Secara global, jumlah ahli yang mampu menulis pembuktian semacam ini diperkirakan hanya ratusan orang
- Dari sisi ekonomi juga, pada sebagian besar sistem biaya verifikasi lebih besar daripada kerugian akibat bug, sehingga nilai praktisnya rendah
Bagaimana AI Mengubah Ekonomi Verifikasi Formal
- Baru-baru ini, asisten coding berbasis LLM menunjukkan hasil bukan hanya pada kode implementasi tetapi juga pada penulisan skrip pembuktian
- Nature, Galois, arXiv, dan lainnya melaporkan kasus LLM yang menghasilkan pembuktian dalam berbagai bahasa
- Saat ini masih diperlukan bimbingan ahli, tetapi otomatisasi penuh diperkirakan mungkin terjadi dalam beberapa tahun ke depan
- Jika biaya verifikasi turun drastis, verifikasi formal dapat diterapkan pada lebih banyak perangkat lunak
- Pada saat yang sama, kode yang dihasilkan AI memerlukan verifikasi formal untuk menjamin keandalan sebagai pengganti peninjauan manusia
- Jika AI dapat membuktikan sendiri kebenaran kodenya, pendekatan ini berpotensi lebih disukai daripada kode yang ditulis manual
Saling Melengkapi antara LLM dan Verifikasi Pembuktian
- Saat LLM menulis skrip pembuktian, walaupun menghasilkan isi palsu (halusinasi), proof checker akan menolaknya
- Checker disusun dari basis kode kecil yang telah diverifikasi, sehingga sulit bagi pembuktian yang salah untuk lolos
- Karena itu, ketidakpastian LLM dapat dilengkapi oleh ketelitian verifikasi formal
- Kombinasi ini berfungsi sebagai jalur otomatisasi yang aman untuk menjamin keandalan kode yang dihasilkan AI
Tantangan Baru: Ketepatan dalam Mendefinisikan Spesifikasi
- Bahkan dalam lingkungan verifikasi otomatis, mendefinisikan spesifikasi (specification) dengan benar tetap menjadi tantangan utama
- Perlu dipastikan bahwa properti yang dibuktikan benar-benar sesuai dengan properti yang dimaksud pengembang
- Penulisan spesifikasi tetap memerlukan keahlian dan pemikiran yang cermat, tetapi jauh lebih sederhana dan cepat daripada pembuktian manual
- AI juga dapat mendukung penerjemahan spesifikasi antara bahasa alami dan bahasa formal
- Namun, ada risiko kehilangan makna, meski ini dinilai masih berada pada tingkat yang dapat dikelola
Prospek Perubahan dalam Cara Pengembangan Perangkat Lunak
- Pengembang dapat beralih ke bentuk kerja di mana properti kode yang diinginkan dituliskan sebagai spesifikasi deklaratif, lalu AI menghasilkan implementasi dan pembuktian sekaligus
- Dalam skenario ini, pengembang tidak perlu meninjau langsung kode yang dihasilkan AI, dan dapat menggunakannya berdasarkan kepercayaan seperti pada bahasa mesin dari compiler
- Singkatnya, tiga perubahan berikut diperkirakan akan terjadi
- Penurunan tajam biaya verifikasi formal
- Peningkatan kebutuhan verifikasi untuk memastikan keandalan kode buatan AI
- Ketelitian verifikasi formal melengkapi sifat probabilistik LLM
- Jika faktor-faktor ini berpadu, verifikasi formal kemungkinan besar akan menjadi teknologi arus utama dalam rekayasa perangkat lunak
- Ke depan, faktor pembatasnya diperkirakan bukan teknologi, melainkan kecepatan penerimaan perubahan budaya pengembangan
Belum ada komentar.