Anthropic chứng minh an toàn cho 239 điểm kiểm thử trong 123 thư viện mã nguồn mở

Anthropic đã dùng Claude để chứng minh bằng toán học rằng 239 điểm kiểm thử thuộc 123 thư viện mã nguồn mở đáp ứng các điều kiện an toàn được xác định trước.

Nhóm Frontier Red Team của Anthropic công bố nghiên cứu ngày 22, cho biết đã phối hợp với đơn vị kiểm chứng Theorem. Nhóm chuyển các bài kiểm thử hiện có thành điều kiện cần kiểm chứng, sau đó dùng một công cụ riêng để kiểm tra các chứng minh do Claude tạo ra.

Các thư viện được chọn nằm trong OSS-Fuzz, dự án mã nguồn mở của Google nhằm phát hiện lỗi. Nhóm nghiên cứu chuyển các bài kiểm thử fuzz hiện có thành mệnh đề: với mọi đầu vào dưới 64 MB, chương trình không bị dừng bất thường, không gặp lỗi an toàn bộ nhớ và không vi phạm điều kiện kiểm chứng. Claude tạo chứng minh, còn Rocq kiểm tra chúng.

Nhóm cho biết sau nhiều tuần sửa các lỗi Claude phát hiện, họ đã kiểm chứng 239 điểm kiểm thử trong 123 thư viện. Điểm kiểm thử là đường dẫn đầu vào được thiết kế để thử một chức năng cụ thể của chương trình. Các chứng minh áp dụng cho mã lệnh RISC-V đã biên dịch, thay vì mã nguồn ban đầu mà con người đọc; bộ chứng minh Rocq được tạo ra dài khoảng 180 triệu dòng.

Kiểm chứng hình thức là phương pháp dùng toán học để xác nhận chương trình tuân thủ các quy tắc đã nêu. Khác với kiểm thử truyền thống, vốn chạy các đầu vào để tìm lỗi, phương pháp này chứng minh mệnh đề đối với mọi đầu vào thuộc điều kiện đã đặt ra. Trong quá trình xây dựng chứng minh, nhóm cũng tìm thấy lỗi mà các bài kiểm thử hiện có chưa phát hiện. Sau khi sửa lỗi, họ lập lại điều kiện kiểm chứng cho phiên bản mã đã cập nhật.

Kết quả lần này chỉ áp dụng cho các chương trình RISC-V chạy trên Linux, đơn luồng, liên kết tĩnh và sử dụng dung lượng bộ nhớ cố định. Nghiên cứu không kiểm chứng mọi chức năng của từng thư viện hay toàn bộ môi trường triển khai thực tế. Anthropic cho biết công cụ chứng minh có thể xác nhận một mệnh đề có đúng hay không, nhưng không thể xác định liệu mệnh đề đó đã bao quát đầy đủ các điều kiện sử dụng trong thực tế hay chưa.

Trong một thử nghiệm riêng, nhóm cho biết Claude đã kiểm chứng phần triển khai zlib của nhân Linux ở cấp tệp thực thi x86. Nhóm cũng thử nghiệm một trình thông dịch Python viết bằng Rust trên hơn 1,7 triệu chương trình được tạo ngẫu nhiên; tỷ lệ hành vi khớp với CPython là 99,95%. Hai thử nghiệm này khác về đối tượng và phương pháp so với việc kiểm chứng 123 thư viện RISC-V.

Anthropic cũng công bố kết quả so sánh 36 nhiệm vụ kiểm chứng quy mô nhỏ. Claude Opus 5.5 dùng ít hơn khoảng 40% token so với Opus 5 để chứng minh một nửa số nhiệm vụ. Nhóm đã công khai một phần các chứng minh để những nhà phát triển khác có thể kiểm tra và tái sử dụng.