Làn sóng khởi nghiệp dùng AI để "chứng minh toán học" cho phần mềm

Kiểm chứng hình thức (formal verification) — quá trình dùng toán học để chứng minh phần mềm không có lỗi — từ lâu vẫn là khái niệm xa xỉ mà chỉ các hệ thống quan trọng bậc nhất mới dám đầu tư. Nhưng làn sóng AI tạo sinh đang khiến lĩnh vực tưởng như khô khan này trở thành tâm điểm của một cuộc đua khởi nghiệp sôi động.

Nhà nghiên cứu Stanford Chuyue Sun và các cộng sự gần đây gây chú ý khi công bố một công cụ AI hoàn thành dự án kỹ thuật chỉ trong chưa đầy nửa ngày với chi phí dưới 500 USD — công việc mà trước đó cần ba chuyên gia hàng đầu làm suốt năm tháng thủ công. Kết quả này đang đánh thức một lĩnh vực lập trình và toán học vốn ít người biết đến.

Từ Signal đến chip Nvidia

Trong nhiều thập kỷ, giới phát triển phần mềm mơ về việc dùng toán học để chứng minh mã nguồn không có lỗi. Quy trình này đòi hỏi kỹ sư viết ra những phát biểu chính xác về mục tiêu của phần mềm, rồi chuyển mã nguồn thành các công thức có thể kiểm chứng. Dù các công ty đã chạy những bộ kiểm thử tinh vi để tìm lỗi, họ hiếm khi chi tiền cho kiểm chứng hình thức — phương pháp có thể phát hiện cả những hành vi bất thường khó lường nhất.

Giờ đây, hàng loạt startup đặt cược rằng AI tạo sinh sẽ biến kiểm chứng hình thức vừa thực tế vừa thiết yếu:

• &Truth — startup mà Sun gia nhập vào tháng 8, huy động được 70 triệu USD và đặt mục tiêu kiểm chứng được mọi ngôn ngữ lập trình. Nghiên cứu của Sun đã dùng AI để kiểm chứng một phần mã mã hóa cuộc trò chuyện trong ứng dụng Signal.
• Harmonic — do CEO Robinhood Vlad Tenev đồng sáng lập, nhận 295 triệu USD đầu tư, vừa công bố AI agent thiên về toán học mang tên Aristotle hỗ trợ kiểm chứng phần mềm viết bằng C và thiết kế phần cứng bằng Verilog. Đối tác thử nghiệm gồm cả Nvidia — công ty có quỹ đầu tư rót vốn vào Harmonic.
• Anthropic và Theorem — vừa công bố dùng AI tìm ra lỗi trong phần mềm mã nguồn mở mà hàng nghìn tỷ lần kiểm thử trước đó không phát hiện được, đồng thời ra mắt tiện ích mở rộng cho Claude.
• Truidic — do Madan Musuvathi thành lập sau hơn 20 năm làm việc tại Microsoft Research, thúc đẩy bởi lo ngại về các vụ tấn công như vụ OpenAI bị hack trên Hugging Face.

"Cầu, tòa nhà không sụp đổ vì người ta đã làm toán trước khi xây dựng. Tại sao chúng ta không làm điều tương tự với mã nguồn?" — Ilya Sergey, Giám đốc khoa học của &Truth.

Lợi ích đã được chứng minh, nhưng còn nhiều rào cản

Không phải ngẫu nhiên mà kiểm chứng hình thức gắn liền với những hệ thống quan trọng nhất. Theo công bố của các công ty, máy bay Boeing, máy chủ Amazon và hơn 2,5 tỷ thiết bị Apple đang hoạt động đều chứa ít nhất một phần phần mềm đã được kiểm chứng hình thức — thường là các đoạn mã liên quan đến bảo mật.

