Phát triển phần mềm đa tác nhân thực chất là bài toán hệ thống phân tán

Phát triển phần mềm đa tác nhân thực chất là bài toán hệ thống phân tán (AGI không thể cứu bạn khỏi điều này)

Gần đây, tôi đã dành nhiều thời gian suy nghĩ về các khung sườn (scaffolding) và ngôn ngữ để quản lý hệ thống các LLM phối hợp với nhau — các ngôn ngữ lập trình mới có thể là giải pháp lý tưởng cho lĩnh vực này. Chúng tôi đang phát triển một bài báo thú vị về một ngôn ngữ biên đạo (choreographic language) dùng để mô tả quy trình làm việc đa tác nhân. Thật thú vị khi các biên đạo, dù quá yếu để áp dụng cho bất kỳ giao thức phân tán thực tế nào, lại là một hình thức toán học ngắn gọn và thanh lịch để mô tả các tương tác riêng biệt phát sinh giữa các tác nhân, đặc biệt là khi kết hợp với lý thuyết trò chơi. Hãy chú ý theo dõi, chúng tôi sẽ chia sẻ nó sớm!

Tuy nhiên, có một phản hồi khá khó chịu mà tôi thường xuyên nghe thấy, thậm chí từ các nhà nghiên cứu khác, đó là sự thờ ơ đối với tình hình hiện tại và mục tiêu phát triển các hình thức toán học cũng như ngôn ngữ để quản lý các tác nhân. Lời than thở phổ biến nhất có thể tóm tắt như sau:

"Giải pháp tốt nhất cho việc phối hợp tác nhân là chỉ cần đợi thêm vài tháng."

Lập luận này大致 tóm lại là:

• Các hệ thống LLM đa tác nhân hiện tại không thể tự động xây dựng phần mềm quy mô lớn (đồng ý ✅).
• Vấn đề cốt lõi nằm ở sự phối hợp (đồng ý ✅).
• Thế hệ mô hình tiếp theo sẽ thông minh hơn (đồng ý ✅).
• Thế hệ mô hình tiếp theo sẽ không gặp vấn đề về phối hợp (⁇ HỎI RỒI ⁇).

Hệ quả chính là việc xây dựng các ngôn ngữ và công cụ để mô tả và quản lý các hệ thống này là một nhiệm vụ vô vọng (như đẩy đá lên dốc Sisyphus); các mô hình mới hơn sẽ khiến chúng lỗi thời, và toàn bộ nỗ lực sẽ đổ sông đổ biển.

Là một nhà nghiên cứu về xác minh, tôi thấy sự đầu hàng này hơi sớm và sai lầm: có một kho tàng literature về hệ thống phân tán, nói chính xác về vấn đề này, mà mọi người đang phớt lờ, cùng với một số kết quả bất khả thi bất biến đối với khả năng của mô hình. Ngay cả khi các mô hình tiếp theo là AGI (cười), vấn đề phối hợp vẫn là một vấn đề cơ bản, và các tác nhân thông minh hơn một mình không thể thoát khỏi nó.

Trong bài đăng này, tôi muốn làm rõ ý tưởng này, phân tích bài toán phát triển phần mềm đa tác nhân thành một mô hình hình thức và thiết lập một số kết nối với các kết quả bất khả thi tiêu chuẩn về hệ thống phân tán. Đồng thuận phân tán là khó, bất kể những người tham gia có "AGI" đến đâu.

Mô hình hình thức của phát triển phần mềm

"Claude. Hãy làm cho tôi một ứng dụng để theo dõi công thức nấu ăn. Đừng mắc lỗi."

Chúng ta có thể mô hình hóa bài toán tổng hợp phần mềm đa tác nhân một cách hình thức như sau: Cho một lời nhắc (prompt) (P :=) "(\textit{Một ứng dụng để theo dõi công thức nấu ăn})", chúng ta có thể định nghĩa công thức (\Phi(P)) là tập hợp các phần mềm nhất quán với lời nhắc đó: [ \Phi(P) := { \phi | \phi ~\text{program} ∧ \phi ~\text{là nhất quán với lời nhắc}~P } ]

