Cleanroom software engineering menuntut agar Anda membuktikan kode Anda benar sebelum Anda mengompilasinya. Kedengarannya mulia sampai Anda menghabiskan tiga jam menulis loop invariant untuk sebuah fungsi yang mengurutkan sepuluh bilangan bulat.

Hambatan utamanya bukan pembuktiannya. Melainkan boilerplate-nya. Membuat verification conditions, memberi anotasi pada loop dengan invariant, dan memformat assertions untuk Dafny, Why3, atau Z3 itu membosankan, rawan kesalahan, dan sangat tidak menyenangkan. LLM ternyata cukup bagus di bagian ini. Mereka tidak bagus dalam pembuktian yang sebenarnya. Memahami perbedaannya adalah apa yang membuat otomatisasi ini berguna alih-alih berbahaya.

Mengapa Kewajiban Pembuktian Manual Membunuh Kecepatan Pengembangan

Dalam Cleanroom, Anda menulis kode dari spesifikasi Box Structure, lalu membuat verification conditions (VCs) untuk membuktikan bahwa implementasi Anda sesuai dengan spesifikasi. Setiap loop membutuhkan invariant. Setiap fungsi membutuhkan precondition dan postcondition. Setiap data refinement membutuhkan abstraction function.

Bagi tim yang berusaha mengirimkan perangkat lunak, ini adalah pajak. Seorang engineer senior mungkin menghabiskan 40% waktunya untuk anotasi dan penyusunan kerangka VC, dan 60% untuk penalaran logis yang sebenarnya. Penyusunan kerangka tidak memerlukan wawasan yang mendalam. Ia membutuhkan kesabaran dan keakraban dengan sintaks prover Anda.

Itulah jenis tugas pattern-matching yang menjadi kekuatan LLM. Mereka telah melihat ribuan loop invariant, metode Dafny, dan file SMT-LIB. Mereka dapat membuat anotasi yang valid secara sintaksis dan cukup masuk akal untuk dijadikan titik awal.

Apa yang Sebenarnya Dimaksud dengan “Mengotomatisasi Bukti Formal dengan LLM”

Mari kita presisi. Sebuah LLM tidak membuktikan kode Anda benar. Sebuah proof solver seperti Z3, CVC5, atau verifier Dafny membuktikan kode Anda benar. LLM mengotomatisasi tenaga kerja manusia yang berada di antara pseudocode Anda dan solver.

Alur kerjanya terlihat seperti ini:

  1. Anda menulis implementasi dan spesifikasinya.
  2. LLM membuat anotasi kandidat: invariant, precondition, postcondition, variabel ghost.
  3. Anda memasukkan kode yang dianotasi ke dalam verifier.
  4. Verifier menerima bukti, menolaknya dengan counterexample, atau time out.
  5. Jika bukti gagal, Anda memeriksa kegagalannya dan meminta LLM untuk menyempurnakan anotasinya.

LLM adalah seorang magang yang sangat cepat dan sangat percaya diri yang mengetahui sintaks setiap alat verifikasi di internet. Ia dengan senang hati akan menghasilkan halusinasi invariant yang terlihat sempurna dan langsung gagal. Tidak apa-apa. Solver menangkap halusinasinya. Nilainya terletak pada menghindari masalah halaman kosong.

Bagaimana LLM Membuat Anotasi yang Dapat Diperiksa Solver

Triknya ada pada prompt. Anda tidak meminta LLM untuk “membuktikan fungsi ini benar.” Anda memintanya untuk membuat artefak tertentu dalam format tertentu.

Misalnya, jika Anda memiliki fungsi mirip Python yang menghitung jumlah sebuah array, Anda memberi prompt LLM seperti ini:

Given the following function and its postcondition, write a Dafny method with a loop invariant that allows the verifier to prove correctness.

Function: sum(arr) returns the sum of all elements in arr.
Postcondition: result == sum(i in 0..|arr|) arr[i]

LLM mengembalikan kode Dafny dengan loop invariant seperti forall k :: 0 <= k < i ==> arr[k] is accounted for in result. Ia mungkin tidak mendapatkan sintaks yang tepat pada percobaan pertama. Tapi ia mendapatkan strukturnya dengan benar, dan itu menghemat waktu Anda sepuluh menit untuk mengetik.

