Bài viết này tóm tắt nội dung từ trước đến nay trong một khuôn khổ, điều này có thể mang lại cảm giác mạch lạc hơn so với việc đọc các bài viết riêng lẻ đang trôi qua nhanh chóng. Tất cả các siêu liên kết trong bài viết này đều dẫn đến các bài viết trước đó, vì vậy nó cũng đóng vai trò như một dạng mục lục. Tôi sẽ giảm bớt việc đưa ra minh chứng cho một số tuyên bố tôi đưa ra ở đây. Nếu bạn không bị thuyết phục bởi một câu nào đó, hãy theo dõi một số liên kết lân cận để biết thêm chi tiết.

Không có gì bàn cãi khi nói rằng, khi trí tuệ nhân tạo phát triển, các chi tiết tính toán bên dưới nó đóng vai trò cực kỳ quan trọng. Mục tiêu của tôi với blog này là suy nghĩ về các cân nhắc thiết kế từ một góc nhìn mới. Có hai khung lập luận chính (thesis statements) sẽ định hướng cho các chủ đề khác nhau mà chúng ta đề cập. Cả hai nghe có vẻ bình thường ở bề nổi, nhưng tôi sẽ đưa chúng đi xa hơn so với hầu hết các nhà bình luận khác.

Principle #1: mối quan hệ tác động qua lại hai chiều giữa tính chính xác (correctness) và hiệu quả (efficiency) (ví dụ: thời gian chạy và lượng điện năng tiêu thụ) nên là trung tâm trong việc thiết kế các hệ thống AI của tương lai. Tôi đang lập luận cho vai trò trung tâm của formal verification trong việc hỗ trợ tối ưu hóa các hệ thống một cách tham vọng hơn, khi các chi tiết tối ưu hóa vượt quá khả năng phân tích đáng tin cậy của con người. Bằng cách sử dụng các phương pháp kỹ thuật đảm bảo tính chính xác, các kỹ sư được khuyến khích thử nghiệm nhanh chóng hơn với các ý tưởng mới giúp cải thiện hiệu năng; và sau đó hiệu năng của các công cụ phục vụ suy luận hình thức trở thành động lực quan trọng thúc đẩy một vòng tuần hoàn tích cực.

Principle #2: chúng ta bỏ lỡ những cơ hội cải tiến quan trọng khi nhìn vào các hệ thống như hiện tại và giả định rằng các hệ thống tương lai sẽ có cùng loại thành phần với các yêu cầu cục bộ giống như hiện nay. Tôi sẽ lập luận cho những thay đổi đáng kể ở cả phần cứng máy tính và ngôn ngữ lập trình, nhưng tôi nghĩ sẽ là một sai lầm nếu dừng lại ở đó. Chúng ta có thể mở rộng phạm vi của các hệ thống mà chúng ta đang thiết kế sang những gì có thể tóm tắt tốt nhất hiện nay là "cấp độ xã hội". Các lĩnh vực như tâm lý học tiến hóa giúp chúng ta hiểu cách con người hoạt động ngày nay như một phần của các hệ thống đó, dẫn đến một số yêu cầu nhất định đối với các hệ thống máy tính vốn không phải là cơ bản và việc sửa đổi chúng có thể mang lại nhiều lợi ích.

Hãy cùng xem xét từng nguyên tắc chi tiết hơn.

Mối quan hệ tác động qua lại giữa Correctness và Efficiency

Nguyên tắc này sẽ giống như những kiểu thông thường mà các kỹ sư đề xuất với nhau, mà không đe dọa đến bản sắc nghề nghiệp nhiều như nguyên tắc tiếp theo!

Chúng ta có thể coi tất cả các tiến bộ khoa học và kỹ thuật như một distributed algorithm lớn, truyền thống được vận hành bởi con người nhưng AI đang ngày càng đảm nhận nhiều hơn quá trình hình thành ý tưởng. Quá trình tự tham chiếu của việc xây dựng các hệ thống AI hiệu năng cao là một ví dụ điển hình (và là điều tôi sẽ quay lại trong các bài viết sau), chẳng hạn như các đột phá về mặt thuật toán của các nhà nghiên cứu con người, kết hợp với việc dịch tự động (ví dụ: bằng các compilers) các đột phá đó thành mã cấp thấp. Ranh giới giữa đóng góp của con người và máy móc đã và đang thay đổi và có thể thay đổi mạnh mẽ hơn nữa, khiến việc xem xét rộng rãi hơn quá trình tìm kiếm và xác thực các ý tưởng trở nên hữu ích.