Điểm mấu chốt ở đây là một lời nhắc ngôn ngữ tự nhiên, theo bản chất của nó, là chưa được xác định đầy đủ (underspecified) — tức là có thể có nhiều chương trình nhất quán với lời nhắc đó. Khi chúng ta sử dụng LLM để xây dựng và viết hệ thống phần mềm, chúng ta thực chất đang yêu cầu LLM chọn một phần tử trong số nhiều phần tử từ tập hợp này.

Ngược lại, khi chúng ta thực hiện phát triển phần mềm đa tác nhân, tức là chúng ta khởi chạy một số tác nhân, (A_1, ⋯, A_n), và yêu cầu họ xây dựng một phần mềm, chúng ta thực chất đang yêu cầu mỗi tác nhân tạo ra các thành phần phần mềm (\phi_1, ⋯, \phi_n) sao cho tất cả chúng đều cụ thể hóa một cách giải thích nhất quán duy nhất của lời nhắc: [ C(\phi_1, \cdots, \phi_n) := \exists \phi \in \Phi(P), \forall i, \phi_i \text{cụ thể hóa} \phi ]

Nói cách khác, đây không gì khác hơn là một bài toán đồng thuận phân tán lớn.

Sự phối hợp giữa các tác nhân

Nói một cách khác, lời nhắc (P) của người dùng trước tiên được chia nhỏ, thông qua một kế hoạch, thành các nhiệm vụ cho một số tác nhân (a_1, ⋯, a_n). Sau đó, các tác nhân này làm việc song song để triển khai các nhiệm vụ mã hóa tương ứng của họ (\phi_1, ⋯, \phi_n), và vào cuối, nếu quá trình tổng hợp thành công, chúng ta hy vọng rằng hệ thống phần mềm được tạo cuối cùng (\phi) được tạo thành từ từng cấu trúc riêng lẻ (\phi := \phi_1 || \cdots || \phi_n), sẽ thỏa mãn yêu cầu của người dùng.

Về bản chất, đây là một bài toán đồng thuận vì các tác nhân (a_1,\cdots,a_n) phải làm việc đồng thời để tạo ra các tạo tác phần mềm (\phi_1,\cdots,\phi_n), nhưng phải giao tiếp và đồng ý đủ để phần mềm cuối cùng (\phi_1 || \cdots || \phi_n) được hình thành tốt và thỏa mãn yêu cầu. Các quyết định thiết kế hoặc lựa chọn trong một (\phi_i) sẽ dẫn đến các ràng buộc ảnh hưởng và tác động đến các lựa chọn có thể có của (\phi_j) cho các tác nhân khác. Ví dụ, nếu tác nhân chịu trách nhiệm triển khai kết nối mạng (a_{\text{network}}) chọn một thư viện với API bất đồng bộ kiểu callback cho các yêu cầu, thì bất kỳ tác nhân nào chịu trách nhiệm cho việc tích hợp tổng thể (a_{\text{integration}}) phải tổ chức cơ sở hạ tầng xung quanh lựa chọn đó, v.v. Các lựa chọn tương tự trong các mô-đun khác sẽ ảnh hưởng đến không gian thiết kế của các tác nhân khác và nói chung quá trình diễn ra như một bài toán tổng hợp chung.

Đây có thực sự là bài toán Đồng thuận Phân tán không?

Khi chúng ta hoàn thành mô hình hình thức của phát triển phần mềm tác nhân, tại thời điểm này, tôi cũng muốn dành một chút thời gian để bác bỏ một số phản đối rõ ràng.

Tại sao (P) lại chưa được xác định đầy đủ (tức là tại sao (|\Phi(P)| \neq 1))? Điều này đúng theo bản chất ngôn ngữ tự nhiên là mơ hồ. Thực tế là chúng ta có một cách để đưa ra các thông số kỹ thuật chính xác và không mơ hồ cho phần mềm. Đó được gọi là ngôn ngữ lập trình. Bất cứ thứ gì khác đều để lại chỗ cho tác nhân đưa ra quyết định thiết kế. Một cách nhìn nhận khác là chúng ta có thể dành thời gian để tinh chỉnh lời nhắc ban đầu để làm cho nó ít mơ hồ hơn, nhưng trừ khi chúng ta đi hết đường đến mã (lúc đó, bạn không sử dụng nhiều tác nhân, chỉ có một), sẽ có một mức độ mơ hồ nhất định trong lời nhắc của chúng ta.