Untuk kontrol lebih lanjut, Anda dapat meminta SMT-LIB secara langsung. Ini berguna ketika Anda sedang membangun pipeline verifikasi kustom alih-alih menggunakan bahasa tingkat tinggi seperti Dafny.

Contoh yang Dapat Dijalankan: Mengotomatisasi Loop Invariant dengan Python dan Z3

Berikut adalah contoh lengkap yang dapat dijalankan. Kita menggunakan Python untuk meminta LLM (API OpenAI) membuat loop invariant untuk fungsi penjumlahan array sederhana, lalu memverifikasinya dengan Z3.

Pertama, instal dependensinya:

pip install z3-solver openai

Lalu jalankan skripnya:

import openai
from z3 import *

code = """
def sum_array(arr):
    s = 0
    i = 0
    n = len(arr)
    while i < n:
        s = s + arr[i]
        i = i + 1
    return s
"""

prompt = f"""You are a formal verification assistant.

Given this Python function that sums an array:
{code}

The postcondition is: result == Sum(arr[j] for j in range(len(arr)))

Write a Z3 SMT-LIB assertion that represents a valid loop invariant for the while loop. The invariant should mention i, s, n, and arr. Use Python Z3 syntax (ForAll, Implies, And, etc.). Return ONLY the Python code for the invariant, no explanation."""

client = openai.OpenAI()
response = client.chat.completions.create(
    model="gpt-4o",
    messages=[{"role": "user", "content": prompt}],
    temperature=0.2,
)

invariant_code = response.choices[0].message.content.strip()
print("Generated invariant:")
print(invariant_code)

# Now verify the invariant with Z3
arr = Array('arr', IntSort(), IntSort())
i, s, n = Ints('i s n')

# We manually parse the LLM's output. In production you'd use an AST parser.
# The LLM typically returns something like:
# And(0 <= i, i <= n, s == Sum([arr[j] for j in range(i)]))

# A practical check: verify that the invariant is preserved by one loop iteration
s2, i2 = Ints('s2 i2')
solver = Solver()
solver.add(n == 3)
solver.add(arr[0] == 1, arr[1] == 2, arr[2] == 3)
solver.add(i2 == 1, s2 == 1)  # assume invariant holds mid-loop

# Execute one iteration
s_next = s2 + Select(arr, i2)
i_next = i2 + 1

# Check that invariant holds after iteration
solver.add(Not(And(i_next >= 0, i_next <= n)))

if solver.check() == unsat:
    print("Invariant preserved for this concrete case.")
else:
    print("Invariant FAILED for this concrete case.")
    print(solver.model())

Skrip ini tidak akan memverifikasi fungsi dalam sekali jalan. Itulah intinya. LLM memberi Anda invariant kandidat. Z3 memberi tahu Anda apakah invariant itu berlaku. Anda mengulangi.

Dalam praktiknya, tim yang membangun pipeline verifikasi berbantuan LLM membungkus loop ini dalam skrip yang mengirimkan VC yang gagal kembali ke LLM, mengurai anotasi baru, menjalankan verifier, dan mengirimkan kembali pesan kesalahan apa pun sebagai prompt penyempurnaan.

Ini bukan verifikasi yang sepenuhnya otonom. Ini adalah verifikasi dengan manusia-di-dalam-loop yang dibantu oleh asisten pengetik yang sangat cepat.

Di Mana Ini Gagal: Halusinasi vs. Kesalahan yang Sebenarnya

LLM akan membuat invariant yang terlalu lemah. Ia akan lupa menyebutkan variabel yang dibutuhkan solver. Ia akan membuat sintaks Dafny dari tahun 2019 yang tidak lagi bisa dikompilasi. Ia dengan percaya diri akan mengatakan bahwa i <= n sudah cukup padahal loop sebenarnya membutuhkan i < n && s == partial_sum(arr, i).

Tidak satu pun dari ini yang fatal. Solver menolaknya. Anda membaca kesalahannya, Anda meminta lagi.

