UC Berkeley ra mắt Vero: Thử thách AI tự lập trình và kiểm chứng phần mềm ở cấp độ kho lưu trữ

Vero: Các AI Agent có thể xây dựng các kho lưu trữ phần mềm được kiểm chứng hình thức (formally verified) không?

Zhe Ye*, Hantao Lou*, Yuechun Sun*, Peiyang Song, Zhengxu Yan, Timothe Kasriel, Qingyang Zhang, Kaiyu Yang, Soonho Kong, Jingxuan He, Dawn Song UC Berkeley; Đại học Chicago; Viện Công nghệ California; Đại học Stanford; Apodex; Amazon Web Services *Đóng góp ngang nhau Tháng 9, 2026 | Thời gian đọc khoảng 10 phút | Bài báo | Trang web dự án | GitHub

Các AI coding agent hiện đã có thể thực hiện thay đổi trên toàn bộ kho lưu trữ (repository). Nhưng sau khi một agent báo cáo rằng “tất cả các bài kiểm thử (test) đều vượt qua”, liệu chúng ta có thể tin tưởng chúng và mã nguồn của chúng không?

Các AI coding agent hiện đã có thể thực hiện thay đổi trên toàn bộ kho lưu trữ và chúng thường kết thúc bằng việc báo cáo rằng tất cả các bài kiểm thử đều vượt qua. Báo cáo đó không có nhiều giá trị như vẻ ngoài của nó, bởi vì các bài kiểm thử chỉ kiểm tra những trường hợp mà ai đó đã nghĩ đến việc viết ra. Kiểm chứng hình thức (formal verification) mang lại sự đảm bảo mạnh mẽ hơn nhiều. Nó tạo ra một bằng chứng được máy tính kiểm tra rằng một triển khai thỏa mãn đặc tả (specification) của nó trên mọi đầu vào mà đặc tả đó bao phủ, chứ không chỉ những trường hợp có trong bộ kiểm thử. Vì vậy, câu hỏi tự nhiên là liệu một AI agent có thực sự làm việc ở tiêu chuẩn này trên một cơ sở mã (codebase) thực tế hay không. Liệu nó có thể triển khai mọi API được yêu cầu trong một kho lưu trữ đa mô-đun, chứng minh mọi đặc tả được cung cấp và giữ cho mã nguồn, các bằng chứng và bản dựng (build) nhất quán trong suốt quá trình hay không? Chúng tôi đã xây dựng Vero để đo lường chính xác điều đó.

Tóm tắt (TL;DR)

Theo hiểu biết của chúng tôi, Vero là bộ tiêu chuẩn (benchmark) đầu tiên yêu cầu các agent thực hiện triển khai và chứng minh cùng lúc ở cấp độ kho lưu trữ. Nó chứa 43 trường hợp Lean 4 đa mô-đun được tuyển chọn từ các dự án thực tế vốn được viết bằng Python, Dafny, Verus và Coq. Trong toàn bộ bộ tiêu chuẩn, các agent phải đối mặt với 743 API được chấm điểm và 2.705 đặc tả hình thức.

Bộ tiêu chuẩn chạy ở hai chế độ. Trong chế độ chỉ chứng minh (proof-only), agent nhận các triển khai tham chiếu và chứng minh các đặc tả dựa trên chúng. Trong chế độ mã và chứng minh (code-and-proof), agent tự viết mọi API được yêu cầu và sau đó chứng minh rằng mã của chính nó thỏa mãn mọi đặc tả.

Cấu hình mạnh nhất mà chúng tôi đánh giá, GPT-5.5 (xhigh) với Codex, giải quyết hoàn toàn 27 trên 43 trường hợp ở chế độ mã và chứng minh và 25 trên 43 ở chế độ chỉ chứng minh. Nó vượt qua lần lượt 87,3% và 85,8% các đặc tả riêng lẻ. Mặc dù vậy, 10 trường hợp vẫn chưa được giải quyết bởi bất kỳ cấu hình nào ở cả hai chế độ. Tổng hợp lại, các con số cho thấy việc chứng minh các đặc tả riêng lẻ không còn là phần khó nhất. Phần khó nhất là duy trì sự nhất quán cho toàn bộ kho lưu trữ bằng chứng để mọi thứ có thể build được và mọi nghĩa vụ chứng minh (proof obligation) đều được hoàn tất.

Những điểm chính