Trên thực tế, quá trình tiến hóa đã tạo ra bộ não của chúng ta để làm phần lớn công việc có thể được coi là chỉ một phần của cùng một bài toán tối ưu hóa liên tục. Thách thức lớn của một hệ thống tiến hóa là có được phản hồi đủ nhanh về chất lượng của các biến thể mới, cho dù chúng là các sinh vật hay các chương trình phần mềm mới. Hiện tượng signaling từ tâm lý học và kinh tế học có thể được coi là một mẹo khéo léo để nhận được phản hồi độ tin cậy cao sớm hơn về các cá thể, mặc dù có những điểm bất lợi tự nhiên đối với một thông lệ cố tình thể hiện một cách tốn kém. Một cách thay thế để đưa phản hồi độ tin cậy cao lên sớm hơn là formal verification, cho phép chúng ta đánh giá các biến thể dưới dạng chứng minh toán học về hành vi của chúng trong mọi tình huống có thể xảy ra.

Đôi khi sự thiếu tin tưởng vào việc tối ưu hóa hệ thống hoặc cải tiến khác cản trở chúng ta áp dụng nó. Cryptography có thể giúp chúng ta vượt qua một số vấn đề về lòng tin khi các ý tưởng và mã nguồn lan truyền rộng rãi. Tuy nhiên, tôi tập trung nhiều hơn vào formal verification như một nhân tố quan trọng cho phép áp dụng các ý tưởng, ngay cả khi chúng ta tự nghĩ ra chúng nhưng đặc biệt là khi chúng đến từ những người khác mà chúng ta có lý do để không tin tưởng.

Trong nhóm đầu tiên, hãy xem xét ví dụ về một recursively self-improving, highly parallel compiler. Nó liên tục phát minh ra các mẹo mới để giúp bản thân chạy nhanh hơn và do đó có thể tạo ra các chương trình tốt hơn trong một khoảng thời gian giới hạn cho trước, nhưng làm thế nào chúng ta biết được nó không tự sửa đổi theo cách biên dịch tất cả các chương trình thành các tác nhân "tiêu diệt toàn bộ loài người"? Chúng ta hoàn toàn có thể chứng minh rằng một quá trình như vậy vẫn duy trì được mục đích ban đầu của compiler, qua bất kỳ số vòng cải tiến nào.

Trong nhóm thứ hai, hãy xem xét ví dụ về các tác nhân AI không tin tưởng lẫn nhau chia sẻ thư viện mã nguồn với nhau. Mô hình proof-carrying code giúp việc phân phối mã nguồn đi kèm với các chứng minh về mức độ phù hợp với mục đích, tính bảo mật, v.v. trở nên khả thi. Các tác nhân AI có thể áp dụng các "brain modules" mới nhanh chóng và tự tin hơn nhiều so với con người, nhờ cơ hội kiểm tra chúng ngay lập tức với các tiêu chuẩn khắt khe nhất, điều này có khả năng là một động lực thúc đẩy quan trọng cho sự tiến bộ tăng tốc trong khoa học và kỹ thuật.

Đôi khi hiệu năng kém của formal verification giới hạn những lợi ích mà chúng ta có thể đạt được như tôi vừa phác thảo. Ví dụ, hầu hết các dự án nghiên cứu của sinh viên mà tôi hướng dẫn tại MIT đều bị nghẽn ở hiệu năng của các automated-theorem-proving tools. Đã có một nỗ lực full-stack thành công, từ phần cứng đến các công cụ lập trình phần mềm, để hỗ trợ việc tính toán machine-learning dựa trên đại số tuyến tính. Formal verification cũng xứng đáng nhận được nỗ lực tương tự, và mọi cấp độ của stack có lẽ sẽ trông khác biệt một cách thú vị so với GPUs và CUDA. Cho đến nay tôi đã viết rất ít về các chi tiết cụ thể mà mình dự định, nhưng hãy chờ đón nhiều bài viết sắp tới.

