Anthropic phát triển phương pháp dùng AI để chứng minh toán học rằng phần mềm không có lỗi, hướng tới phần mềm không lỗi

Chuyện gì đã xảy ra?

Anthropic đã chia sẻ một cách mới gọi là "xác minh hình thức". Cách này viết mã phần mềm bằng ngôn ngữ giống toán học, rồi dùng toán để chứng minh mã không có lỗi. Anthropic làm việc cùng nhóm nghiên cứu Theorem và dùng mô hình AI Claude của mình để thực hiện. Nhóm đã thử nghiệm 123 thư viện phần mềm mã nguồn mở, tức là các gói mã miễn phí mà người khác có thể tái sử dụng. Mỗi khi quá trình chứng minh tìm ra lỗi, Claude giúp sửa lỗi rồi công việc tiếp tục.

Các con số và sự kiện chính

• Phép chứng minh áp dụng cho mã chạy trên bộ xử lý RISC-V (một loại chip CPU) với hệ điều hành Linux, dùng một lượng bộ nhớ cố định, dạng chương trình tĩnh một luồng (một chương trình chạy trong một dòng công việc).
• Trong điều kiện này, nhóm chứng minh được rằng các lỗi gây treo chương trình không xảy ra.
• Quá trình này dùng hơn 100 triệu token (đơn vị văn bản mà mô hình AI đọc và viết).
• Anthropic cho biết Claude Opus 5.5 cho kết quả với ít token hơn Claude Opus 5, trong một thử nghiệm gồm 36 lần chạy xác minh.

Vì sao đây không phải ý tưởng mới?

Xác minh hình thức đã có từ lâu. Nhưng các phép chứng minh cần rất nhiều công sức của con người. Vì vậy, cách này chủ yếu được dùng cho những hệ thống quan trọng đến tính mạng, như phần mềm trong máy bay. Nếu AI giúp giảm công sức, cách này có thể dùng được cho nhiều phần mềm hơn.

Vì sao điều này quan trọng?

AI đang tìm ra nhiều lỗi trong phần mềm, và có lỗi đã gây ra sự cố lớn, như bản cập nhật khẩn cấp cho PHP. Nếu AI cũng giúp chứng minh mã an toàn, phần mềm có thể đáng tin cậy hơn. Anthropic còn cho rằng chi phí token cao có thể giảm theo thời gian, vì các mô hình tốt hơn cần ít token hơn và các phép chứng minh có thể dùng lại cho phần mềm khác.

Cần theo dõi điều gì?

• Phép chứng minh hiện chỉ áp dụng cho RISC-V. Anthropic nói chip Arm và x86 vẫn có thể có lỗi, nên cần thử nghiệm thêm.
• Phép chứng minh phải bao phủ mọi môi trường máy tính mà phần mềm chạy. Anthropic cho rằng giới hạn này có thể được khắc phục khi phương pháp và mô hình tiến bộ.
• Theorem cung cấp phương pháp xác minh dựa trên LLM miễn phí cho các dự án mã nguồn mở.
• Kỹ năng xác minh được dùng trong công việc này cũng được công bố công khai trên GitHub.