Việc hoàn thiện kho lưu trữ khó hơn nhiều so với thành công trên từng đặc tả riêng lẻ. GPT-5.5 (xhigh) vượt qua 87,3% đặc tả trong chế độ mã và chứng minh và 85,8% trong chế độ chỉ chứng minh, nhưng chỉ hoàn thành đầy đủ 27/43 và 25/43 trường hợp. Vero chỉ tính một lần chạy là giải quyết hoàn toàn khi mọi đặc tả được cung cấp đều được chứng minh và kho lưu trữ được chấm điểm vẫn có thể build được và không chứa các tiên đề (axiom) không hợp lệ.

Các thư viện bổ đề (lemma) có thể tái sử dụng là một mô hình nhất quán trong các lần giải quyết hoàn toàn. Trong 82 lần giải quyết hoàn toàn, các định lý hỗ trợ do agent viết chiếm trung vị là 73,6% số dòng chứng minh trong chế độ mã và chứng minh và 71,6% trong chế độ chỉ chứng minh. Trong 80 trên 82 lần giải quyết hoàn toàn, ít nhất một định lý hỗ trợ phục vụ cho hai hoặc nhiều đặc tả; trong 65 lần, một định lý hỗ trợ phục vụ ít nhất năm đặc tả.

Sự tự do trong triển khai vừa có lợi vừa có hại. Các agent đôi khi thay thế một thuật toán tham chiếu khó chứng minh bằng một triển khai đơn giản hơn nhưng vẫn thỏa mãn các đặc tả tương tự. Bài báo xác định năm cặp trường hợp-agent trên ba kho lưu trữ mà điều này mang lại hiệu quả. Ngược lại, có 17 cặp tương ứng là giải quyết hoàn toàn ở chế độ chỉ chứng minh nhưng lại thất bại ở chế độ mã và chứng minh.

Bộ tiêu chuẩn vẫn còn nhiều dư địa để phát triển. 10 trên 43 trường hợp vẫn chưa được giải quyết bởi bất kỳ cấu hình nào ở cả hai chế độ. Bài báo liên kết nhiều thất bại còn lại với các bất biến toàn cục (global invariants), hành vi lặp lại, các định nghĩa được cung cấp và các chuỗi bổ đề có thể tái sử dụng phức tạp.

Tại sao Vero mới mẻ và quan trọng

Hầu hết các bộ tiêu chuẩn mã được kiểm chứng đều tập trung vào các hàm riêng lẻ. Một vài bộ tiêu chuẩn ở quy mô kho lưu trữ thường cung cấp một triển khai cố định và chỉ đánh giá việc tạo bằng chứng. Do đó, chúng bỏ qua một khó khăn cốt lõi của công việc kiểm chứng thực tế: các lựa chọn về triển khai và chứng minh ảnh hưởng lẫn nhau trên toàn bộ cơ sở mã.

Vero biến sự ràng buộc đó thành nhiệm vụ chính. Các agent phải đưa ra các lựa chọn nhất quán trên một dự án Lean 4 đa mô-đun, thay vì giải quyết một chuỗi các lỗ hổng chứng minh độc lập. Điều này làm lộ ra các vấn đề về kỹ thuật chứng minh dài hạn, sự phối hợp giữa triển khai-chứng minh và việc duy trì bản dựng mà các đánh giá ở cấp độ hàm không đo lường được.

Cách Vero hoạt động

Khung kho lưu trữ (Repository scaffold)

Mỗi trường hợp Vero là một dự án Lean 4 độc lập. Lean 4 là một ngôn ngữ lập trình và trình chứng minh định lý, trong đó các bằng chứng được kiểm tra bởi một nhân (kernel) nhỏ đáng tin cậy. Người quản lý cung cấp ba lớp nội dung cố định:

Các kiểu dữ liệu chia sẻ và định nghĩa hỗ trợ.

Các chữ ký API xác định những gì cần phải triển khai.

Các đặc tả hình thức được viết dưới dạng các vị từ (predicates) trên một giao diện triển khai toàn kho lưu trữ.

Agent điền vào các phần thân triển khai và các nghĩa vụ chứng minh. Một lần giải quyết hoàn toàn yêu cầu mọi nghĩa vụ được chỉ định phải vượt qua khi trình chấm điểm xây dựng lại kho lưu trữ từ một nguồn chuẩn sạch.

Hình 1. Quy trình xây dựng, đánh giá, chấm điểm và kiểm toán hình thức từ đầu đến cuối của Vero.

Một khung, hai chế độ

Chế độ chỉ chứng minh. Bộ tiêu chuẩn cung cấp triển khai tham chiếu. Agent phải chứng minh mọi đặc tả dựa trên đó. Điều này cô lập việc xây dựng bằng chứng trong khi vẫn giữ được các phụ thuộc ở quy mô kho lưu trữ.