Bài toán có vốn dĩ là đồng thời (concurrent) không? Động lực để sử dụng nhiều tác nhân cho một hệ thống phần mềm nằm ngoài phạm vi của bài đăng này, nhưng ngay khi chúng ta đưa ra quyết định đó và có nhiều tác nhân làm việc trên các nhiệm vụ của mình, bài toán vốn dĩ là đồng thời (bất kể họ có làm việc song song hay xen kẽ trên một luồng duy nhất), và chúng ta phải giải quyết các vấn đề về phối hợp.

Tại sao không có một giám sát viên duy nhất để quy định các lựa chọn? Tại sao không để các tác nhân đưa ra đề xuất song song và sau đó có một loại giám sát viên nào đó quản lý việc hợp nhất PR vào cơ sở mã chung? Thử hay đấy! Kho git là một cách tiếp cận khá tiêu chuẩn để cố gắng phối hợp phát triển phần mềm song song, nhưng bạn chưa giải quyết được bài toán đồng thời cơ bản; tốt nhất bạn đã tự mã hóa mình vào một lựa chọn đồng thời duy nhất, và không phải là một lựa chọn tốt lắm: khi một quyết định thiết kế được chọn và hợp nhất vào cơ sở mã, điều gì sẽ xảy ra với công việc phải được rebase? Nếu nó có xung đột thì sao? Một số công việc phải bị mất.

Điểm chính tôi muốn truyền đạt ở đây không phải là bạn không thể đôi khi thực hiện phát triển phần mềm đa tác nhân trong khi bỏ qua bài toán đồng thời — rõ ràng mọi người đã đạt được một số thành công trong phát triển phần mềm với các tác nhân mà không cần kéo ra thuật toán Paxos — mà quan điểm này giúp chúng ta dự đoán trước cách chúng ta đang giải quyết các bài toán đồng thời cơ bản này với các quy trình phối hợp của mình. Bây giờ, nếu bạn mời tôi đi uống vài ly, có lẽ tôi sẽ đi xa hơn để nói rằng nếu chúng ta muốn phát triển phần mềm đa tác nhân thực sự mở rộng quy mô, thì các câu hỏi này phải được suy nghĩ và trả lời cẩn thận.

Các kết quả bất khả thi cho phát triển phần mềm đa tác nhân

Bây giờ chúng ta đã có mô hình hình thức này của phát triển phần mềm tác nhân, đã đến lúc phần "trả thưởng" của bài đăng blog này! Hãy vẽ một số kết nối với hệ thống phân tán và phác thảo một số kết quả bất khả thi.

FLP cho hệ thống đa tác nhân (Safety, Liveness, Fault Tolerance, chọn hai)

Tất nhiên, chúng ta có thể bắt đầu từ đâu khác ngoài FLP, ôi FLP thân yêu. Bài báo mang tính bước ngoặt của Fischer, Lynch và Paterson "Sự bất khả thi của Đồng thuận Phân tán với Một Quy trình Lỗi" thiết lập một kết quả bất khả thi cơ bản quy định đồng thuận trong bất kỳ hệ thống phân tán bất đồng bộ nào (đúng! bao gồm cả chúng ta).

Định lý FLP (Fischer et al., 1985): Trong bất kỳ hệ thống phân tán nào có độ trễ tin nhắn tùy ý và khả năng xảy ra ít nhất một lỗi crash (sập) của nút, không có giao thức xác định nào có thể đảm bảo tất cả các nút không lỗi đạt được đồng thuận trong thời gian giới hạn.

Trước khi chúng ta phá vỡ các hệ quả của định lý này, tôi muốn dành một chút thời gian để lập luận rằng các giả định của FLP (tin nhắn bất đồng bộ, lỗi crash) áp dụng cho giao thức của chúng ta:

• Tin nhắn bất đồng bộ: Việc gửi tin nhắn đến LLM thường bất đồng bộ. LLM thường chịu trách nhiệm xác định khi nào tin nhắn được đọc và chúng có thể trì hoãn điều này tùy ý. Tuy nhiên, một tác nhân LLM cố gắng gửi tin nhắn cho tác nhân khác, dù thông qua hệ thống tệp dùng chung, hàng đợi chuyển tiếp tin nhắn hoặc bất kỳ khung sườn nào khác, thời điểm tin nhắn này sẽ được nhìn thấy bởi tác nhân kia thường được xác định bởi LLM kia — khi nó hoàn thành quá trình suy luận của mình, hoặc khi các chương trình hoặc công cụ nó gọi đã hoàn thành. Nhìn chung chúng ta không thể đặt ra giới hạn cho việc giao tin nhắn.

