Editorial Ilmu Komputer & AI
Schwarz: Verifikasi Program Agentik yang Sadar Solver
Masalah inti
Sistem verifikasi agentik sering kali dapat menghasilkan spesifikasi tingkat sumber yang tampak masuk akal, tetapi masuk akal saja tidak cukup: verifier tetap harus mengubah spesifikasi tersebut menjadi obligasi SMT yang dapat dibuktikan oleh solver. Ketika langkah ini gagal, loop yang digerakkan LLM saat ini biasanya hanya mengekspos kesalahan verifier yang kasar, timeout, atau hasil solver unknown. Model tidak dapat mengetahui apakah spesifikasinya salah, ada lemma pembantu yang hilang, konteks bukti memuat fakta yang tidak relevan, atau obligasinya memerlukan pandangan teori yang berbeda.
Makalah ini memperkenalkan **Schwarz**, sebuah harness verifikasi agentik yang membuat kegagalan bukti berbasis SMT menjadi lokal, dapat diperiksa, dan dapat diperbaiki. Schwarz mengubah verifikasi yang gagal menjadi tugas perbaikan yang terlokalisasi pada obligasi: snapshot titik program mengekspos fakta yang diperiksa pada suatu batas, lemma lokal memungkinkan agen mengusulkan langkah bukti yang hilang, dan kebijakan solver yang sadar teori memandu agen menuju formulasi yang ramah solver untuk obligasi numerik, terkuantifikasi, memori, dan floating-point. Penulis mengimplementasikan Schwarz
Inovasi
Schwarz dievaluasi pada 1.475 tugas. Hasilnya dilaporkan dalam dua kelompok utama.
Pertama, pada 475 benchmark dari alat verifikasi agentik terkini, Schwarz menyelesaikan **95,2%** tugas. Kelompok ini dapat dibandingkan secara langsung dengan sistem verifikasi agentik sebelumnya, sehingga hasilnya menunjukkan bahwa perbaikan yang sadar solver secara substansial meningkatkan tingkat keberhasilan pada tugas yang memang menyasar verifikasi yang digerakkan LLM.
Kedua, pada 1.000 tugas dari track SV-COMP 2026 ReachSafety, Schwarz menyelesaikan **91,5%** tugas. Tugas-tugas ini rata-rata **1.427 LOC**, sehingga menjadi uji skalabilitas, bukan latihan benchmark kecil. Baseline pembandingnya adalah **CPAchecker**, yang menyelesaikan **60,1%** tugas yang sama. Selisih 31,4 poin persentase adalah hasil empiris utamanya: harness agentik yang sadar solver dapat mengungguli verifier mapan non-agentik pada track benchmark verifikasi standar.
Makalah ini juga melaporkan ablasi dan perbandingan dengan baseline agen murni. Keduanya menunjukkan bahwa perbaikan yang sadar solver efektif dan skalabel. Dengan kata lain, keuntungannya bukan sekadar dari penggunaan agen LLM; keuntungan itu berasal dari
Mengapa penting
Wawasan utama Schwarz adalah bahwa hambatan dalam verifikasi agentik bukan hanya pembuatan spesifikasi, melainkan *penerjemahan* spesifikasi menjadi obligasi SMT yang benar-benar dapat dibuktikan oleh solver. Ketika penerjemahan itu gagal, kesalahan verifier yang kasar hampir tidak memberi sinyal apa pun kepada LLM. Model tidak dapat membedakan beberapa akar penyebab yang sangat berbeda: spesifikasi yang salah, lemma pembantu yang hilang, fakta yang tidak relevan dalam konteks bukti, atau obligasi yang memerlukan pandangan teori berbeda. Schwarz mengatasi ini dengan membuat kegagalan menjadi lokal, dapat diperiksa, dan dapat diperbaiki.
Ketiga mekanisme tersebut memetakan langsung ke akar penyebab itu. Snapshot titik program mengatasi masalah konteks bukti dengan mengekspos fakta yang diperiksa pada suatu batas. Lemma lokal mengatasi masalah langkah bukti yang hilang dengan memungkinkan agen mengusulkan fakta perantara yang terbatas cakupannya. Kebijakan solver yang sadar teori mengatasi masalah formulasi dengan memandu agen menuju encoding yang ramah solver untuk obligasi numerik, terkuantifikasi, memori, dan floating-point. Dekomposisi inilah yang mengubah hasil `unknown` yang opak menjadi tugas perbaikan yang dapat ditindaklanjuti.
Hasil empiris mendukung desain tersebut. Tingkat penyelesaian 95,2% pada 475 benchmark verifikasi agentik menunjukkan bahwa pendekatan ini berhasil pada tugas yang sudah dirancang untuk verifikasi yang digerakkan LLM. Tingkat penyelesaian 91,5% pada 1.000 tugas SV-COMP 2026 ReachSafety, dengan rata-rata 1.427 LOC, menunjukkan bahwa pendekatan ini berskala di luar contoh kecil. Perbandingan dengan CPAchecker pada 60,1% sangat penting karena CPAchecker adalah verifier mapan non-agentik; hasilnya menunjukkan bahwa perbaikan agentik yang sadar solver dapat mengungguli alur kerja verifikasi tradisional pada track ini. Ablasi dan baseline agen murni lebih lanjut menunjukkan bahwa keuntungannya berasal dari perbaikan yang sadar solver, bukan semata-mata dari kehadiran agen LLM.
Beberapa batasan dan pertanyaan terbuka masih ada. Evaluasi dilaporkan untuk C dan Rust/Verus, sehingga generalisasi ke bahasa dan backend verifikasi lain belum ditetapkan. Kebijakan yang sadar teori mencakup obligasi numerik, terkuantifikasi, memori, dan floating-point, tetapi kombinasi teori lain mungkin memerlukan kebijakan tambahan. Makalah ini tidak melaporkan waktu per tugas atau penggunaan sumber daya solver dalam abstrak yang tersedia, sehingga biaya loop perbaikan relatif terhadap CPAchecker tidak dikuantifikasi di sini. Terakhir, track SV-COMP 2026 ReachSafety adalah keluarga benchmark yang spesifik; kinerja pada track lain dan pada basis kode skala industri masih perlu diuji.
Untuk praktik, Schwarz menyarankan prinsip desain bagi alat verifikasi agentik: ekspos antarmuka solver kepada agen dalam bentuk terstruktur yang terlokalisasi pada obligasi. Alih-alih meminta LLM memperbaiki kesalahan verifier global, berikan snapshot, slot lemma lokal, dan kebijakan yang sadar teori. Ini membuat tugas agen dapat diperiksa dan menjaga pencarian bukti tetap terbatas. Untuk pekerjaan selanjutnya, perluasan yang wajar adalah dukungan bahasa yang lebih luas, kebijakan teori yang lebih kaya, dan integrasi dengan asisten bukti interaktif tempat lemma lokal dapat digunakan kembali lintas obligasi.
Siapa yang sebaiknya membaca
Membuka konten member…