Bahaya yang sebenarnya adalah sebaliknya. Ketika LLM membuat invariant yang terlalu kuat, solver mungkin membuktikan program benar terhadap spesifikasi yang lebih ketat dari yang Anda maksudkan. Anda mengira Anda telah membuktikan bahwa sum_array berfungsi untuk semua array. Padahal Anda sebenarnya membuktikannya hanya berfungsi untuk array yang semua elemennya positif, karena LLM menambahkan konjungsi ekstra yang terlihat masuk akal.

Selalu tinjau spesifikasi yang dihasilkan. LLM menulis boilerplate. Anda memiliki logikanya.

Kapan Memercayai Mesin, dan Kapan Membuat dengan Tangan

Gunakan otomatisasi LLM untuk:

  • Penyusunan kerangka VC untuk fungsi sederhana dengan precondition dan postcondition yang jelas.
  • Terjemahan sintaks antar bahasa bukti. Mengkonversi spesifikasi Dafny ke Why3 atau SMT-LIB bersifat mekanis dan rawan kesalahan. LLM sangat bagus dalam hal ini.
  • Pembuatan variabel ghost untuk bukti data refinement. Polanya berulang.

Jangan gunakan otomatisasi LLM untuk:

  • Bukti yang kritis untuk keamanan di mana bug spesifikasi yang halus lebih buruk daripada tidak ada bukti sama sekali.
  • Logika temporal yang kompleks atau properti liveness. Data pelatihan LLM lebih tipis di sini, dan halusinasi lebih mungkin lolos.
  • Algoritma baru yang tidak menyerupai apa pun dalam corpus pelatihan. Jika Anda menemukan protokol konsensus baru, LLM tidak tahu invariant apa yang dibutuhkannya.

Pertanyaan yang Sering Diajukan

Apa yang dimaksud dengan verification condition dalam rekayasa Cleanroom?

Verification condition adalah formula logis yang dibuat dari kode dan spesifikasinya. Jika formula tersebut valid, kode Anda mengimplementasikan spesifikasi dengan benar. Dalam Cleanroom, ini biasanya dibuat sebelum kompilasi dan dilunasi menggunakan proof assistant atau solver otomatis.

Bisakah LLM menggantikan proof assistant seperti Coq atau Isabelle?

Tidak. LLM membuat kode dan anotasi yang dapat diperiksa oleh proof assistant. Mereka tidak melakukan langkah bukti yang sebenarnya. Proof assistant tetap menjadi otoritas apakah sebuah bukti valid.

Apa LLM terbaik untuk membuat anotasi verifikasi formal?

GPT-4o dan Claude 3.5 Sonnet keduanya berkinerja baik pada sintaks Dafny dan SMT-LIB. Model yang lebih kecil sering kesulitan dengan sintaks yang tepat yang dibutuhkan oleh proof solver. Atur temperature rendah (0,1-0,2) untuk mengurangi halusinasi kreatif.

Bagaimana cara mencegah LLM membuat spesifikasi yang salah?

Anda tidak bisa. Anda memperlakukan output LLM sebagai draf. Selalu jalankan anotasi yang dihasilkan melalui verifier Anda. Selalu baca precondition dan postcondition yang dihasilkan untuk memastikan cocok dengan maksud Anda. Jangan pernah menganggap verifikasi yang berhasil berarti spesifikasinya benar.

Mulai dari Bagian yang Membosankan

Jika tim Anda sedang melakukan Cleanroom atau pekerjaan correctness-by-construction apa pun, otomatisasi bernilai tertinggi bukanlah pembukti teorema AI yang canggih. Ini adalah skrip yang membuat loop invariant Anda dan memformat SMT-LIB Anda sehingga Anda tidak perlu melakukannya.

Pilih lima pola anotasi yang paling membosankan dalam codebase Anda. Tulis template prompt untuk masing-masing. Jalankan melalui LLM, verifikasi outputnya, dan commit yang lolos. Itu saja. Anda baru saja mengembalikan 40% waktu verifikasi Anda untuk biaya satu panggilan API.

Bukti yang sulit tetap milik Anda. Tapi setidaknya Anda tidak akan mengetiknya dari awal.