Kesenjangan antara kode yang benar dan program yang terverifikasi

LLM dapat menulis Rust yang dikompilasi dan bahkan lulus cargo test. Apa yang tidak dapat mereka lakukan secara andal adalah menulis pembuktian formal bahwa kode tersebut benar untuk semua kemungkinan masukan.

Masalahnya bukan sintaks Rust. Verifikasi formal mengharuskan Anda menyatakan apa yang ingin dibuktikan, menemukan invarian yang membuat pembuktian berhasil, dan mengekspresikan keduanya dalam bahasa yang diterima verifikator. LLM dilatih pada kode sumber, bukan pada tindakan membuktikan. Mereka melihat teorema, tetapi jarang melihat dua puluh upaya gagal yang mendahului pembuktian yang berhasil.

Jika Anda menempelkan pencarian biner rekursif ke GPT-4 dan memintanya untuk “membuktikan ini benar”, Anda akan mendapatkan sesuatu yang terlihat seperti pembuktian. Itu akan menyebutkan invarian perulangan dan prekondisi. Itu juga mungkin menggunakan sintaks dari Dafny, mereferensikan lemma yang tidak ada, dan menegaskan invarian yang terlalu lemah untuk menetapkan postkondisi. Itu terlihat benar sampai Anda mencoba memeriksanya.

Seperti apa sebenarnya verifikasi formal Rust

Rust memiliki beberapa tool verifikasi. Kani adalah model checker yang mengeksplorasi secara eksaustif semua kemungkinan state suatu fungsi hingga batas tertentu. Prusti dan Creusot adalah verifikator deduktif yang menerjemahkan Rust ke logika dan meminta SMT solver untuk membuktikan properti. Masing-masing memerlukan anotasi dalam sintaks tertentu.

Berikut adalah fungsi sederhana dan seperti apa pembuktian deduktif nyata di Creusot:

// Requires creusot-contracts crate
use creusot_contracts::*;

#[requires(a.len() > 0)]
#[ensures(result == a[0])]
pub fn first<T>(a: &[T]) -> &T {
    &a[0]
}

Creusot memeriksa bahwa prekondisi a.len() > 0 menjamin postkondisi result == a[0]. Ini sepele karena logikanya sederhana. Sekarang kita buat lebih sulit:

use creusot_contracts::*;

#[requires(n <= 1000)]
#[ensures(result == n * (n + 1) / 2)]
pub fn sum_to(n: u32) -> u32 {
    let mut i = 0;
    let mut s = 0;
    #[invariant(i <= n)]
    #[invariant(s == i * (i + 1) / 2)]
    while i < n {
        i += 1;
        s += i;
    }
    s
}

Invarian adalah bagian yang sulit. Manusia menuliskannya dengan memikirkan apa yang tetap benar pada setiap iterasi. LLM mungkin menebak s == i * (i - 1) / 2 karena pola tersebut muncul dalam data pelatihan, atau mungkin menghilangkan invarian sepenuhnya dan membiarkan solver gagal.

Apa yang terjadi ketika Anda meminta pembuktian kepada LLM

Saya menguji ini dengan beberapa model. Promptnya adalah: “Tulis fungsi Rust yang terverifikasi yang menghitung faktorial dari n menggunakan Creusot, dengan prekondisi, postkondisi, dan invarian perulangan yang lengkap.”

Responsnya terbagi dalam tiga kategori.

Pertama, beberapa model menghasilkan anotasi yang terlihat masuk akal tetapi menggunakan sintaks yang salah. Mereka menulis #[precondition(...)] alih-alih #[requires(...)], atau mencampuradukkan sintaks Prusti dengan sintaks Creusot. Kodenya bahkan tidak bisa di-parse.

Kedua, beberapa model menghasilkan anotasi yang sintaksis benar dengan invarian yang terlalu lemah. Fungsi faktorial membutuhkan invarian seperti res == fact(i). Model sering menulis res >= i, yang benar tetapi tidak berguna untuk membuktikan postkondisi. Creusot akan melaporkan bahwa ia tidak dapat menetapkan tujuan, dan LLM tidak memiliki mekanisme untuk memperbaikinya.

Ketiga, beberapa respons mendapatkan invarian dengan benar tetapi menghasilkan lemma bantu yang tidak ada. Mereka mereferensikan fungsi math::fact yang tidak ada dalam library standar Creusot. Pembuktian hanya berfungsi jika Anda membangun definisi logis itu sendiri.

Tidak satu pun dari model yang menghasilkan pembuktian yang lulus pada percobaan pertama.

Di mana LLM sebenarnya membantu dalam alur kerja verifikasi

Ini tidak berarti LLM tidak berguna untuk verifikasi formal. Ini berarti Anda harus menggunakannya untuk tugas yang tepat.

Mereka pandai menghasilkan boilerplate. Diberikan signature fungsi, LLM biasanya dapat menghasilkan klausa #[requires] dan #[ensures] yang menangkap kontrak yang jelas. Untuk fungsi fn divide(a: i32, b: i32) -> i32, ia akan dengan benar menyarankan #[requires(b != 0)] dan #[ensures(result * b == a)]. Ini bukan wawasan mendalam, tetapi menghemat pengetikan.

Mereka cukup baik dalam menjelaskan error verifikator. Jika Creusot melaporkan “cannot prove loop invariant”, menempelkan error ke LLM sering menghasilkan penjelasan berguna tentang apa yang seharusnya dilakukan invarian. Ini tidak akan menyarankan invarian persis yang Anda butuhkan, tetapi akan mempersempit ruang pencarian.

