Chúng ta vừa khám phá một cách mà một trí tuệ đơn lẻ có thể tự cải thiện theo thời gian, sử dụng formal verification để đảm bảo rằng tất cả các phiên bản sửa đổi vẫn nhất quán với các yêu cầu ban đầu. Tuy nhiên, chúng ta cũng có thể kỳ vọng rằng các hệ thống cải tiến hoạt động trong các hệ sinh thái cùng với những hệ thống khác, kết hợp giữa hợp tác và cạnh tranh, theo một phong cách liên quan đến các distributed systems trong ngành máy tính chính thống ngày nay. Tôi muốn đề xuất một vai trò khác cho formal verification trong bối cảnh đó, và tôi sẽ bắt đầu gợi mở nó bằng một ví dụ từ khoa học viễn tưởng.

Trong a famous scene của The Matrix, Neo được cắm cáp kết nối với máy tính và được “lập trình” kiến thức về kung fu. Ngay sau khi thức tỉnh, anh ấy đã sẵn sàng giao đấu hiệu quả (trong virtual reality) với sư phụ của mình. Ai trong chúng ta lại không thích ý tưởng đi tắt đón đầu cách học các kỹ năng mới thông thường chứ?

Cách tiếp cận học kỹ năng mới này thậm chí có thể đóng vai trò cốt lõi hơn đối với các AI agents trong tương lai, những tác tử có thể muốn “mượn” một ý tưởng từ vi khuẩn theo kiểu lateral gene transfer, nơi các cá thể đang hoạt động truyền “mã nguồn” (code) cho nhau. Kiểu hợp tác tìm kiếm này trong không gian của mã nguồn tốt có thể đóng vai trò quyết định trong việc tăng tốc mạnh mẽ tiến trình phát triển công nghệ.

Thật không may, khi đi vào lập kế hoạch chi tiết, chúng ta gặp phải một số trở ngại thực sự trong việc áp dụng. Chuyển giao các kỹ năng trong một môi trường nơi tất cả các tác tử tin tưởng lẫn nhau là một chuyện, nhưng nếu chúng ta muốn thực hiện các chuyển giao trong một cộng đồng toàn cầu (ngân hà?) thì sao? Làm thế nào chúng ta biết được rằng những nhà cung cấp kỹ năng mới luôn nghĩ cho lợi ích tốt nhất của chúng ta và không cố gắng ghi đè lên bộ não của chúng ta theo những cách mà chúng ta thực sự không mong muốn từ trước?

Hãy lùi lại một bước và suy nghĩ xem cách học truyền thống tránh được các rủi ro này như thế nào, xem xét các mối nguy hiểm mới của các giải pháp thay thế ảo được tối giản hóa (và mối liên hệ của chúng với các thách thức an ninh mạng đã được thiết lập sẵn), rồi thảo luận về cách formal verification có thể giúp ích.

Các con đường học tập

Tổ tiên hunter-gatherer của chúng ta đã học bằng cách quan sát những người đi trước thực hiện các công việc trong cuộc sống hàng ngày, trong khi chúng ta đã quen với việc ngồi trong lớp học để được hướng dẫn, nhưng đối với các mục đích của chúng ta, các luồng công việc này là như nhau: một số loại trải nghiệm giáo dục đã được thiết kế để giúp người xem học hỏi. Chúng ta có thể mô tả nó một cách đơn giản qua hình vẽ dưới đây.

Trải nghiệm giác quan cung cấp dữ liệu cho bộ não con người, bên trong đó các quyết định có thể được đưa ra về việc kiến thức có giá trị được cho là nào đáng tin cậy và đáng ghi nhớ. Yếu tố đó được nhân hóa thành “The Skeptic” (Người hoài nghi) trong hình vẽ. Các ý tưởng đã được kiểm chứng sẽ được chuyển cho “The Archivist” (Người lưu trữ), người sẽ lưu trữ kiến thức mới vào đúng nơi, trong một hệ thống kiến thức có tổ chức đã tồn tại sẵn, đặc thù cho từng cá nhân. Rõ ràng chúng ta không đi sâu đến mức chi tiết của neuroscience, nhưng phần giải thích sơ lược này là đủ để giúp chúng ta nghĩ về triển vọng và rủi ro của việc tải xuống các kỹ năng. Chúng ta cần một Skeptic có thể bác bỏ các kỹ năng không thực sự phù hợp với mục tiêu của chúng ta, và chúng ta cần một Archivist linh hoạt có thể tích hợp các kỹ năng vào khung tư duy của một tác tử. Sự phức tạp của cả hai nhiệm vụ này có thể giải thích cho việc con người mất nhiều thời gian để học các kỹ năng của người trưởng thành, và có lý do để hào hứng với việc tăng tốc đáng kể các giai đoạn này, mà không từ bỏ các mục đích của chúng.

