Phòng thí nghiệm RDI của Đại học California, Berkeley vừa công bố một benchmark có tên Vero. Benchmark này yêu cầu tác nhân AI làm đồng thời hai việc ở quy mô toàn bộ kho mã: triển khai mọi API bắt buộc, đồng thời chứng minh mọi đặc tả được đưa ra là đúng, trong khi vẫn giữ mã nguồn, chứng minh và bản build luôn nhất quán với nhau. Các benchmark xác minh hình thức trước đây về cơ bản chỉ dừng ở mức một định lý hoặc một hàm đơn lẻ; đây là benchmark đầu tiên ở cấp độ toàn kho mã.
Đề bài gồm 43 dự án Lean 4 nhiều mô-đun, được chuyển thể từ mã nguồn hiện có viết bằng Python, Dafny, Verus và Coq, tổng cộng bao phủ 743 API và 2.705 đặc tả hình thức. Việc đánh giá chạy theo hai chế độ: chế độ chỉ chứng minh đưa sẵn phần triển khai tham chiếu, tác nhân chỉ cần chứng minh; chế độ mã và chứng minh yêu cầu tác nhân tự viết phần triển khai rồi chứng minh nó thỏa mãn đặc tả.
Bảng điểm
Số lượng giải trọn vẹn (trên tổng 43) trong ngân sách 90 phút:
| Cấu hình | Mã & chứng minh | Chỉ chứng minh |
|---|---|---|
| GPT-5.5 (xhigh) + Codex | 27 | 25 |
| Claude Opus 4.8 + Claude Code | 8 | 10 |
| GPT-5.5 (medium) + Codex | 2 | 6 |
| Claude Sonnet 5 + Claude Code | 2 | 2 |
Khoảng cách giữa dòng đầu và dòng thứ ba đáng chú ý: cùng một GPT-5.5, cùng một Codex, chỉ cần chuyển mức suy luận từ medium lên xhigh, điểm số ở chế độ mã và chứng minh nhảy từ 2 lên 27. Ở dạng nhiệm vụ này, lợi ích biên của ngân sách suy luận còn lâu mới bão hòa.
Cái khó không nằm ở từng chứng minh riêng lẻ
Dòng đầu bảng xếp hạng còn một bộ số khác. GPT-5.5 (xhigh) ở chế độ mã và chứng minh đạt tỷ lệ 87,3% trên từng đặc tả riêng lẻ, ở chế độ chỉ chứng minh là 85,8%, nhưng xét theo tiêu chí 'toàn bộ dự án được giải trọn vẹn' thì chỉ còn 27/43 và 25/43. Nhận định của nhóm nghiên cứu rất rõ ràng: chứng minh từng đặc tả riêng lẻ không còn là điểm khó, cái khó là giữ cho toàn bộ kho chứng minh nhất quán với nhau.
Khoảng cách giữa hai con số này có ý nghĩa kỹ thuật thực sự. Tỷ lệ đạt 87% trên từng đặc tả, quy đổi sang một dự án có vài chục đặc tả, đồng nghĩa gần như dự án nào cũng sẽ còn sót lại vài đặc tả bị kẹt. Mà xác minh hình thức là kiểu được ăn cả ngã về không: chỉ cần một đặc tả chưa chứng minh xong, toàn bộ kho không build được, những phần đã chứng minh đúng trước đó cũng không được tính điểm một phần nào. Điều này hoàn toàn khác với một dự án có bộ kiểm thử đơn vị đạt 87% vẫn có thể lên sản phẩm.
Một chi tiết khác nằm ở thành phần của mã chứng minh. Trong những lượt chạy giải trọn vẹn, các bổ đề phụ trợ chiếm trung vị 73,6% mã chứng minh. Nói cách khác, ba phần tư những gì tác nhân viết ra là giàn giáo tạm dựng để đỡ cho chứng minh chính. Tỷ lệ này cho thấy các mô hình hiện nay đang đi theo hướng ưu tiên chiều rộng, chất chồng bổ đề để ép ra kết quả, thay vì tìm ra cấu trúc chứng minh gọn gàng.
Tự chọn thuật toán: giúp ích 5 lần, phản tác dụng 17 lần
Chế độ mã và chứng minh cho tác nhân một bậc tự do: phần triển khai có thể tự viết, nghĩa là có thể chọn một thuật toán dễ chứng minh hơn. Nhóm nghiên cứu đã thống kê hiệu quả ròng của bậc tự do này: qua so sánh theo cặp, có 5 trường hợp thành công nhờ đổi thuật toán, nhưng 17 trường hợp lại thất bại vì chính điều đó.
Tỷ lệ 5 trên 17 này khá đáng nói. Về lý thuyết, việc được tự chọn cách triển khai lẽ ra chỉ có lợi chứ không hại — tệ nhất thì cứ chép lại phần triển khai tham chiếu. Nhưng thực tế mô hình thường chọn một cách viết mà nó cho là 'thông minh' nhưng lại khó chứng minh hơn, rồi sa lầy trong 90 phút không thoát ra được. Biết viết code và biết loại code nào dễ chứng minh là hai năng lực khác nhau, còn tác nhân AI hiện tại mới chỉ có năng lực đầu.
Bảng xếp hạng còn để lại một điểm: trong 43 dự án, có 10 dự án không hề được giải bởi bất kỳ cấu hình nào, ở cả hai chế độ. Nhóm này tạo thành giới hạn cứng hiện tại của phương pháp, cũng là nơi vòng nghiên cứu tiếp theo cần tập trung nhất.
Với những người làm công cụ lập trình AI, giá trị tham khảo của Vero không nằm ở bảng xếp hạng, mà ở chỗ nó tách 'tính nhất quán ở cấp toàn kho mã' — thứ trước đây chỉ cảm nhận được bằng kinh nghiệm — thành một chỉ số có thể đo được. Các benchmark kiểu SWE-bench đo khả năng sửa đúng một lỗi, còn Vero đo khả năng chịu được toàn bộ ràng buộc của một dự án kỹ thuật, hai loại độ khó này không cùng một cấp độ.
Nguồn tham khảo: blog công khai của phòng thí nghiệm RDI, Đại học California, Berkeley, CocoLoop; quy mô benchmark, số lượng giải trọn vẹn ở hai chế độ, tỷ lệ đạt từng đặc tả, tỷ trọng bổ đề phụ trợ và số liệu so sánh theo cặp đều được đối chiếu theo báo cáo công khai.