Benchmark Vero Berkeley: Hanya 27 dari 43 Repo Terpecahkan Penuh

Berkeley RDI Lab merilis benchmark baru bernama Vero. Benchmark ini meminta agen AI melakukan dua hal sekaligus, pada skala seluruh basis kode: mengimplementasikan setiap API yang dibutuhkan, dan membuktikan bahwa setiap spesifikasi yang diberikan benar-benar terpenuhi, sambil menjaga kode, bukti, dan proses build tetap konsisten sepanjang waktu. Benchmark verifikasi formal sebelumnya umumnya berhenti pada level satu teorema atau satu fungsi saja; benchmark setingkat repositori penuh ini adalah yang pertama.

Soal ujiannya terdiri dari 43 proyek Lean 4 multi-modul, yang dipindahkan dari kode yang sudah ada dalam Python, Dafny, Verus, dan Coq, mencakup total 743 API dan 2.705 spesifikasi formal. Evaluasi dijalankan dalam dua mode: dalam mode hanya-bukti, agen diberi implementasi acuan dan hanya bertugas menulis buktinya; dalam mode kode-dan-bukti, agen harus menulis sendiri implementasinya lalu membuktikan bahwa implementasi itu memenuhi spesifikasi.

Papan skor

Jumlah instance yang terpecahkan penuh (dari total 43) dengan batas waktu 90 menit:

Celah antara baris pertama dan ketiga patut dicermati: dengan GPT-5.5 dan Codex yang sama persis, hanya dengan menaikkan pengaturan reasoning dari medium ke xhigh, skor mode kode-dan-bukti melompat dari 2 menjadi 27. Untuk jenis tugas seperti ini, imbal hasil marjinal dari anggaran reasoning masih jauh dari titik jenuh.

Yang sulit bukan pembuktian satu spesifikasi

Baris teratas itu menyimpan sepasang angka lain. GPT-5.5 (xhigh) berhasil melewati 87,3% spesifikasi individual dalam mode kode-dan-bukti, dan 85,8% dalam mode hanya-bukti. Tapi begitu tolok ukurnya berubah menjadi “seluruh instance diselesaikan secara penuh,” angka itu anjlok menjadi 27/43 dan 25/43. Kesimpulan para peneliti cukup tegas: membuktikan satu spesifikasi saja bukan lagi bagian yang sulit — yang sulit adalah menjaga konsistensi seluruh repositori bukti.

Celah antara kedua angka ini punya konsekuensi rekayasa yang nyata. Tingkat kelulusan 87% pada spesifikasi individual berarti, pada proyek dengan puluhan spesifikasi, hampir setiap proyek akan menyisakan beberapa spesifikasi yang macet. Dan verifikasi formal itu sifatnya semua-atau-tidak-sama-sekali: kalau satu saja spesifikasi belum terbukti, seluruh repositori gagal di-build, dan bagian yang sudah terbukti benar sebelumnya pun tidak mendapat nilai parsial sama sekali. Ini jauh berbeda dari proyek software biasa yang lolos 87% unit test dan tetap bisa dirilis.

Detail lain menyangkut komposisi kode bukti itu sendiri. Dari seluruh proses yang berhasil diselesaikan penuh, lemma bantu (auxiliary lemma) menyumbang median 73,6% dari kode bukti. Artinya, tiga perempat dari yang ditulis agen AI itu sebenarnya hanya perancah sementara untuk menopang bukti utama. Rasio ini mengisyaratkan bahwa model saat ini cenderung mengambil pendekatan breadth-first — menumpuk lemma untuk menerobos secara paksa — alih-alih menemukan struktur bukti yang ringkas.

Memilih algoritma sendiri: membantu 5 kali, merugikan 17 kali

Mode kode-dan-bukti memberi agen satu derajat kebebasan tambahan: karena implementasinya ditulis sendiri, agen bisa memilih algoritma yang lebih mudah dibuktikan. Para peneliti mengukur efek bersih dari kebebasan ini lewat perbandingan berpasangan: pergantian algoritma membawa keberhasilan pada 5 kasus, tapi justru menyebabkan kegagalan pada 17 kasus.

Rasio 5 berbanding 17 ini cukup mengatakan banyak hal. Secara teori, kebebasan memilih implementasi sendiri seharusnya hanya menguntungkan — dalam skenario terburuk, agen tinggal menyalin implementasi acuan. Kenyataannya, model sering memilih implementasi yang dianggapnya cerdas, yang ternyata jauh lebih sulit dibuktikan, lalu terjebak di sana selama 90 menit penuh tanpa bisa keluar. Kemampuan menulis kode dan kemampuan mengenali kode mana yang mudah dibuktikan adalah dua hal yang berbeda, dan agen AI saat ini baru menguasai yang pertama.

Papan peringkat masih menyisakan satu catatan lagi: dari 43 instance, 10 di antaranya tidak pernah berhasil diselesaikan oleh konfigurasi apa pun, di kedua mode sekalipun. Instance-instance ini menandai batas keras dari metode yang ada saat ini, dan menjadi titik yang paling perlu diperhatikan pada putaran riset berikutnya.

Bagi orang-orang yang membangun alat coding berbasis AI, nilai penting Vero bukan pada peringkatnya, melainkan pada cara benchmark ini mengubah “konsistensi setingkat repositori” — sesuatu yang sebelumnya hanya bisa dinilai berdasarkan feeling — menjadi metrik yang bisa diukur. Benchmark seperti SWE-bench menguji apakah model bisa memperbaiki satu bug dengan benar; Vero menguji apakah model bisa bertahan di bawah keseluruhan batasan sebuah proyek rekayasa. Keduanya berada pada tingkat kesulitan yang sama sekali berbeda.

Sumber: blog publik Berkeley RDI Lab, CocoLoop; skala benchmark, jumlah penyelesaian penuh untuk kedua mode, tingkat kelulusan per spesifikasi, proporsi lemma bantu, dan statistik perbandingan berpasangan telah diverifikasi sesuai laporan publik.