Chế độ mã và chứng minh. Các phần thân triển khai tham chiếu bị ẩn đi. Agent viết mọi phần thân API được yêu cầu và chứng minh từng đặc tả tương ứng dựa trên triển khai của chính nó. Đây là thiết lập tạo đồng thời chính của Vero.

Chế độ mã và chứng minh bổ sung các nghĩa vụ triển khai ngoài việc xếp chồng nhiệm vụ. Một thuật toán thân thiện với chứng minh có thể dễ kiểm chứng hơn nhiều so với một thuật toán tham chiếu trung thực nhưng khó, trong khi một lựa chọn triển khai kém có thể tạo ra các nghĩa vụ chứng minh mới hoặc làm hỏng bản dựng.

Chấm điểm độc lập và các biện pháp bảo vệ chống gian lận

Trình chấm điểm chỉ trích xuất nội dung từ các vùng được phép chỉnh sửa bởi agent, chèn nó vào một dự án mới được tạo từ nguồn chuẩn và xây dựng lại toàn bộ dự án. Nó kiểm tra các phụ thuộc chứng minh dựa trên một danh sách cho phép các tiên đề (axiom allowlist) và sử dụng các bộ lọc dựa trên quy tắc và LLM-judge để loại bỏ các khai báo hoặc instance typeclass làm tầm thường hóa các nghĩa vụ. Các biện pháp bảo vệ này được thiết kế để đảm bảo rằng các bằng chứng được công nhận là đã được máy tính kiểm tra và không phụ thuộc vào việc chỉnh sửa nội dung chuẩn cố định hoặc các tiên đề không được phép.

Được xây dựng từ các kho lưu trữ thực tế

Vero chứa 43 trường hợp: 13 trường hợp được dịch từ các dự án nhận thức kiểm chứng viết bằng Dafny, Verus hoặc Coq, và 30 trường hợp được dịch từ các dự án Python mà người quản lý cũng viết các đặc tả hình thức cho chúng. Bộ tiêu chuẩn bao gồm các hợp đồng thông minh và giao thức blockchain, hệ thống phân tán và đồng thuận, cơ sở hạ tầng quan trọng về bảo mật, toán học hình thức, cấu trúc dữ liệu, thuật toán và các tiện ích số.

Quy trình tuyển chọn tuân theo các bước: khám phá, lựa chọn, lập kế hoạch, dịch thuật, viết đặc tả khi cần và xác thực. Mỗi giai đoạn chạy như một AI agent với sự kiểm soát của con người. Các triển khai Lean 4, đặc tả và bằng chứng thực tế (ground-truth) thu được là công trình tuyển chọn mới; không có bằng chứng thực tế Lean 4 công khai nào tồn tại trước đó cho các trường hợp được đánh giá.

Đánh giá và kết quả chính

Việc đánh giá bao gồm bốn cấu hình coding-agent tiên tiến dưới hai bộ khung agent. Mỗi lần chạy đều nhận được toàn quyền truy cập hệ thống tệp, bản dựng và chuỗi công cụ Lean cùng với ngân sách thời gian thực là 90 phút.

Bảng 1. Kết quả toàn bộ kho lưu trữ sau ngân sách 90 phút.

GPT-5.5 (xhigh) đạt được 25 lần giải quyết hoàn toàn ở chế độ mã và chứng minh và 23 lần ở chế độ chỉ chứng minh trong vòng 45 phút. Mặc dù vậy, hầu hết các trường hợp được giải quyết chỉ bởi một cấu hình duy nhất và 10 trường hợp vẫn chưa được giải quyết trên tất cả tám tổ hợp agent-chế độ.

Hình 2. Quỹ đạo giải quyết hoàn toàn và ma trận giải quyết hoàn toàn chính xác.

Vero sử dụng việc giải quyết hoàn toàn làm kết quả chính vì độ bao phủ đặc tả một phần có thể bị thổi phồng bởi các nghĩa vụ dễ dàng hơn. Trong chế độ mã và chứng minh, một đặc tả chưa được chứng minh có thể chỉ ra một bằng chứng còn thiếu hoặc một triển khai không vượt qua được đặc tả đó. Độ bao phủ trên từng đặc tả vẫn hữu ích cho việc chẩn đoán, nhưng chỉ độ bao phủ hoàn toàn mới chứng nhận triển khai đã gửi dựa trên tất cả các đặc tả của bộ tiêu chuẩn.

Kết quả tiết lộ điều gì