50 Năm Tranh Luận: Kiểm Chứng Hình Thức Có Thực Sự 'Thất Bại' Như Bài Báo Kinh Điển Năm 1979 Từng Dự Đoán?

Trong bối cảnh các kỹ sư phần mềm đang dần hào hứng trở lại với kiểm chứng hình thức (formal verification) nhờ sức mạnh của AI, một câu hỏi thú vị được đặt ra: Liệu những lập luận phản đối từ 50 năm trước có còn đúng? Bài viết này sẽ mổ xẻ từng luận điểm trong bài báo kinh điển "Social Processes and Proofs of Theorems and Programs" (1979) và đối chiếu với sự phát triển của công nghệ hiện đại, đặc biệt là trong kỷ nguyên mã nguồn do AI tạo ra.

Sự Trỗi Dậy Bất Ngờ Của Một Lĩnh Vực Từng Bị Coi Là 'Chết Yểu'

Trong suốt nhiều thập kỷ, kiểm chứng hình thức thường bị giới kỹ sư phần mềm xem là "không thực tế", "lãng phí thời gian" hoặc chỉ hữu dụng trong vài trường hợp đặc thù như hàng không hay quân sự. Tuy nhiên, làn sóng AI viết mã đã thay đổi tất cả. Các tác nhân AI (AI agents) tạo ra một lỗ hổng lớn trong sự hiểu biết của con người về chương trình chúng viết, từ đó tạo nhu cầu cấp thiết về các phương pháp đảm bảo tính đúng đắn khác ngoài việc đọc code thủ công.

"AI agents để lại một lỗ hổng trong sự hiểu biết của chúng ta về các chương trình chúng viết, từ đó tạo ra nhu cầu về các phương tiện đảm bảo tính đúng đắn khác."

Nhìn vào Google Trends, có thể thấy lượng tìm kiếm về "formal verification" hay "formal methods" đã tăng vọt trong hai năm qua. Các ngôn ngữ đặc tả mới liên tục ra đời, cộng đồng học Lean (một trợ lý chứng minh toán học) ngày càng đông đảo, và có những dự án táo bạo như Signal Shot – nỗ lực xác minh end-to-end các ứng dụng quan trọng.

Lập Luận 1: Khoảng Cách Giữa Yêu Cầu Thực Tế Và Đặc Tả Hình Thức

Bài báo năm 1979 lập luận rằng, quá trình chuyển từ một yêu cầu "không chính thức" (mang tính trực quan của con người) sang một đặc tả hình thức (formal specification) là một quá trình đầy rủi ro, dễ sai sót và không thể kiểm chứng được.

Quan điểm hiện đại: Điều này vẫn đúng, nhưng có một điểm yếu trong lập luận: Đặc tả hình thức vẫn gần với yêu cầu thực tế hơn so với code triển khai. Vì vậy, sai sót trong đặc tả sẽ dễ bị phát hiện hơn. Hơn nữa, các ngôn ngữ đặc tả hiện đại như Quint cho phép lập trình viên tương tác, kiểm tra mọi trường hợp biên (edge-case) để đảm bảo đặc tả khớp với trực giác của mình.

Lập Luận 2: Sự Phụ Thuộc Giữa Đặc Tả Và Triển Khai

Tác giả bài báo cũ cho rằng đặc tả chỉ có giá trị khi nó độc lập với phần triển khai. Trong quy trình phát triển phần mềm lặp (iterative) như hiện nay, sự độc lập này gần như là bất khả thi.

Quan điểm hiện đại: Lập luận này ngay cả trong quá khứ cũng không thực sự mạnh, và càng yếu hơn khi có AI agents tham gia. Khi có thêm sự hiểu biết mới, điều này luôn tốt cho quy trình phát triển. Con người vẫn là người phân xử cuối cùng, quyết định đặc tả nên thay đổi theo hướng nào.

Điều thú vị là với AI agents, việc chúng được phép tạo code và tạo cả bằng chứng (proofs) là hoàn toàn hợp lý. Nhưng nếu cần sửa đổi đặc tả, chỉ con người mới có quyền quyết định điều gì là đúng đắn – điều này đưa chúng ta trở lại với thách thức về tính độc lập nhưng ở một cấp độ quản trị cao hơn.

Lập Luận 3: Bộ Máy Xác Minh Tự Động Hoàn Toàn Là Bất Khả Thi

Bài báo cho rằng việc xây dựng các bộ máy xác minh hoàn toàn tự động là "rất khó xảy ra". Trong 50 năm, đúng là vẫn cần nỗ lực của con người, nhưng công cụ AI đang thu hẹp khoảng cách này rất nhanh.

Hình minh họa: Robot đọc và kiểm chứng mọi thứ

Igor Konnov, trong bài viết "Formal proofs for distributed protocols with AI may be closer than you think", đã mô tả trải nghiệm chứng minh tính an toàn (safety) của giao thức Ben-Or trong Lean với sự hỗ trợ của AI. Điều này cho thấy rào cản về tốc độ và chi phí đang dần được gỡ bỏ.

Lập Luận 4: Giảm Động Lực Cho Các Lớp Phòng Thủ Khác

Các tác giả năm 1979 lo ngại rằng khi có một chương trình đã được "chứng minh đúng", lập trình viên sẽ chủ quan, bỏ bê các biện pháp phòng thủ khác như giám sát (monitoring), giới hạn tốc độ (rate-limiting)...

Quan điểm hiện đại: Đây là một lập luận yếu, dựa trên giả định tồi tệ nhất về hành vi của con người. Trong thực tế, kiểm chứng hình thức và các lớp phòng thủ khác là bổ trợ, không phải thay thế. Các hệ thống hiện đại vẫn cần giám sát để phát hiện các lỗi không lường trước được, ngay cả khi đã qua kiểm chứng.

Kết Luận: Không Phải 'Tất Cả Hoặc Không Có Gì'

Bài báo năm 1979 kết luận bằng một đoạn rất đáng suy ngẫm:

"Sự khao khát làm cho chương trình trở nên đúng đắn là mang tính xây dựng và quý giá. Nhưng cách nhìn 'nguyên khối' về kiểm chứng đã bỏ qua những lợi ích từ việc chấp nhận một tiêu chuẩn đúng đắn như chuẩn của các chứng minh toán học thực thụ, hay một tiêu chuẩn độ tin cậy như chuẩn của các công trình kỹ thuật thực thụ."

Tôi hoàn toàn đồng ý với quan điểm này. Kiểm chứng toàn phần (full verification) hiếm khi là cách tốt nhất để đạt độ tin cậy. Nhưng điều đó không có nghĩa là các mảnh ghép của formal methods trở nên vô dụng. Ngược lại, chúng cực kỳ hữu ích cho việc hiểu sâu hơn về hệ thống, đưa ra các quyết định thiết kế tốt hơn, và tăng tốc độ phát triển.

Trong kỷ nguyên AI viết code, các kỹ sư giờ đây tập trung vào việc đặc tả những gì cần viết và kiểm tra xem nó đã được viết đúng theo đặc tả hay chưa. Kiểm chứng còn giúp các tác nhân AI "khép kín vòng lặp" (close the loop) – biết được liệu thứ chúng viết ra có chính xác hay không. Đây chính là động lực lớn nhất cho sự trỗi dậy của lĩnh vực tưởng chừng đã "chết" này.

Bài viết dựa trên phân tích từ Ivan Gavran, có tham khảo ý kiến từ Thomas Pani và Ranadeep Biswas.