• Lỗi crash: Điều này cần ít biện minh hơn, nhưng các tác nhân khá háo hức tự bắn vào chân mình. Lỗi crash trong bối cảnh này không chỉ có nghĩa là một cái gì đó như quá trình本身 chết đi, mà cũng có thể là một cái gì đó như tác nhân chạy một công cụ không bao giờ kết thúc (tức là một bash script với vòng lặp vô tình, v.v.). Những lúc khác, chúng có thể chỉ tự pkill mình. Nhìn chung, các tác nhân có thể sập bất ngờ.

Vậy điều đó có nghĩa gì cho chúng ta? Cụ thể, điều đó có nghĩa là trong bất kỳ hệ thống đa tác nhân nào, bất kể các tác nhân thông minh đến đâu, họ sẽ không bao giờ có thể đảm bảo rằng họ có thể làm cả hai điều cùng một lúc:

• An toàn (Safety): Tức là tạo ra phần mềm được hình thành tốt thỏa mãn thông số kỹ thuật của người dùng.
• Sống (Liveness): Tức là luôn đạt được đồng thuận trên mô-đun phần mềm cuối cùng.

Bạn có thể ngạc nhiên về phần tính sống (liveness), vì các tác nhân dường như luôn tiến bộ và kết thúc trong hầu hết các quy trình làm việc, nhưng điều này không có nghĩa là họ đạt được đồng thuận — thực tế, một mô hình rất phổ biến mà tôi thấy là một loại vòng lặp, đi đi lại lại trên các quyết định thiết kế nơi một tác nhân chọn một quyết định thiết kế, tác nhân khác hoàn tác thay đổi, chọn một quyết định khác, và sau đó họ lặp lại.

Một sự thật thú vị khác từ quan điểm này là quan sát rằng khi chúng ta có các tác nhân chạy trên một máy dùng chung, chúng ta có thể làm tốt hơn một chút so với mô hình lỗi crash thuần túy — cụ thể, chạy các lệnh như ps | grep claude v.v. có thể tương ứng với một cái gì đó giống như một bộ phát hiện lỗi (failure detector) mà từ đó chúng ta có thể thu được các giới hạn mạnh hơn về đồng thuận. Cụ thể, bài báo "Bộ phát hiện lỗi không đáng tin cậy cho các hệ thống phân tán đáng tin cậy" của Chandra và Toueg được xây dựng trên FLP và chứng minh rằng đồng thuận là có thể trong cài đặt FLP nếu và chỉ nếu các tác nhân được phép truy cập vào một thiết bị phát hiện lỗi (có thể không đáng tin cậy) báo cáo liệu các tác nhân khác còn sống hay không. Nếu các tác nhân tương ứng với các quy trình, và quá trình còn sống tương đương với tiến bộ (điều này không nhất thiết luôn đúng), thì ps có thể cung cấp cho chúng ta một cái gì đó như vậy. Một điều cần rút ra từ điều này có thể là cung cấp cho LLM một công cụ để kiểm tra tính sống của các tác nhân khác.

Bài toán các tướng Byzantine cho phát triển phần mềm đa tác nhân

Kết quả bất khả thi thứ hai tôi muốn phác thảo một kết nối là tinh tế hơn một chút, nhưng vẫn hữu ích để suy nghĩ: "Bài toán các tướng Byzantine" của Lamport.

Trong một hệ thống phân tán, một nút Byzantine là một khái niệm mô hình hóa tương ứng với giả định thất bại trường hợp xấu nhất cho một người tham gia; trong khi các định lý như FLP giả định rằng khi máy chủ lỗi, nó sẽ sập và ngừng tham gia giao thức, các nút Byzantine có thể làm điều đó, hoặc họ có thể làm bất cứ điều gì, tức là họ có thể отклон từ giao thức theo các cách tùy ý, chẳng hạn như giả mạo tin nhắn từ người dùng khác, gửi tin nhắn cho những người tham gia mà nó không có ý định, hoặc lặp lại các tin nhắn trước đó như một vài ví dụ.