Byron Cook, nhà khoa học cấp cao tại AWS, cho biết kiểm chứng hình thức đã giúp giảm lo ngại của khách hàng về bảo mật đám mây và giúp các nhóm nội bộ làm việc nhanh hơn nhờ diệt lỗi lớn ngay từ đầu. Đội ngũ bảo mật của Apple cũng thừa nhận một số lỗi mà kiểm chứng hình thức phát hiện trong thư viện mã hóa corecrypto "không thể tìm ra bằng bất kỳ cách nào khác".

Tuy vậy, nhiều công ty công nghệ quy mô trung bình nói với WIRED rằng họ thường chỉ kiểm chứng một tính năng chính, nếu có. Lý do:

• Thiếu kỹ sư chuyên về kiểm chứng
• Chi phí vượt xa rủi ro tiềm tàng
• Lo ngại việc chờ đợi hàng tuần để kiểm chứng mã sẽ kìm hãm tốc độ đổi mới

"Không phải thuốc chữa bách bệnh"

Không phải ai cũng lạc quan. Will Wilson, người điều hành startup săn lỗi Antithesis, gọi kiểm chứng hình thức là "một cái bẫy" đối với những người mê toán như anh. Antithesis từng chi hàng triệu USD để kiểm chứng hình thức một số lớp phòng thủ an ninh mạng — quy trình Wilson mô tả là "cực kỳ khó chịu" — vậy mà công cụ riêng của họ vẫn tìm thêm được lỗi, và chính Antithesis cũng phát hiện lỗi trong phần mềm mà vài khách hàng đã kiểm chứng hình thức.

"Nó có thể mang lại cho bạn chút yên tâm, nhưng chỉ kiểm thử toàn diện và mạnh mẽ mới chứng minh được sự yên tâm đó là thật." — Will Wilson

Vitalik Buterin, kỹ sư nổi tiếng với việc tạo ra Ethereum, cũng thẳng thắn: "kiểm chứng hình thức không phải là thuốc chữa bách bệnh". Dù vậy, ông và nhiều người ủng hộ vẫn tin đây sẽ là lá chắn quan trọng chống lại các cuộc tấn công mạng do AI phát động.

Một lo ngại khác đến từ chính những người trong ngành: June Andronick và Gerwin Klein của Proofcraft cảnh báo các đặc tả do AI tạo ra có thể khơi dậy "niềm tin không có cơ sở" vào kết quả. Klein thừa nhận công việc kiểm chứng "gây nghiện như một trò chơi giải đố" — và nếu mọi chuyện suôn sẻ, ông sẽ còn được giải nhiều đố hơn bao giờ hết.

Bài toán chưa có lời giải

Câu hỏi lớn vẫn bỏ ngỏ: liệu AI có thể đưa kiểm chứng hình thức ra khỏi phạm vi các hệ thống tối quan trọng của NASA hay Apple để trở nên phổ biến? Công nghệ hiện vẫn ở giai đoạn thử nghiệm nguyên mẫu. Nhu cầu thì cao, nhưng chưa rõ khách hàng sẵn sàng trả bao nhiêu và muốn tiếp cận công nghệ theo cách nào.

Với các dự án mã nguồn mở — nền tảng của vô số ứng dụng — câu chuyện còn khó hơn. Michael Rosenberg, người duy trì thư viện curve25519-dalek, bày tỏ hy vọng sẽ có nguồn tài trợ bền vững cho các nỗ lực kiểm chứng lâu dài, nhưng thừa nhận: "Tôi không biết điều đó sẽ diễn ra thế nào, và chắc chắn chúng ta không nên trông chờ vào lòng tốt của các công ty AI."

Với độc giả Việt Nam quan tâm đến an toàn thông tin và phát triển phần mềm, làn sóng này đáng để theo dõi: nếu kiểm chứng hình thức thực sự được AI "dân chủ hóa", nó có thể thay đổi cách các doanh nghiệp công nghệ trong nước tiếp cận bảo mật — từ chỗ chạy theo sửa lỗi, chuyển sang chứng minh chủ động rằng phần mềm của mình đúng đắn ngay từ đầu.