Những phép toán "đầy phiền toái" có thể giải cứu vibe coding khỏi chính nó

Paresh Dave Kinh doanh Ngày 29/10/2026, 11 giờ 00 phút Phương pháp toán học phức tạp có thể giải cứu xu hướng "Vibe Coding" Công ty khởi nghiệp mới mang tên &Truth đang tham gia cuộc đua tự động hóa quy trình kiểm chứng hình thức (formal verification) - một phương pháp phức tạp sử dụng toán học để chứng minh phần mềm vận hành đúng như thiết kế. Ảnh minh họa: Jobanny Cabrera; Getty Images CommentLoader Lưu bài viếtLưu bài viết này CommentLoader Lưu bài viếtLưu bài viết này Nhà nghiên cứu Chuyue Sun tại Đại học Stanford cùng các đồng nghiệp trong lĩnh vực khoa học máy tính đã phát triển một công cụ AI có khả năng hoàn thành một dự án kỹ thuật trong chưa đầy nửa ngày với chi phí dưới 500 USD, so với khoảng thời gian năm tháng mà ba chuyên gia trình độ cao phải thực hiện thủ công. Sự sụt giảm đáng kể về thời gian và chi phí, được bà Sun công bố trong một bài báo khoa học gần đây, là một trong những kết quả ban đầu giúp hồi sinh một lĩnh vực lập trình và toán học vốn ít được biết đến: kiểm chứng hình thức. Trong nhiều thập kỷ qua, các nhà phát triển luôn kỳ vọng sử dụng toán học để chứng minh phần mềm không có lỗi. Quy trình này đòi hỏi nhiều thời gian và công sức, buộc các kỹ sư phải đưa ra các phát biểu chính xác về mục tiêu của phần mềm và chuyển đổi mã nguồn thành các công thức có thể kiểm chứng. Dù các doanh nghiệp hiện đã áp dụng các quy trình kiểm thử tinh vi để phát hiện tối đa các khiếm khuyết trong phần mềm, họ hiếm khi chi trả cho việc kiểm chứng hình thức - phương pháp có khả năng phát hiện những hành vi bất thường khó lường hơn. Hiện nay, một làn sóng các công ty khởi nghiệp đang đặt cược rằng AI tạo sinh sẽ giúp việc kiểm chứng hình thức phần mềm trở nên khả thi và mang tính thiết yếu. Trong số đó có &Truth, công ty mà bà Sun đã gia nhập vào tháng 8 và vừa chính thức ra mắt vào thứ Năm. Nghiên cứu của bà Sun đã chứng minh tiềm năng của công nghệ này thông qua việc sử dụng AI để kiểm chứng một phần mã nguồn mã hóa các cuộc trò chuyện trên ứng dụng nhắn tin Signal. "Cầu cống hay các công trình xây dựng không bị sụp đổ vì con người đã tính toán toán học trước khi thi công", ông Ilya Sergey, Giám đốc khoa học của &Truth cho biết. "Tại sao chúng ta không làm điều tương tự đối với mã nguồn? Công nghệ suy luận toán học đã có sẵn, chỉ là rất khó để mở rộng quy mô." &Truth đã huy động được 70 triệu USD từ các nhà đầu tư và đặt mục tiêu kiểm chứng mọi ngôn ngữ lập trình trong tương lai. Đối thủ Harmonic, do Tổng Giám đốc điều hành Robinhood Vlad Tenev đồng sáng lập và đã nhận được 295 triệu USD tài trợ, tuần này thông báo rằng tác tử AI chuyên về toán học Aristotle của họ hỗ trợ kiểm chứng phần mềm viết bằng ngôn ngữ C và các thiết kế phần cứng bằng Verilog. Doanh nghiệp này đang đánh giá công nghệ với các khách hàng tiềm năng, bao gồm các nhà sản xuất chip Tensordyne và Nvidia, trong đó nhánh đầu tư mạo hiểm của Nvidia cũng là một trong những nhà đầu tư của công ty. Tuần trước, Anthropic và công ty khởi nghiệp kiểm chứng Theorem đã cùng công bố việc sử dụng AI để hỗ trợ tìm kiếm các lỗi trong phần mềm mã nguồn mở mà hàng nghìn tỷ lượt kiểm thử trước đó không thể phát hiện. Hai bên cũng giới thiệu một tiện ích bổ sung cho Claude nhằm hỗ trợ các nhà phát triển khác trong công tác kiểm chứng. Chi phí của dự án ban đầu không được tiết lộ. Kỳ vọng lớn nhất là hướng tới một tương lai nơi phần mềm vận hành tin cậy hơn và giảm bớt các mối lo ngại về an ninh mạng. Tuy nhiên, liệu AI có thể đưa phương pháp kiểm chứng hình thức vượt ra ngoài các hệ thống tối quan trọng tại những tổ chức như NASA hay Apple để ứng dụng rộng rãi hay không vẫn là câu hỏi còn bỏ ngỏ. Công nghệ này hiện vẫn đang trong giai đoạn thử nghiệm nguyên mẫu. Dù nhu cầu rất lớn, mức chi phí khách hàng sẵn sàng chi trả cũng như phương thức họ lựa chọn để tiếp cận công nghệ vẫn chưa rõ ràng. Kiểm chứng hình thức phụ thuộc vào việc đưa ra các giả định về cách máy tính và con người tương tác với phần mềm, và một số chuyên gia vẫn hoài nghi về khả năng của phương pháp này trong việc phát hiện các lỗi phát sinh từ thao tác người dùng hay sự cố phần cứng. Ông Will Wilson, người điều hành Antithesis - một công ty khởi nghiệp ứng dụng AI trong tìm kiếm lỗi phần mềm, gọi phương pháp kiểm chứng hình thức (formal verification) là "một cái bẫy" đối với những người đam mê toán học như ông. Antithesis đã chi hàng triệu USD để kiểm chứng hình thức cho một số hệ thống phòng thủ an ninh mạng của mình, một quy trình được ông Wilson mô tả là "hết sức nan giải". Tuy vậy, công ty khởi nghiệp này vẫn phát hiện thêm các lỗi khác bằng công cụ do chính mình phát triển; Antithesis cũng tìm thấy lỗi trong phần mềm của nhiều khách hàng vốn đã được kiểm chứng hình thức. Ông Wilson nhận định: "Phương pháp này có thể đem lại sự an tâm nhất định, nhưng chỉ việc kiểm thử toàn diện và kỹ lưỡng mới có thể chứng minh sự an tâm đó là có cơ sở". Đồng quan điểm, ông Vitalik Buterin, kỹ sư sáng lập đồng tiền mã hóa Ethereum, từng nhận định trong một bài viết hồi đầu năm rằng: "Kiểm chứng hình thức không phải là phương thuốc vạn năng". Dù vậy, ông cùng các bên ủng hộ cách tiếp cận này vẫn tin rằng đây sẽ là tuyến phòng thủ quan trọng trước nguy cơ các hệ thống AI tiến hành tấn công mạng và gây ra thiệt hại trên diện rộng. An ninh cốt lõi Theo thông tin công bố từ các doanh nghiệp, máy bay của Boeing, máy chủ của Amazon và hơn 2,5 tỷ thiết bị Apple đang hoạt động đều tích hợp một số phần mềm đã qua kiểm chứng hình thức. Các đoạn mã này thường liên quan đến an ninh bảo mật, nơi các lỗ hổng có thể dẫn tới hậu quả nghiêm trọng nếu bị khai thác. Ông Byron Cook, nhà khoa học xuất sắc kiêm Phó Chủ tịch tại Amazon Web Services, cho biết kiểm chứng hình thức đã giải tỏa mối lo ngại của khách hàng về bảo mật điện toán đám mây và giúp các đội ngũ nội bộ đẩy nhanh tiến độ công việc nhờ khắc phục sớm các lỗi lớn. Tuy nhiên, chia sẻ với tạp chí WIRED, đại diện một số công ty công nghệ quy mô vừa cho biết họ thường chỉ kiểm chứng duy nhất một tính năng trọng yếu của sản phẩm, hoặc thậm chí không thực hiện. Các lý do được đưa ra bao gồm sự thiếu hụt kỹ sư chuyên môn, chi phí vượt quá rủi ro tiềm ẩn, và trên hết là quan ngại việc phải chờ đợi nhiều tuần để mã nguồn được kiểm chứng hình thức sẽ làm chậm tốc độ đổi mới sáng tạo. Hồi đầu năm nay, nhóm an ninh của Apple cho biết một số vấn đề được kiểm chứng hình thức phát hiện trong thư viện mã hóa "corecrypto" của hãng là không thể tìm ra bằng phương pháp nào khác. Tuy nhiên, Apple cho biết thêm hãng buộc phải "thận trọng" khi bổ sung mã mới vào corecrypto nhằm bảo đảm năng lực rà soát bắt kịp tiến độ. Hai lãnh đạo an ninh mạng tại các doanh nghiệp lớn chưa từng áp dụng kiểm chứng hình thức cho biết họ chưa rõ liệu tự động hóa có đem lại hiệu quả tương xứng hay không. Dù vậy, các lãnh đạo này, do không được phép phát ngôn công khai, cho biết họ có thể cân nhắc việc chi trả cho các phòng nghiên cứu AI lớn để nhận về các đoạn mã do AI tạo ra đã được "kiểm chứng". Các nhà phát triển dự án phần mềm mã nguồn mở, vốn là nền tảng của nhiều ứng dụng, cũng đang tăng cường thử nghiệm phương pháp kiểm chứng có AI hỗ trợ. Tổ chức phi lợi nhuận Beneficial AI Foundation đã sử dụng một khoản tài trợ từ Anthropic để