Tầm quan trọng của Thiết kế Toàn diện (Holistic Design)

Các kỹ sư đều sẽ đồng ý rằng đôi khi việc tập trung vào một phần của hệ thống hiện có không để lại đủ số bậc tự do (degrees of freedom) để đáp ứng một số mục tiêu cải tiến. Đề xuất của tôi về việc triển khai lại hardware-software stack để tăng tốc formal verification phù hợp với truyền thống đó, ngay cả khi nó vẫn còn mang tính suy đoán và do đó việc hoài nghi là hoàn toàn hợp lý. Và tôi sẽ có rất nhiều thứ để viết về các chi tiết ở cấp độ này, say mê nghiên cứu về hardware-software codesign. Tuy nhiên, mang tính gây tranh cãi hơn, tôi muốn lập luận rằng chúng ta có thể đạt được nhiều cải tiến hơn nữa bằng cách mở rộng phạm vi hệ thống mà chúng ta xem xét.

Dưới đây là một số ví dụ đã được đề cập trong các bài viết chi tiết cho đến nay, đi lên theo một nấc thang trừu tượng hóa từ thế giới vật lý đến nhận thức rộng lớn hơn.

• Việc kiểm soát xe tự lái (self-driving vehicles) dường như liên quan đến các vấn đề phức tạp về computer vision và nhiều thứ khác. Tuy nhiên, chúng ta có thể tránh được những vấn đề đó bằng cách thay đổi môi trường vật lý sao cho các phương tiện tự hành có làn đường dành riêng cho mình với cấu trúc hình học được cố tình thiết kế đơn giản hơn.

• Natural-language processing dường như là nền tảng cho nhiều ứng dụng hấp dẫn của AI. Tuy nhiên, một tương lai của các tác nhân AI có thể dựa trên các ngôn ngữ tổng hợp (synthetic languages) dễ xử lý hơn nhiều.

• Các AI coding assistants giải quyết các bài toán khó trong việc áp dụng các ngôn ngữ lập trình phổ biến hiện nay để giải quyết các thách thức lập trình mới. Tuy nhiên, chúng ta có thể làm cho bài toán dễ dàng hơn nhiều bằng cách thay đổi chính các ngôn ngữ lập trình. (Tôi sẽ viết nhiều hơn nữa trong các bài đăng tương lai về "cách thức đúng đắn" để tự động hóa cả lập trình phần mềm và thiết kế phần cứng kỹ thuật số, nhằm mang lại các đảm bảo tính chính xác mạnh mẽ.)

Khi chúng ta đi lên nấc thang cao hơn, tâm lý học tiến hóa bắt đầu trở nên hữu ích hơn để hiểu nguồn gốc của các thách thức AI mà chúng ta đã quen thuộc. Natural language là một ví dụ đặc biệt phức tạp mà sự tiến hóa đã định hình để nó khó một cách có chủ đích do việc sử dụng nó trong signaling; chúng ta không cần phải chọn các engineering abstractions khó một cách cố ý! Một chủ đề mà chúng ta sẽ quay lại trong nhiều bài viết sau là làm thế nào chúng ta có thể tận dụng một cái nhìn khách quan về nhận thức của chính mình và nguồn gốc của nó để phát hiện các cơ hội đơn giản hóa trí tuệ thông qua những thay đổi lớn hơn đối với cách thế giới vận hành.