Mereka berguna untuk menerjemahkan antar bahasa verifikasi. Jika Anda memiliki pembuktian Dafny dan ingin mem-port-nya ke Prusti, LLM dapat menangani sebagian besar pemetaan sintaksis. Logika yang mendasarinya sama. Ini adalah jenis tugas pattern-matching yang dikuasai LLM.

Keterbatasan fundamental: pembuktian adalah pencarian, bukan penyelesaian

Menulis pembuktian tidak seperti menulis web server. Ketika Anda menulis web server, ada banyak jawaban yang benar. Ketika Anda menulis pembuktian, ada tepat satu jawaban, atau keluarga kecil jawaban, dan yang lainnya salah.

LLM adalah prediktor token berikutnya. Mereka menghasilkan kelanjutan yang paling mungkin diberikan konteks. Langkah pembuktian bukan kelanjutan yang paling mungkin. Itu adalah langkah yang menutup kewajiban pembuktian, yang mungkin adalah opsi kedua puluh atau kedua ribu yang paling mungkin.

Pertimbangkan membuktikan bahwa fungsi pengurutan mengembalikan permutasi dari masukannya. Wawasan kuncinya biasanya mendefinisikan multiset atau menghitung kemunculan. LLM mungkin menyarankan membandingkan panjang, yang diperlukan tetapi tidak cukup. Dibutuhkan manusia untuk mengenali bahwa kesetaraan panjang tidak menyiratkan permutasi, dan memperkenalkan invarian penghitungan.

Model checking dengan Kani menghindari sebagian dari ini karena tidak memerlukan invarian. LLM dapat menghasilkan harness kani::proof lebih andal karena terlihat seperti unit test. Tetapi Kani hanya berfungsi untuk verifikasi terbatas. Jika Anda membutuhkan pembuktian tak terbatas, Anda masih membutuhkan manusia.

Alur kerja praktis yang menggunakan keduanya

Jika Anda ingin memverifikasi Rust hari ini, berikut adalah alur kerja yang benar-benar berfungsi.

Mulailah dengan menulis kode secara normal. Jalankan cargo test. Kemudian tambahkan kontrak. Gunakan LLM untuk menghasilkan klausa #[requires] dan #[ensures] dari signature fungsi. Tinjau dengan cermat. Model akan mendapatkan yang mudah dengan benar dan yang sulit dengan salah yang halus.

Jalankan verifikator. Ia akan gagal pada setidaknya satu perulangan. Ambil pesan error dan minta LLM untuk menjelaskan invarian apa yang hilang. Gunakan penjelasannya sebagai titik awal, bukan sebagai jawaban. Tulis invarian Anda sendiri.

Iterasi. Verifikator akan memberi tahu Anda apakah invarian Anda cukup kuat. LLM tidak akan. Perlakukan model sebagai programmer pasangan yang mengenal sintaks tetapi belum pernah menyelesaikan pembuktian.

Jawaban jujur atas pertanyaan tersebut

Dapatkah LLM menulis pembuktian formal untuk Rust? Tidak. Belum. Tidak tanpa manusia yang memahami logika.

Mereka dapat menulis kerangka, menjelaskan error, dan menerjemahkan antar tool. Tetapi menemukan invarian, lemma, atau hipotesis induksi yang membuat pembuktian berhasil masih merupakan keterampilan manusia.

Jika Anda mencari tool yang memungkinkan Anda melewati belajar separation logic atau Hoare triples, LLM bukanlah itu. Jika Anda mencari tool yang membuat kurva pembelajaran tidak setajam dengan menangani sintaks dan boilerplate sementara Anda fokus pada logika, LLM layak dicoba.

Mulailah dengan Kani jika Anda ingin pemeriksaan terbatas tanpa invarian. Beralih ke Creusot atau Prusti ketika Anda membutuhkan pembuktian tak terbatas. Gunakan LLM untuk mendapatkan sintaks yang benar, tetapi harapkan untuk menulis pembuktian sendiri.

Pertanyaan yang Sering Diajukan

Apa itu verifikasi formal dalam Rust?

Verifikasi formal menggunakan logika matematika untuk membuktikan bahwa program memenuhi spesifikasi untuk semua kemungkinan masukan. Di Rust, tool seperti Kani, Prusti, dan Creusot menambahkan anotasi ke fungsi yang menjelaskan prekondisi, postkondisi, dan invarian. Verifikator kemudian memeriksa apakah properti ini berlaku.

Bisakah ChatGPT menulis pembuktian untuk Kani?

ChatGPT dapat menulis harness pembuktian Kani, yang terlihat seperti unit test dengan atribut #[kani::proof]. Harness ini lebih mudah dihasilkan daripada pembuktian deduktif karena tidak memerlukan invarian perulangan. Namun, harness kompleks dengan asumsi dan asersi masih membutuhkan tinjauan manusia.

Apa perbedaan antara Kani dan Creusot?

Kani adalah bounded model checker. Ia mengeksplorasi semua jalur eksekusi yang mungkin hingga batas tertentu dan memeriksa panic atau kegagalan asersi. Creusot adalah verifikator deduktif. Ia menerjemahkan Rust ke formula logika dan menggunakan SMT solver untuk membuktikan properti untuk semua masukan, termasuk perulangan tak terbatas, tetapi memerlukan invarian yang diberikan oleh pengguna.

Mengapa LLM kesulitan dengan invarian perulangan?

Invarian perulangan memerlukan penalaran tentang apa yang tetap benar di seluruh iterasi, yang merupakan bentuk penalaran induktif. LLM dilatih untuk memprediksi kelanjutan teks yang mungkin, bukan untuk mencari pernyataan logis tepat yang menutup kewajiban pembuktian. Invarian yang benar seringkali bukan token berikutnya yang paling mungkin.