Kiểm tra cryptographic signatures là một khởi đầu tốt, nhưng nó vẫn để ngỏ nhiều lỗ hổng cho các cuộc cryptographically signed to help guarantee that it comes from the source it claims to come from. Chúng ta bắt đầu với một Skeptic có sức mạnh vừa phải bên trong tác tử để kiểm tra kỹ năng, trong trường hợp này bằng cách kiểm tra cryptographic signature. (Chúng ta sẽ nâng cấp Skeptic của mình sau.) Các kỹ năng được chấp thuận sau đó được tích hợp vào các kiến trúc phần mềm lớn hơn bởi một Archivist.

Kiểm tra cryptographic signatures là một khởi đầu tốt, nhưng nó vẫn để ngỏ nhiều lỗ hổng cho các cuộc supply-chain attacks. Có thể đúng là kỹ năng đó đến từ tác tử mà chúng ta nghĩ, nhưng tác tử đó đang cố tình muốn phá hoại chúng ta. Hoặc nguồn gốc thực sự đó có thể đã bị xâm nhập bởi một kẻ tấn công nào đó, kẻ đã đưa vào một lỗ hổng nguy hiểm. Nguy hiểm nhất là, tất cả những người tham gia vào chuỗi cung ứng này đều có ý định tốt, nhưng ai đó đã vô tình tạo ra một lỗi (bug) mà vẫn mang lại những hậu quả thảm khốc – có lẽ chỉ biểu hiện trong những hoàn cảnh hiếm hoi trùng hợp với cách sử dụng của chính chúng ta. Các kỹ thuật chính thống cho supply-chain security hầu như có rất ít giải pháp cho rủi ro cuối cùng này, nhưng chúng ta sẽ đề cập đến một biện pháp bảo vệ thỏa đáng.

Hãy nhấn mạnh ngay những ưu điểm đáng kể của kiểu “học” này so với những gì chúng ta biết từ cuộc sống của chính mình. Một kỹ năng/mô-đun mới có thể được sao chép nguyên văn vào một hệ thống phần mềm lớn hơn. Thay vì tốn kém thời gian đầu tư vào giáo dục, chúng ta có thể chuyển đổi các phiên bản mới liên tục và ngay lập tức. Ngược lại với những gì có thể xảy ra trong quá trình học của con người, nơi một kỹ năng rõ ràng được mã hóa khác nhau trong mỗi bộ não, có lẽ rải rác khắp các ngóc ngách của trí nhớ, kỹ năng ở đây có thể được mã hóa thành một mô-đun riêng biệt, và việc lùi lại để hiểu cấu trúc của trí tuệ kỹ thuật số thông qua các bộ phận được tách biệt rõ ràng của nó vẫn khả thi. Sự tách biệt rõ ràng này rất hữu ích cho việc đảm bảo chất lượng của toàn bộ hệ thống.

Tuy nhiên, một kiến trúc sạch sẽ nhưng đầy rẫy các mô-đun độc hại sẽ không mang lại lợi ích gì cho chúng ta. May mắn thay, có rất nhiều tài liệu nghiên cứu trước đây từ thế giới của formal verification. Hãy cùng xem xét nó và cách nó có thể giúp các AI agents tái phát triển mã nguồn của chính chúng nhanh hơn nhiều so với thói quen của chúng ta.

Formal Verification và Chuỗi cung ứng phần mềm

Một số bộ phận trong thế giới nghiên cứu ngôn ngữ lập trình thường có xu hướng xem thường ngôn ngữ lập trình JavaScript và hệ sinh thái phần mềm web của nó, nhưng tôi muốn ghi nhận cách chia sẻ hợp lý các mô-đun phần mềm giữa các trang web của nó. Một ứng dụng web điển hình sẽ tích hợp nhiều libraries (các gói mã nguồn tái sử dụng được xuất bản riêng biệt) chỉ bằng cách liên kết tới chúng, tương tự như cách nó có thể bao gồm một liên kết có thể nhấp tới một trang web khác. Nghĩa là, thư viện được biểu diễn dưới dạng một URL để từ đó mã nguồn có thể được tải xuống. Các phương pháp bảo mật web tiêu chuẩn được sử dụng để xác nhận rằng một thư viện thực sự đến từ trang Internet mà chúng ta nghĩ, bao gồm cả việc sử dụng chữ ký kỹ thuật số trong HTTPS. Nếu lo lắng rằng các máy chủ lưu trữ sẽ lén lút tráo đổi các thư viện hợp pháp bằng các thư viện độc hại, chúng ta thậm chí có thể sử dụng một tiêu chuẩn web chưa được đánh giá đúng mức gọi là subresource integrity để liên kết các liên kết với các cryptographic hashes vốn có thể được sử dụng để kiểm tra xem chúng ta có tải về chính xác đoạn mã nguồn được dự định bởi tác giả của chương trình hay không.