Các chế độ lỗi Byzantine có thực sự liên quan cho phát triển phần mềm đa tác nhân không? Mặc dù mô hình lỗi này hơi bảo thủ — chắc chắn các tác nhân của chúng ta sẽ không cố tình phá vỡ hệ thống của chúng ta — tôi nghĩ mô hình này vẫn hữu ích để suy nghĩ trong cài đặt của chúng ta vì các lỗi Byzantine dường như là một cách tốt để nắm bắt ý tưởng về "hiểu sai" lời nhắc đầu vào của chúng ta. Một tác nhân hiểu sai lời nhắc có thể, cho tất cả các mục đích và ý định, được coi là một tác nhân Byzantine trong giao thức, tích cực làm việc chống lại những người tham gia khác đang cố gắng tạo ra một hệ thống phần mềm chính xác. Trong sự hiện diện của các tác nhân như vậy, chúng ta có thể vẫn đạt được đồng thuận không?

Định lý các tướng Byzantine (Lamport-Shostak-Pease, 1982): Trong bất kỳ hệ thống chuyển tiếp tin nhắn đồng bộ nào với (f) tác nhân Byzantine có thể отклон từ giao thức tùy ý, sự đồng thuận giữa các quy trình trung thực chỉ có thể đạt được nếu tổng số quy trình (n \gt 3f + 1).

Vì vậy, cụ thể, với cách giải thích này, nếu chúng ta khởi chạy (n) tác nhân để triển khai hệ thống phần mềm của mình, nếu nhiều hơn (\frac{n - 1}{3}) tác nhân hiểu sai lời nhắc thì đồng thuận là không thể. Trong bài báo, Lamport đề xuất một thuật toán cho cài đặt này, ở mức cao liên quan đến việc thu thập phiếu bầu từ tất cả những người tham gia và lấy đa số. Việc bỏ phiếu tập thể trong cài đặt của chúng ta nhiều hơn là một cấu trúc lý thuyết và một nơi mà sự tương tự của chúng ta bắt đầu phá vỡ một chút — không gian triển khai phần mềm đủ lớn mà việc bỏ phiếu khó có thể tạo ra nhiều tiến bộ — nhưng vẫn có một số hiểu biết hữu ích chúng ta có thể rút ra từ kết quả bất khả thi này.

Quan sát chính ở đây là kết quả của Lamport là một giới hạn cứng về số lượng tối đa các sự hiểu sai chúng ta có thể dung nạp để phát triển phần mềm thực sự có thể. Đây không phải là điều gì đó sẽ được giải quyết bởi các tác nhân thông minh hơn hoặc LLM tốt hơn. Bài toán tổng hợp của chúng ta vốn dĩ chưa được xác định đầy đủ, và do đó các tác nhân có thể luôn có sự hiểu sai. Một hành động có thể thực hiện được từ phân tích này là trong khi chúng ta không thể cải thiện số lượng sự hiểu sai (f) chúng ta có thể dung nạp, chúng ta có thể tăng khả năng thành công bằng cách áp dụng các kỹ thuật để giảm số lượng sự hiểu sai — cụ thể, các cơ chế xác minh bên ngoài như kiểm thử, phân tích tĩnh và xác minh hiệu quả chuyển đổi sự hiểu sai thành lỗi crash — thay vì tiếp tục với sự hiểu sai của mô tả ngôn ngữ tự nhiên, tác nhân có thể sập, hoặc tinh chỉnh cách giải thích của nó để khớp với các bài kiểm tra, từ đó chúng ta có thể tái sử dụng các kết quả FLP yếu hơn.

Đọc thêm

Ngoài FLP và các tướng Byzantine, còn một số kết quả hệ thống phân tán chính khác có thể đáng để suy nghĩ trong bối cảnh phát triển phần mềm đa tác nhân, nhưng mà các liên kết chính xác đã được để lại như một bài tập cho người đọc :)

