Anthropic: Claude đã xác minh chính thức quy mô lớn đối với thư viện mã nguồn mở

Ngày 22 tháng 10, Frontier Red Team thuộc công ty trí tuệ nhân tạo Anthropic đã công bố một nghiên cứu cho thấy các mô hình ngôn ngữ lớn hiện nay đã có khả năng tự động sinh ra các chứng minh hình thức ở quy mô lớn hơn. Nhóm này, phối hợp cùng Theorem, đã thực hiện xác minh hình thức các thuộc tính an toàn trên hơn 100 thư viện mã nguồn mở thực tế ở cấp độ tập lệnh RISC-V, dựa trên mô hình Claude — đây là lần đầu tiên một hệ thống AI tiến hành xác minh hình thức quy mô lớn đối với phần mềm mức sản xuất ở cấp độ tập lệnh. Trong quá trình xây dựng các chứng minh, nhóm còn tình cờ phát hiện nhiều lỗ hổng bảo mật tồn tại từ lâu nhưng chưa từng được phát hiện. Phương pháp thử nghiệm bao gồm việc chuyển đổi các bộ kiểm thử fuzz có thể biên dịch sẵn trong Google OSS-Fuzz thành đặc tả hình thức, rồi thực hiện xác minh trên các đầu vào có kích thước tối đa 64 MB, trong các ràng buộc như: phân tích tĩnh nhị phân đơn luồng, ngân sách bộ nhớ cố định, kiến trúc CPU RISC-V và môi trường chạy Linux.