Xác nhận việc tải xuống mã nguồn mà một người dùng Internet cụ thể muốn đưa cho chúng ta chắc chắn là một khởi đầu tuyệt vời, nhưng nếu người dùng đó độc hại hoặc chỉ đơn giản là kém năng lực thì sao? Khi đó chúng ta có thể nhận về một thư viện hoàn toàn không phù hợp với mục đích của mình. Rủi ro này không chỉ là mối quan tâm học thuật. Một trường hợp thế giới thực nổi tiếng là sự cố event-stream tai tiếng, được tài liệu hóa trong an academic paper. Tóm lại, một người duy trì mới đã tiếp quản một gói JavaScript phổ biến và lén đưa vào một lỗ hổng bảo mật mới vốn chỉ hiển thị trong các hoàn cảnh tương đối cụ thể liên quan đến bitcoin. Các tác giả bài báo lập luận rằng “các kỹ thuật phân tích chương trình thông thường có khả năng sẽ bỏ lỡ cuộc tấn công này”.

Tuy nhiên, các giải pháp cho vấn đề này cũng đã được biết đến, đặc biệt được phát triển từ khi Internet bùng nổ vào những năm 1990. Trong phần còn lại của bài viết này, tôi sẽ tập trung vào ý tưởng gọi là proof-carrying code, ý tưởng có một loạt các biến thể khác nhau rất thú vị. (Tôi cũng nên “công khai hoàn toàn” ở đây về thực tế là thuật ngữ này được giới thiệu trong luận án tiến sĩ của George Necula, người hướng dẫn tiến sĩ của chính tôi.)

Ý tưởng chính của proof-carrying code là gì? Về mặt lý thuyết, một tác tử thông minh nhận được một thư viện phần mềm có thể phân tích nó một cách triệt để để biết nó có thực hiện đúng những gì được mong đợi hay không. Thật không may, hầu hết các thuộc tính hành vi đáng quan tâm đều là undecidable đối với hầu hết các ngôn ngữ lập trình. Hơn nữa, rõ ràng là tác giả của thư viện hiểu rõ nó hơn người dùng thư viện đó, vì vậy sẽ là bỏ lỡ cơ hội nếu yêu cầu người dùng tự phân tích thư viện từ đầu mà không có sự hướng dẫn nào từ tác giả thư viện. Hình thức hướng dẫn tối thượng là gì? Đó sẽ là một chứng minh toán học rằng thư viện đáp ứng các yêu cầu cụ thể. Thuộc tính thiết yếu của bất kỳ ngôn ngữ chứng minh hình thức thực thụ nào là, mặc dù việc tìm kiếm các chứng minh có thể là không khả thi đối với nhiều bài toán đáng quan tâm, nhưng việc kiểm tra các chứng minh lại tương đối đơn giản, vì các chứng minh về cơ bản là các chuỗi sử dụng các quy tắc từ một tập từ vựng cố định, và thuật toán kiểm tra chỉ cần đi qua chuỗi đó và xác nhận mỗi quy tắc đã được sử dụng chính xác. Tôi cần nhấn mạnh rằng ở đây chúng ta không nói về các “chứng minh trên giấy” truyền thống đòi hỏi sự chú ý sát sao của con người để kiểm tra. Thay vào đó, chúng ta đang nói về các chứng minh được biểu diễn dưới dạng tệp máy tính, với cấu trúc được xác định cẩn thận để kiểm tra có thể dự đoán được.

Chúng ta thực sự gặp phải một số thách thức tương tự mà tôi đã giới thiệu khi suy đoán về recursive self-improvement: một chứng minh chỉ tốt bằng định lý mà nó chứng minh. Nếu thuộc tính hình thức được thiết lập là “sai”, nếu nó không phù hợp với mục đích không chính thức của chúng ta, thì việc viết chứng minh và kiểm tra chứng minh có thể phản tác dụng, tạo ra cảm giác an toàn giả tạo. Dưới đây là chuyến tham quan qua ba kiểu đặc tả (specification), mỗi kiểu đại diện cho một cách hiểu trong số nhiều cách trong lĩnh vực này về những gì chúng ta thực sự muốn nói khi nói về tính “an toàn” của một thư viện.

