Anthropic vừa công bố kết quả hợp tác với Theorem: Claude đã tạo ra các chứng minh toán học cho thấy hơn 100 thư viện open source thực tế tuân thủ các quy tắc bảo mật, ngay ở cấp độ mã assembly (RISC-V). Theo Anthropic, đây là nỗ lực quy mô lớn đầu tiên dùng AI để kiểm chứng hình thức (formal verification) cho phần mềm thực tế.

Vì sao kiểm thử thông thường chưa đủ?

Phần mềm nào cũng có lỗi, kể cả những hệ thống được kiểm tra kỹ nhất. Nhân Linux, chạy trên hàng tỷ thiết bị, vừa có hơn 1.000 lỗ hổng được công bố. Trong khi đó, các mô hình AI ngày càng giỏi tìm lỗi và nối nhiều lỗi nhỏ thành một cuộc tấn công nghiêm trọng. Phòng thủ truyền thống vì thế không còn đủ.

Chứng minh thay vì chỉ thử

Kiểm chứng hình thức giống như chứng minh một định lý toán học: thay vì thử hàng triệu trường hợp rồi hy vọng không sót, người ta chứng minh rằng mã luôn tuân theo quy tắc đã đặt ra. Trước đây việc này cực kỳ tốn kém. Hệ điều hành seL4 mất 2 người-năm để viết nhưng tới 20 người-năm để chứng minh, nên chỉ dùng cho các lĩnh vực như hàng không của Airbus.

Ý nghĩa với người dùng

Trong quá trình viết chứng minh, Claude còn phát hiện những lỗi tồn tại nhiều năm dù đã chạy hàng nghìn tỷ lần kiểm thử. Nếu cách làm này phổ biến, ứng dụng ngân hàng, thiết bị y tế hay xe tự lái trong lĩnh vực công nghệ có thể đi kèm bảo đảm an toàn được chứng minh, thay vì chỉ "đã thử nhiều".