Anthropic Dùng Claude Để Chứng Minh Code Tự Động

Frontier Red Team của Anthropic làm việc với Theorem để giao phần chứng minh cho Claude. Model tạo ra khoảng 180 triệu dòng code chứng minh toán học chỉ trong vài tuần, dựa trên chương trình kiểm thử từ 123 thư viện mã nguồn mở trong dự án an ninh OSS-Fuzz của Google.

Trước đây, việc chứng minh phần mềm chạy không lỗi trong mọi hoàn cảnh rất tốn kém. Một nhóm chuyên gia đã cần 20 năm công sức để xác minh hình thức kernel hệ điều hành nhỏ seL4, nên cách này chỉ được dùng cho các trường hợp cực đoan như phần mềm hàng không của Airbus.

Cách làm của Anthropic là đổi các bài kiểm thử lỗi thành bài toán toán học, phân tích mã máy đã biên dịch rồi tạo ra các chứng minh dài. Một chương trình xác minh độc lập tên Rocq tự động kiểm tra các chứng minh đó, và Anthropic nói quy trình gần như không cần người rà lại.

Nhóm nghiên cứu gọi đây là quá trình tạo chứng minh hoàn toàn tự chủ, dù công cụ và nền tảng hình thức do con người ở Theorem xây dựng. Trong lúc tạo chứng minh, Claude gặp hàng trăm lỗi và được phép tự sửa. Nhiều lỗi chỉ hiện ra trong điều kiện rất cụ thể, như tệp vào rất lớn hoặc một chuỗi truy cập nhất định.

Khi kiểm tra một trình đọc PDF rất phổ biến, nhóm tìm ra số lỗi an ninh trong một tuần bằng với số lỗi thường được báo cho phần mềm đó trong cả một năm. Trong một ứng dụng khác, Claude phát hiện một lỗi logic bị bỏ sót hơn một thập kỷ.

Anthropic thừa nhận được xác minh hình thức không có nghĩa là không lỗi. Các chứng minh chỉ đúng dưới điều kiện chặt: một kiến trúc bộ xử lý cụ thể, chương trình một luồng, và đầu vào dưới 64 MB; trong thực tế, các thư viện này chạy trên phần cứng khác và trong cấu hình khác.

Chi phí tính toán rất cao, khi từng chứng minh có thể ngốn tới hàng trăm triệu token. Anthropic không công bố tổng chi phí dự án. Một thử nghiệm nhỏ hơn cho thấy chứng minh có thể dùng lại, và các model mới cũng hiệu quả hơn: Opus 5.5 giải quyết một nửa số chứng minh với khoảng 40% ít token hơn Opus 5.