Functional correctness đặc tả rất chi tiết về việc, chẳng hạn, chính xác hàm toán học nào mà thư viện nên tính toán. Kiểu đặc tả này thường đòi hỏi nhiều công sức nhất, hầu như luôn yêu cầu công việc bổ sung đáng kể từ tác giả của thư viện. Một chứng minh thường rút ra từ các hiểu biết sâu sắc về mã nguồn vốn không hiển nhiên ngay cả với các lập trình viên khác.

Isolation (Sự cô lập) là các đặc tả cố gắng thực thi đơn thuần rằng một thư viện khớp vào sơ đồ khối của một hệ thống lớn hơn theo cách mong đợi, không can thiệp trực tiếp vào hoạt động của các thành phần khác. Một thuộc tính cô lập lâu đời là memory safety, thuộc tính này đại khái liên quan đến việc chứng minh rằng một mô-đun phần mềm chỉ truy cập vào các phần của bộ nhớ dùng chung mà chúng ta đã cấp tham chiếu một cách rõ ràng. Hầu hết các công trình ban đầu về proof-carrying code đều tập trung vào sự đảm bảo này, gắn liền với các ngôn ngữ memory-safe như Java. Một ngôn ngữ lập trình đang rất nổi tiếng hiện nay quảng bá tính năng memory safety là Rust, ngôn ngữ hỗ trợ các đảm bảo như vậy mặc dù cho phép tính linh hoạt tương đối cao để lập trình các thuật toán phức tạp và nhanh chóng (ít nhất là chừng nào lập trình viên tránh từ khóa unsafe, từ khóa thực sự nổi bật đối với người đọc). Lợi ích lớn của các ngôn ngữ an toàn là, trên thực tế, việc triển khai ngôn ngữ lập trình tự động hóa việc kiểm tra memory safety với mức độ nghiêm ngặt cao. Lập trình viên phải đưa thêm một số gợi ý trong mã nguồn, thường được diễn đạt dưới dạng một type system, nhưng những gợi ý này khi gộp lại có xu hướng ít dài dòng hơn nhiều so với các chứng minh toán học.

Side-Channel Security, thứ mà tôi đã giới thiệu trong bài viết trước, đối phó với thực tế là các hệ thống được triển khai không nhất thiết phải tuân thủ các ranh giới sạch sẽ mà chúng ta thấy trong các sơ đồ kiến trúc hệ thống. Đôi khi, một lỗ hổng bảo mật trong một thư viện biểu hiện ở cách thời gian tính toán làm rò rỉ bí mật. Tinh vi hơn, một đối thủ giám sát lượng bức xạ điện và từ của hệ thống có thể tìm hiểu được bí mật đó. Tôi đã đề cập đến một số công trình gần đây của mình chứng minh việc không có các timing side channels cho phần cứng (hardware) và phần mềm (compilers).

Các hệ thống xác minh nguyên mẫu phi vụn vặt đã được xây dựng xung quanh tất cả các phong cách này, nhưng hãy để tôi đề cập đến một thành phần quan trọng khác. Mặc dù JavaScript trên web chính là một phản ví dụ, nhưng thông thường các gói phần mềm được viết dưới dạng source code bằng ngôn ngữ thân thiện với con người và sau đó được chuyển đổi thành các định dạng như machine code hoặc bytecode bằng các compilers. Ngay cả khi một chương trình nguồn đã được chứng minh là đáp ứng một đặc tả, một lỗi compiler vẫn có thể tạo ra phiên bản cấp thấp hơn không còn tuân thủ nữa. Đó là lý do tại sao công trình ban đầu về proof-carrying code đã đưa ra phân loại gồm hai cách để thu hẹp khoảng cách niềm tin này.

Một certified compiler như CompCert được chứng minh hình thức là chính xác, loại bỏ rủi ro biên dịch sai (miscompilation). Ngược lại, một certifying compiler không chỉ dịch mã nguồn mà còn dịch cả chứng minh của nó, tạo ra một chứng minh mới áp dụng cho mã nguồn được tạo ra. Sự tương phản giữa chúng tương tự như một thử nghiệm tư duy có thể xảy ra khi thuê nhà thầu xây nhà cho bạn. Sự tương đương của một certified compiler là một công ty thầu đã trải qua quá trình chứng nhận rộng rãi, thuyết phục các chuyên gia rằng họ chỉ xây dựng những ngôi nhà hàng đầu. Sự tương đương của một certifying compiler là một công ty thầu bàn giao mỗi ngôi nhà mới cùng với các bản thiết kế và một tài liệu chứng minh để các chuyên gia có thể đọc và nhanh chóng tin tưởng rằng ngôi nhà được xây dựng tốt.

