Nhà nghiên cứu Chuyue Sun của Stanford và các nhà khoa học máy tính đồng nghiệp của cô đã phát triển một công cụ AI giúp hoàn thành một dự án kỹ thuật trong vòng chưa đầy nửa ngày với chi phí dưới 500 USD, so với 5 tháng mà ba chuyên gia có tay nghề cao phải mất để thực hiện cùng một công việc theo cách thủ công. Việc giảm đáng kể thời gian và chi phí, như Sun đã báo cáo trong một bài báo gần đây, là một trong những kết quả ban đầu đang đánh thức một lĩnh vực ít người biết đến về mã hóa và toán học được gọi là xác minh hình thức.

Trong nhiều thập kỷ, các nhà phát triển đã hình dung ra việc sử dụng toán học để chứng minh rằng phần mềm của họ không có lỗi. Quá trình này kéo dài và tốn nhiều công sức, đòi hỏi các kỹ sư phải viết các tuyên bố chính xác về mục tiêu của phần mềm và chuyển mã của họ thành các công thức có thể được xác thực. Mặc dù các công ty đã tiến hành các thử nghiệm phức tạp để xác định càng nhiều lỗ hổng trong phần mềm của họ càng tốt, nhưng họ hiếm khi bỏ ra chi phí để xác minh chính thức, điều này có thể phát hiện ra những hành vi thậm chí còn thất thường hơn.

Giờ đây, một làn sóng các công ty khởi nghiệp đang đặt cược rằng AI sáng tạo sẽ khiến việc xác minh phần mềm chính thức trở nên thiết thực và cần thiết. Trong số đó có &Truth, Sun đã tham gia vào tháng 8 và ra mắt công khai vào thứ Năm. Nghiên cứu của Sun đã chứng minh tiềm năng của công nghệ bằng cách sử dụng AI để xác minh một phần mã hóa các cuộc hội thoại trong ứng dụng nhắn tin Signal.

Ilya Sergey, giám đốc khoa học của &Truth cho biết: “Những cây cầu, tòa nhà không sụp đổ vì người ta đã tính toán trước khi xây dựng chúng”. "Tại sao chúng ta không làm điều tương tự đối với mã? Công nghệ lý luận toán học đều có sẵn, chỉ 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 cuối cùng là xác minh bất kỳ ngôn ngữ lập trình nào. Rival Harmonic, được đồng sáng lập bởi Giám đốc điều hành Robinhood Vlad Tenev và đã nhận được 295 triệu đô la tài trợ, đã công bố trong tuần này rằng tác nhân AI tập trung vào toán học Aristotle hỗ trợ xác minh phần mềm được viết bằng C và thiết kế phần cứng bằng Verilog. Họ đang đánh giá công nghệ này với những người dùng tiềm năng, bao gồm các nhà sản xuất chip Tensordyne và Nvidia, công ty có quỹ đầu tư mạo hiểm là một trong những nhà đầu tư của công ty khởi nghiệp.

Và chỉ tuần trước, Anthropic và công ty khởi nghiệp xác minh Theorem đã cùng tuyên bố rằng họ đã sử dụng AI để hỗ trợ tìm ra lỗi trong phần mềm nguồn mở mà hàng nghìn tỷ bài kiểm tra đã không phát hiện ra. Họ cũng giới thiệu một tiện ích bổ sung dành cho Claude để giúp các nhà phát triển khác xác minh. Chi phí của dự án ban đầu không được tiết lộ.

Lời hứa lớn là một tương lai nơi phần mềm chạy đáng tin cậy hơn với ít vấn đề đau đầu về bảo mật hơn. Nhưng liệu AI có thể mang lại khả năng xác minh chính thức vượt ra ngoài các hệ thống quan trọng nhất tại các tổ chức như NASA và Apple và được sử dụng rộng rãi hay không vẫn là một câu hỏi mở.

Công nghệ này vẫn đang trong giai đoạn tạo mẫu. Mặc dù nhu cầu cao nhưng vẫn chưa rõ khách hàng sẵn sàng trả bao nhiêu và họ thích áp dụng công nghệ như thế nào. Xác minh chính thức dựa 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 nghi ngờ về khả năng phát hiện lỗi xuất phát từ lỗi người dùng và sự cố phần cứng.

Will Wilson, người điều hành công ty khởi nghiệp phần mềm AI săn lỗi Antithesis, gọi việc xác minh chính thức là “một cái bẫy” đối với những người đam mê toán học như anh. Antithesis đã chi hàng triệu đô la để chính thức xác minh một số biện pháp bảo vệ an ninh mạng của mình, một quá trình mà Wilson mô tả là “một điều khó chịu”. Tuy nhiên, công ty khởi nghiệp này vẫn phát hiện ra các lỗi bổ sung khi sử dụng công cụ của riêng mình và Antithesis cũng đã tìm thấy các lỗi trong phần mềm mà một số khách hàng của họ đã chính thức xác minh. Wilson nói: “Nó có thể mang lại cho bạn một số sự đảm bảo, nhưng chỉ có thử nghiệm toàn diện mạnh mẽ mới có thể chứng minh sự đảm bảo của bạn là đúng”.

Hay như Vitalik Buterin, kỹ sư nổi tiếng với việc tạo ra tiền điện tử Ethereum, đã viết trong một bài đăng trên blog vào đầu năm nay, “xác minh chính thức không phải là thuốc chữa bách bệnh”. Nhưng ông và những người ủng hộ phương pháp này vẫn tin rằng đây sẽ là một biện pháp phòng thủ quan trọng chống lại các hệ thống AI phát động các cuộc tấn công mạng và tàn phá.