• Kiến thức chung (Common Knowledge) (Halpern & Moses, 1990): Bài báo này định nghĩa một mô hình hình thức để lý luận về dòng chảy của kiến thức nhận thức trong một hệ thống phân tán và thiết lập các kết quả bất khả thi cho sự tồn tại của kiến thức chung trong các hệ thống như vậy.
• Đồng bộ một phần (Partial Synchrony) (Dwork, Lynch & Stockmeyer, 1988): Mô hình đồng bộ một phần của Dwork et al. là lối thoát tiêu chuẩn để cung cấp đồng thuận bất chấp FLP. Thủ thuật chính trong công việc này là đặt ra giới hạn trên cho độ trễ tin nhắn — trong các hệ thống phân tán thực tế, thiết bị không chờ đợi vô hạn để tin nhắn đến, và sẽ hết thời gian chờ và yêu cầu gửi lại. Với sự đơn giản hóa này, đồng thuận trở nên có thể giải quyết được với chi phí tăng độ phức tạp tin nhắn.
• Định lý CAP (Gilbert & Lynch, 2002): Tất nhiên, bất kỳ bài đăng nào về hệ thống phân tán "phổ thông" sẽ không hoàn chỉnh nếu không có tham chiếu đến định lý CAP được ca ngợi! CAP, giống như FLP, cung cấp một kết quả bất khả thi quy định rằng bất kỳ hệ thống phân tán nào phải chọn giữa nhiều nhất hai trong số Tính nhất quán (Consistency - các tác nhân có đồng thuận về các chế độ xem nội bộ của họ), Tính sẵn sàng (Availability - các tác nhân có thể phục vụ các yêu cầu cuối cùng) và Khả năng chịu phân vùng (Partition tolerance - các tác nhân vẫn có thể tiến bộ ngay cả khi một phần của mạng không thể truy cập được).

Kết luận

Vậy, điều này để lại chúng ta ở đâu? Lập luận tôi đã xây dựng xuyên suốt bài đăng này là phát triển phần mềm đa tác nhân vốn dĩ là một bài toán hệ thống phân tán, và như vậy, nó kế thừa các kết quả bất khả thi từ tài liệu. Định lý FLP cho chúng ta biết hệ thống phân tán không thể có cả tính an toàn, tính sống và khả năng chịu lỗi. Các tướng Byzantine của Lamport cho chúng ta giới hạn chính xác về các quy trình Byzantine trước khi đồng thuận trở nên không thể. Lưu ý rằng không có kết quả nào trong số này phụ thuộc vào trí thông minh của tác nhân.

Điểm không phải là phát triển phần mềm đa tác nhân là không thể — mọi người chắc chắn đang vận chuyển phần mềm thực với các tác nhân ngày nay, và họ có thể sẽ vận chuyển nhiều thứ lộn xộn hơn vào ngày mai. Lập luận tôi đưa ra nhiều hơn là những người này hiện đang làm như vậy bằng cách ngầm giải quyết các bài toán phối hợp này, thường thông qua các cơ chế tạm thời (ad-hoc) không có sự đảm bảo hay chế độ lỗi nào được suy nghĩ kỹ.

Tài liệu hệ thống phân tán có các hình thức toán học chính xác cho tất cả các cơ chế này, bốn mươi năm định lý về những gì chúng có thể và không thể giải quyết cho bạn, và các quy tắc rõ ràng về khi và ở đâu các kỹ thuật khác nhau nên được áp dụng.

Điều này đưa chúng ta trở lại trích dẫn từ phần mở đầu của chúng ta: "Giải pháp tốt nhất cho việc phối hợp tác nhân là chỉ cần đợi thêm vài tháng."

Có thể. Tôi sẽ thừa nhận điều đó, nhưng ngay cả khi vậy, các kết quả bất khả thi ở trên không phải là các tạo vật nhất thời của khả năng của các mô hình hiện tại; chúng sẽ không biến mất khi các tác nhân trở nên thông minh hơn; chúng là các thuộc tính vốn có của lĩnh vực này. Các tác nhân thông minh hơn có thể thu hẹp các hằng số trong thuật toán của chúng ta, nhưng chúng sẽ không, và không thể, loại bỏ các giới hạn. Nếu chúng ta muốn phát triển phần mềm đa tác nhân thực sự mở rộng quy mô, thì sớm hay muộn ai đó phải thực sự làm công việc thiết kế các giao thức, ngôn ngữ và công cụ giải quyết các bài toán phối hợp cơ bản như một mối quan tâm hàng đầu thay vì hy vọng nó sẽ biến mất.