Các certifying compilers lần đầu tiên được nghiên cứu trong bối cảnh các type systems, nơi một cách tiếp cận chú trọng đến việc duy trì thông tin kiểu dữ liệu (type) từ các chương trình nguồn xuống tận ngôn ngữ assembly (hiện là typed assembly language). A program in that final language looks like one of the classic low-level languages of computer science, nhưng nó duy trì thông tin kiểu phân loại các phần của trạng thái máy với các loại giá trị mà chúng có thể chứa. Chương trình typed assembly có thể được kiểm tra tự động bằng một thuật toán tương đối đơn giản, không cần phải tin tưởng vào bất kỳ điều gì về chương trình nguồn hoặc compiler. Bản thân tôi cũng có một số công trình nghiên cứu liên quan gần đây trong bối cảnh cryptography và timing side channels.

Suy ngẫm về toàn bộ bộ kỹ thuật này, những gì nó bổ sung vào tư duy chính thống hiện nay về chuỗi cung ứng phần mềm là vượt ra ngoài việc chỉ xác nhận phần mềm đến từ nguồn dự kiến. Thay vào đó, chúng ta nhận được các đảm bảo toán học mạnh mẽ ngay cả khi không tin tưởng vào nguồn gốc của một gói phần mềm. Cũng có các lợi thế rõ ràng so với các kỹ thuật như chạy mã nguồn không đáng tin cậy trong các sandboxes, môi trường đặc biệt hạn chế tương tác với phần còn lại của hệ thống. Một mặt, việc chạy phần mềm đã được xác minh có thể rẻ hơn, không cần giám sát thời gian chạy (runtime monitoring). Mặt khác, sandboxing không thể thiết lập functional correctness (trong các trường hợp chúng ta muốn mức độ tin cậy đó đối với một mô-đun) và thông thường cũng không chặn được rò rỉ thông tin qua các side channels. Đúng là khi một sandbox phát hiện một chương trình hành xử sai, nó thường chỉ có thể tạm dừng chương trình, một bất ngờ không mấy dễ chịu mà chúng ta có thể tránh được bằng cách chứng minh trước rằng chương trình sẽ tự hành xử đúng mực.

Kết luận

Tương tự bài viết trước, thông điệp cấp cao nhất ở đây, hiện tại là về tiềm năng cho các tác tử không tin tưởng lẫn nhau trao đổi mã nguồn cùng với các chứng minh có thể kiểm tra được về tính an toàn của nó, là sự kết hợp giữa lạc quan (có một lượng lớn công trình nghiên cứu và các triển khai phi vụn vặt) và cảnh báo (việc chọn đặc tả đúng vẫn rất khó). Các động lực của việc Neo học kung fu trong The Matrix có thể không hoàn toàn đúng trong một thế giới coi trọng các ý tưởng này. Yêu cầu Neo cắm cáp kết nối với máy tính trong một thời gian dài để học kung fu mang lại giá trị đáng kể, nhưng chúng ta có lẽ có thể giúp anh ấy (hoặc ít nhất là một AI agent) tiếp thu tất cả chỉ trong tích tắc. Trong khoảnh khắc ngay sau khi anh ấy bừng tỉnh và trước khi nói “Tôi biết kung fu,” anh ấy nên chạy bộ kiểm tra chứng minh (proof checker) trước – điều này không làm gián đoạn hành động vì việc kiểm tra chứng minh sẽ diễn ra rất nhanh chóng.

Nói một cách nghiêm túc hơn, tôi muốn khẳng định rằng ý tưởng này là nhân tố quan trọng cho một thế giới nơi các AI agents thực thi một thuật toán phân tán để thúc đẩy công nghệ tiến lên phía trước. Các tác tử khác nhau có thể thử nghiệm các phương pháp khác nhau để tạo ý tưởng và sau đó bán các kết quả tốt nhất của họ cho những tác tử khác, ngay cả những đối thủ cạnh tranh vốn có lý do chính đáng để không tin tưởng họ. Kết quả là một thị trường toàn cầu cho việc tự cải thiện của tác tử, giữ lại các đặc điểm của nền kinh tế loài người chúng ta nhưng có khả năng vận hành với tốc độ cao hơn nhiều.

Một số công cụ kỹ thuật khác, blockchains và deep learning, cần được xem xét về vai trò của chúng trong nền kinh tế tương lai này, và tôi sẽ dành một vài bài viết tiếp theo để nói về chúng.