Bảo mật cốt lõi

Theo tiết lộ của 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 có chứa ít nhất một số phần mềm đã được xác minh chính thức. Mã được đề cập thường liên quan đến bảo mật và các lỗ hổng trong đó có thể gây ra tác hại nghiêm trọng nếu bị khai thác.

Byron Cook, một nhà khoa học nổi tiếng và phó chủ tịch của Amazon Web Services, cho biết việc xác minh chính thức đã làm giảm bớt những 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ộ phát triển nhanh hơn bằng cách xử lý sớm các lỗi lớn.

Tuy nhiên, một số công ty công nghệ cỡ trung bình nói với WIRED rằng họ thường chỉ xác minh một tính năng chính của sản phẩm, nếu có. Họ trích dẫn việc thiếu kỹ sư xác minh, chi phí vượt quá rủi ro tiềm ẩn và có lẽ quan trọng nhất là lo ngại rằng việc chờ đợi hàng tuần để mã được xác minh chính thức có thể làm chậm sự đổi mới.

Đầu năm nay, nhóm bảo mật của Apple cho biết một số vấn đề được xác minh chính thức được phát hiện trong thư viện “corecrypto”, được sử dụng để mã hóa, không thể được tìm thấy bằng cách nào khác. Nhưng công ty nói thêm rằng họ phải “thận trọng” khi thêm mã mới vào corecrypto để đảm bảo có thể theo kịp quá trình xem xét nó.

Hai giám đốc điều hành an ninh mạng tại các công ty lớn chưa chính thức xác minh bất kỳ mã nào cho biết họ không chắc liệu tự động hóa có mang lại giá trị hay không. Nhưng các giám đốc điều hành, những người không được phép phát biểu công khai, nói rằng họ có thể tưởng tượng việc trả tiền cho các phòng thí nghiệm AI lớn để có được mã do AI tạo ra “đã được xác minh”.

Các nhà phát triển dự án phần mềm nguồn mở, vốn là nền tảng của nhiều ứng dụng, đang ngày càng thử nghiệm xác minh với sự hỗ trợ của AI. Năm nay, Tổ chức AI có lợi phi lợi nhuận đã sử dụng khoản trợ cấp từ Anthropic để xác thực mã mã hóa tương tự như Sun đã làm tại Stanford trong năm nay. Michael Rosenberg, người duy trì thư viện có tên là Curve25519-dalek, hy vọng nguồn tài trợ bền vững sẽ xuất hiện cho những nỗ lực xác minh đang diễn ra. “Tuy nhiên, tôi không biết điều đó sẽ xảy ra như thế nào và chúng tôi chắc chắn không nên dựa vào thiện chí của các công ty AI,” ông nói.

Một số công ty khởi nghiệp mong muốn mở rộng xác minh cũng không chắc chắn nên triển khai công cụ của họ trực tiếp cho khách hàng hay thông qua các bên trung gian như Anthropic. Kế hoạch chung của họ là sử dụng AI để tự động hóa phần lớn công việc liên quan đến việc xác định cách thức hoạt động của một chương trình. Ví dụ: các thông số kỹ thuật cho một bảng dữ liệu có thể yêu cầu nó phải chứa các mục giống nhau trước và sau khi sắp xếp, chỉ là theo một thứ tự khác. Những nỗ lực tự động hóa hơn nữa, có thể không liên quan đến AI, sẽ dịch mã đó sang định dạng mà các công cụ toán học như Lean, Rocq và Isabelle có thể sử dụng để kiểm tra xem mã có hoạt động như dự định hay không.

Một người mới tham gia lĩnh vực xác minh chính thức khác gần đây là Madan Musuvathi, người đã rời Microsoft Research sau hơn 20 năm để thành lập công ty khởi nghiệp Truidic. Sau những sự cố như vụ hack OpenAI của Hugging Face, anh cảm thấy cần phải thương mại hóa nghiên cứu của mình một cách cấp thiết. Musuvathi nói: “AI trong tay kẻ tấn công có thể cực kỳ mạnh mẽ, nhưng việc xác minh có thể “làm cho AI trở nên an toàn và bảo mật cho mọi người, ở mọi nơi”.

Proofcraft, một trong số ít các công ty từ lâu đã cung cấp dịch vụ xác minh truyền thống, cho biết sự phấn khích ngày càng tăng về quy trình này đang chuyển thành một loạt câu hỏi từ các khách hàng tiềm năng. June Andronick, Giám đốc điều hành của công ty và Gerwin Klein, nhà khoa học trưởng của công ty, cho biết sự quan tâm dễ dàng vượt xa những gì họ và đối thủ cạnh tranh của họ có thể cung cấp.

Nhưng cả hai đều lo lắng rằng các thông số kỹ thuật do AI tạo ra có thể tạo ra “sự tin tưởng vô căn cứ” vào kết quả. Người xác minh cũng mong muốn duy trì niềm vui mà công việc mang lại cho họ. Klein gọi nó là “khá gây nghiện, giống như một trò chơi giải đố”. Nếu mọi việc suôn sẻ, anh ấy sẽ giải quyết được nhiều việc hơn bao giờ hết.

Bình luận

Quay lại đầu trang