Tôi cũng đã dành nhiều bài đăng để thảo luận về cách một phương pháp tiếp cận thiết kế toàn diện (holistic-design) làm lộ ra các điểm yếu của deep learning, kỹ thuật AI phổ biến nhất ngày nay. Những thành công của nó dựa trên khả năng tìm kiếm và kết hợp các tri thức đã có (prior art), để giải quyết các bài toán mới bằng cách tham khảo các tập dữ liệu huấn luyện khổng lồ gồm các giải pháp trước đó. Tuy nhiên, nó có những điểm yếu lớn ở cả hai khía cạnh hệ thống mà tôi đã nhấn mạnh ở trên. Các vấn đề về correctness đã quá nổi tiếng, do tính không thể lý giải của các mô hình đã học và do đó dẫn đến rủi ro rằng chúng sẽ đưa ra các quyết định đi ngược lại mong muốn của chúng ta. Vấn đề về efficiency nằm ngay trong từ "deep" (sâu), biểu thị một cấu trúc tính toán bắt buộc dẫn đến sự chậm trễ lớn trong việc phản hồi các prompt, nhân lên gấp bội khi các tầng chức năng bổ sung được thêm vào (bất chấp những nỗ lực cường độ cao nhằm tối ưu hóa toàn bộ stack từ thuật toán đến phần cứng, những nỗ lực vốn mang lại nhiều kết quả cho throughput hơn là latency). Tôi sẽ đề xuất một hoặc hai phương pháp tiếp cận mới để giải quyết cả hai vấn đề này, sử dụng mô hình symbolic mode of AI vốn đã không còn hợp thời (đôi khi hợp tác với deep learning), trong một lớp áo hiện đại rõ ràng nhất của nó là formal verification.

Nhưng chẳng phải phong cách đó đã bị mất uy tín, với việc deep learning đánh bại nó hoàn toàn trong nhiều lĩnh vực quan trọng hay sao? Tôi lập luận rằng các bài toán AI khó nhất phần lớn lại giống với những bài toán tôi đã liệt kê ở trên, nơi chúng ta có những con đường để tránh chúng thông qua thiết kế hệ thống toàn diện hơn. Ở đó nguyên tắc là chúng ta nên tái cấu trúc thế giới để tăng tính dễ hiểu (legibility) đối với các công nghệ trí tuệ có các đặc tính tốt. Một số phản ứng bác bỏ sẽ đến từ bản chất con người, khi những người trong ngành công nghiệp công nghệ và những nơi khác không muốn từ bỏ các bài toán khó và giải pháp đắt đỏ vốn rất hữu ích để thể hiện năng lực và sự giàu có. Tuy nhiên, việc vượt qua những động lực lệch lạc (perverse incentives) đó là rất xứng đáng để thúc đẩy các hệ thống chi phí thấp hơn mang lại các câu trả lời đáng tin cậy hơn.

Các Bước Tiếp Theo

Loạt bài viết tiếp theo của tôi sẽ đề cập đến thành phần trung tâm là specifications dành cho formal verification. Sẽ không giúp ích gì nhiều nếu chứng minh rằng một hệ thống tuân theo một specification mà không bao quát được các mục tiêu thực tế của chúng ta. Tôi sẽ xem xét một số ví dụ về formal verification ngày nay, xen kẽ với các kịch bản có vẻ giống như khoa học viễn tưởng ở thời điểm hiện tại nhưng có thể xuất hiện trước khi chúng ta kịp nhận ra.

Nói cách cách: Mức độ khai sáng đầu tiên là nhận ra tiềm năng của formal verification trong việc hỗ trợ phát triển nhanh chóng các hệ thống phức tạp sao cho chúng đạt được tính chính xác ngay từ khi xây dựng (correct by construction). Mức độ khai sáng thứ hai (mà các tên tuổi lớn trong ngành formal verification đã nhận ra và viết về trong nhiều thập kỷ) là nhận thấy rằng các hệ thống phải được chứng minh dựa trên các specifications, và công việc thiết kế specifications thì không hiển nhiên dễ quản lý hơn so với bản thân các sản phẩm mà chúng áp dụng vào. Mức độ khai sáng thứ ba là nhận ra bộ kỹ thuật giúp việc tránh các sai sót specification nguy hiểm trở nên dễ dàng hơn chúng ta nghĩ, như tôi sẽ giải thích trong các bài viết sắp tới.

Sau đó, chúng ta có thể quay lại xem xét cách khai thác thêm tính song song (parallelism) trong tính toán có thể là một trong những hoạt động quan trọng nhất cho tương lai của sự sống thông minh trong vũ trụ, thúc đẩy một vòng tuần hoàn tích cực của việc cải thiện trí tuệ được đảm bảo bằng các chứng minh hình thức (formally assured intelligence) có thể tự cải tiến chính nó.