Tự động hóa chứng minh toán học với LLM: Xây dựng bộ giải nén Zstandard trong Lean

Tôi từ lâu đã có cảm tình với các ngôn ngữ định kiểu phụ thuộc (dependently-typed languages) như Coq và Lean. Chúng mang đến khả năng tạo ra một hệ thống kiểu dữ liệu có thể mã hóa và thực thi các bất biến (invariants) tinh vi tùy ý. Đây là kiểu dữ liệu mà trong các ngôn ngữ thông thường, kết cục (tốt nhất) chỉ là một dòng chú thích, và sẽ nhanh chóng bị lãng quên khi quy mô nhóm phát triển tăng lên. Sau đó, bạn sẽ gặp phải những hiểu lầm tinh vi và các thành phần không thực sự khớp với nhau. Thường thì các thành phần đó đã phát triển đến mức đủ lớn, khiến cho việc điều chỉnh chúng trở thành một viễn cảnh mệt mỏi khi vấn đề được phát hiện. Có lẽ, như cách các kiểu phụ thuộc gợi mở, bạn có thể viết các bất biến đó một cách hình thức và để máy tính kiểm tra chúng.

(Tái bút: Coq đã đổi tên! Tôi nhớ nhiều năm trước tại một hội nghị Coq ở Princeton, tôi đã gợi ý rằng trong một thế giới nói tiếng Anh, việc đặt tên một ngôn ngữ lập trình là Coq là một trở ngại. Tôi không nghĩ khán giả lúc đó đồng tình. Tôi cũng nói đùa rằng nhiều bài thuyết trình ở đó nghe như bài phát biểu của Tyrion Lannister, vì có quá nhiều "Coqs" và "Hoares". Một câu đùa hài hước và đúng thời điểm, mặc dù nó hoàn toàn thất bại vì nó diễn ra trước mùa cuối của loạt phim đó và việc chúng ta đồng loạt xóa sạch ký ức về nó.)

Vấn đề luôn nằm ở chỗ sức mạnh lớn của hệ thống kiểu dữ liệu đi kèm với nỗ lực chứng minh lớn. Tôi chắc chắn có thể làm chứng cho những ngày trọn vẹn chỉ để chứng minh những điều thực sự đơn giản. Việc thực hiện các chứng minh thực ra khá thú vị: nó đầy thách thức, mang tính tương tác và có mục tiêu rõ ràng. Nhưng trời ơi, nó tốn quá nhiều thời gian, đặc biệt nếu bạn giống tôi, không biết mình đang làm gì. Ngoài ra còn có trải nghiệm khó chịu định kỳ, sau nhiều giờ nỗ lực, bạn nhận ra rằng mục tiêu mà bạn đang cố gắng chứng minh thực tế lại là sai. Kết quả kinh điển ở đây là bản tổng kết từ nỗ lực seL4, cho thấy rằng ngay cả khi dự án đủ lớn để các kỹ sư tích lũy kinh nghiệm đáng kể, họ vẫn dành thời gian chứng minh gấp khoảng 10 lần so với thiết kế và triển khai. Cuối cùng, họ có số dòng mã chứng minh nhiều gấp hơn 20 lần so với mã C.

Chi phí đó đã khiến việc lập trình bằng các ngôn ngữ định kiểu phụ thuộc trở nên cực kỳ chuyên biệt (niche). Nó cũng thúc đẩy mọi người cố gắng tự động hóa quá trình này. Nỗ lực mà tôi biết sơ qua là F*, nơi hệ thống cố gắng để một bộ giải SMT tự động giải quyết các nghĩa vụ (obligations). Điều đó chắc chắn hiệu quả với các trường hợp đơn giản, nhưng rất dễ để tạo ra thứ gì đó khiến bộ giải SMT "bay vào không gian" và chạy hàng giờ, khiến bạn tự hỏi liệu nó có bao giờ kết thúc hay không. Tôi thấy rằng những người sử dụng các ngôn ngữ này nhiều phải phát triển giác quan thứ sáu để biết điều gì sẽ làm bộ giải hài lòng, và sau đó xây dựng mọi thứ xung quanh điều đó. Nó có thể giúp ích, nhưng đến một mức độ nào đó, nó biến vấn đề thành chủ nghĩa thần bí: bạn kết thúc bằng việc phục vụ một vị thần phức tạp và thất thường.

Một sự thật quan trọng là, ít nhất về mặt lý thuyết, một khi mệnh đề đã đúng, nội dung chứng minh của nó không còn quan trọng: chỉ sự tồn tại của nó mới quan trọng. Điều này không hoàn toàn đúng do hai yếu tố phức tạp: thứ nhất, cái mà nhóm seL4 gọi là "kỹ thuật chứng minh" (proof engineering): nhu cầu cấu trúc các chứng minh để giảm bớt nỗ lực điều chỉnh lại chúng sau khi thay đổi mã. Và thứ hai, các chứng minh đủ phức tạp có thể khiến ngay cả các trình kiểm tra kiểu (type checkers) cũng bị quá tải và tiêu tốn lượng lớn bộ nhớ.

Hiện nay chúng ta đã có các LLM, kết hợp với tính không quan trọng của chứng minh (proof irrelevance), hứa hẹn sẽ là một hình thức tự động hóa chứng minh cực kỳ hiệu quả. Với lượng tự động hóa đủ lớn, có lẽ bạn không cần phải lo lắng quá nhiều về kỹ thuật chứng minh. Bạn vẫn cần tránh làm quá tải trình kiểm tra kiểu, nhưng trong các thử nghiệm hạn chế của tôi, LLM có thể tránh được điều đó. Có khả năng, LLM đột nhiên làm cho các hệ thống định kiểu phụ thuộc trở nên thực tế hơn đáng kể. Tôi muốn thử nghiệm điều này nên đã xây dựng một bộ giải nén Zstandard bằng Lean, chủ yếu vì tôi cũng tò mò về Zstandard.

Zstandard dường như đang thắng thế trong cuộc cạnh tranh thay thế gzip làm tiện ích nén chuẩn. Nó là một bộ nén kiểu LZ77 khác, nhưng cung cấp mã hóa entropy tốt hơn và thiết kế cẩn thận cho phép nó đạt được tốc độ giải nén rất ấn tượng. Nó sẽ không bao giờ đẹp như bzip2, nhưng sự thanh lịch rạng rỡ của biến đổi Burrows–Wheeler không có nhiều ý nghĩa trước những lợi thế thực tế đáng kể:

(Các phép đo được thực hiện trên máy tính tham chiếu tiêu chuẩn, tức là bất cứ thứ gì tác giả đang sử dụng vào thời điểm đó. Và lưu ý thang đo log trên trục y: gzip và Zstandard nằm trong phân khúc tốc độ riêng của chúng. Đây là máy Apple và gzip của Apple được tối ưu hóa đặc biệt; hãy kỳ vọng gzip sẽ chậm hơn ở những nơi khác.)

Zstandard (do Yann Collet thực hiện, dựa trên công trình ANS nền tảng của Jarek Duda) có một RFC, nhưng nó khá ngắn gọn. Nó chứa tất cả thông tin bạn cần để triển khai bộ giải nén, nhưng trừ khi bạn đã khá quen thuộc với nén dữ liệu, tôi nghĩ bạn sẽ cần đọc lại vài lần để hiểu chuyện gì đang xảy ra. Ít nhất tôi đã phải đọc phần 4.1 nửa tá lần trước khi cảm thấy mình nắm bắt được nó. Quá muộn trong quá trình này, tôi phát hiện ra đồng nghiệp của mình, Nigel Tao, đã viết một bài giải thích về Zstandard tốt hơn những gì tôi có thể làm. Vì vậy, nếu bạn muốn hiểu Zstandard, bạn nên đọc bài đó. Tôi chỉ định đưa ra lời giải thích về phần thú vị nhất, bộ mã hóa entropy, và kết hợp nó với một chút truyền bá về Lean.

Công việc của một bộ mã hóa entropy là, với một tập hợp các ký hiệu có xác suất không đồng nhất, mã hóa một chuỗi các ký hiệu đó bằng cách sử dụng ít bit nhất có thể. Bộ mã hóa entropy kinh điển là bộ mã hóa Huffman. Các bộ mã hóa Huffman xây dựng một cây nhị phân với các ký hiệu ở các nút lá, và Huffman đã chỉ ra rằng một thuật toán rất đơn giản tạo ra một cây tiền tố tối ưu: bạn lấy danh sách các ký hiệu, tìm hai ký hiệu có xác suất thấp nhất và tạo thành một nút cây với chúng là các nút con. Nút cây đó sau đó có xác suất là tổng xác suất của hai nút con, và sau đó bạn lặp lại thuật toán với số ký hiệu ít hơn hai, nhưng bây giờ với một nút cây được thêm vào. Rõ ràng mỗi bước của thuật toán này làm giảm kích thước của tập hợp các phần tử đi một, vì vậy nó kết thúc, và nó cũng tạo ra một cây tối ưu. Các cây Huffman rất nhanh vì bạn có thể xây dựng một bảng được lập chỉ mục bởi n bit tiếp theo (trong đó n là độ dài của mã dài nhất). Mục nhập bảng cho bạn biết ký hiệu bạn đã giải mã và bao nhiêu bit cần đọc lại. Nhược điểm của cây Huffman là chúng chỉ có thể sử dụng một số nguyên bit cho mỗi ký hiệu: nếu bạn có một ký hiệu mà -log2(p) = 2.3 thì lý tưởng nhất là bạn muốn sử dụng 2.3 bit để mã hóa nó. Nhưng Huffman buộc bạn phải làm tròn lên 3 bit hoặc làm tròn xuống, điều này sẽ buộc một số ký hiệu khác tiêu tốn nhiều bit hơn.

Zstandard sử dụng cây Huffman, nhưng nó cũng có một bộ mã hóa entropy nén cao hơn gọi là FSE. FSE là một máy trạng thái. Có nhiều trạng thái hơn ký hiệu, và mỗi ký hiệu nhận được một phần các trạng thái phản ánh xác suất xuất hiện của nó trong luồng. Vì vậy, nếu có một ký hiệu dự kiến xuất hiện 50% thời gian, nó nhận được ~50% số trạng thái. Mỗi trạng thái có ba giá trị: ký hiệu cho trạng thái đó, số bit cần đọc từ luồng bit khi ở trạng thái đó, và số trạng thái cơ sở được cộng vào các bit đó để có được trạng thái tiếp theo. Bây giờ, nếu bạn nhớ lại, vấn đề với cây Huffman là chúng chỉ có thể sử dụng một số nguyên bit, và các trạng thái này cũng đọc một số nguyên bit. Nhưng thủ thuật là nếu bạn nhắm đến việc đọc 1.5 bit cho một ký hiệu nhất định, thì một nửa số trạng thái của nó sẽ đọc 1 bit và một nửa sẽ đọc 2 bit. Sau đó, bạn đạt được mục tiêu của mình ở mức trung bình. Bảng trạng thái không bao giờ được truyền đi. RFC quy định một thuật toán để xây dựng bảng từ danh sách xác suất ký hiệu, và vì vậy chỉ cần truyền các xác suất.

Hãy lấy một ví dụ. Giả sử chúng ta có bốn ký hiệu và chúng ta sẽ sử dụng 16 trạng thái. Vì vậy, chúng ta phải xấp xỉ xác suất ký hiệu theo đơn vị 1/16. (Nếu bạn muốn xấp xỉ xác suất chính xác hơn, bạn có thể sử dụng số lượng trạng thái lớn hơn; zstd thực tế không bao giờ sử dụng ít hơn 32 trạng thái.)

Bất kỳ ký hiệu nào cũng có thể theo sau bất kỳ ký hiệu nào khác, và một ký hiệu có thể chỉ có một trạng thái duy nhất. Vì vậy, mọi ký hiệu phải có khả năng tiếp cận mọi trạng thái. Hãy nhìn vào trạng thái ba, trạng thái duy nhất cho ký hiệu D. Vì nó là trạng thái duy nhất, nó phải đọc bốn bit, đủ để mã hóa bất kỳ trạng thái nào khác. Nhưng nếu bạn nhìn vào một ký hiệu như B, các trạng thái của nó chỉ yêu cầu bạn đọc một hoặc hai bit. Tuy nhiên, tập hợp 16 trạng thái tiếp theo có thể xảy ra được phân chia chính xác giữa các trạng thái đó cho ký hiệu B. Vì vậy, đối với bất kỳ trạng thái cụ thể nào, có chính xác một trạng thái cho ký hiệu B có thể tiếp cận nó.

Một lần nữa, hãy xem xét ký hiệu B, mà chúng ta đã nói có xác suất là 5/16. Số bit lý tưởng để mã hóa ký hiệu đó là -log2(5/16) = 1.68. Có ba trạng thái ký hiệu B đọc hai bit và hai trạng thái đọc một bit. Các trạng thái không được sử dụng thường xuyên như nhau và, được tính trọng số theo tần suất sử dụng, giá trị trung bình gần như chính xác với giá trị cho các xác suất đã lượng tử hóa. Nếu bạn muốn nắm bắt xác suất ký hiệu thực sự với độ chính xác cao hơn, hãy sử dụng bảng lớn hơn.

Thủ thuật trung tâm là, bằng cách cung cấp nhiều trạng thái cho các ký hiệu phổ biến hơn, bộ mã hóa không chỉ chọn một ký hiệu: nó còn chọn trạng thái nào của ký hiệu đó để rơi vào, và lựa chọn đó mang thông tin chuyển tiếp sang ký hiệu tiếp theo. Đó là nơi các bit thông tin phân số đi đến. Nhưng bộ mã hóa entropy này vẫn chỉ dựa trên bảng, vì vậy nó chạy rất nhanh.

Điểm khó là bạn không thể làm việc theo hướng tiến. Giả sử bạn muốn mã hóa C, D. Bạn bắt đầu ở trạng thái C nào? Chà, D chỉ có một trạng thái nên đó phải là trạng thái C có thể tiếp cận trạng thái đó. Nếu D có nhiều trạng thái thì bạn sẽ cần lo lắng về những gì xảy ra sau D để biết bạn cần trạng thái nào trong số đó. FSE buộc bạn phải bắt đầu ở cuối chuỗi và làm việc ngược lại. (Điều đó không quá tệ vì bạn thường cần biết toàn bộ chuỗi để tính toán xác suất ký hiệu.) Hơn nữa, một bộ nén Zstandard do đó mã hóa các ký hiệu từ sau ra trước, nhưng ghi đầu ra theo từng phần, vì vậy bộ giải nén phải tìm đến cuối khối và đọc các bit ngược lại để sắp xếp lại! Đó là đi vào các chi tiết rộng hơn của định dạng mà tôi sẽ không đề cập; hãy xem bài viết của Nigel.

Các bộ mã hóa entropy cơ bản không quan tâm đến xác suất giữa các ký hiệu. Nghĩa là, chúng không thể sử dụng thực tế là chữ Q thường đi sau chữ U (trong tiếng Anh). Phải có một mã hóa khác khai thác những dư thừa đó. Trong Zstandard, đó là cấu trúc Lempel–Ziv truyền thống, nơi nó mã hóa các byte ký tự hoặc các tham chiếu ngược đến dữ liệu đã giải mã trước đó. Vì vậy, FSE chủ yếu được sử dụng để mã hóa hiệu quả các độ lệch và độ dài tham chiếu ngược này.

Lean

Hãy nói về Lean! Ở trên tôi đã nói rằng đó là một ngôn ngữ định kiểu phụ thuộc, và đó là một khái niệm được diễn đạt tốt hơn trong các ví dụ thay vì một định nghĩa phức tạp. Vì vậy, đây là kiểu của một hàm đọc n byte từ một luồng và, nếu nó không ném ra lỗi, sẽ trả về một mảng byte mà hệ thống kiểu biết là dài n byte.

Đây là một hàm trả về hai số và một mảng byte sao cho số đầu tiên là số nguyên tố, tổng của hai số chia hết cho sáu, và mảng byte dài ít nhất bằng số nhỏ hơn trong hai số đó.

Đó không phải là kiểu dữ liệu mà bất kỳ ai cũng cần. Nó chỉ chứng minh rằng bạn có thể đi xa đến mức nào tùy thích với điều này. Các ngôn ngữ định kiểu phụ thuộc đủ để mã hóa ngay cả những cấu trúc toán học rất phức tạp, và việc sử dụng chủ yếu của Lean hiện tại là một ngôn ngữ hình thức để phát biểu và chứng minh toán học. Cuốn sách gần đây, The Proof in the Code, là một bài diễn giải ngắn gọn, được viết tốt về câu chuyện Lean ra đời như thế nào. Tác giả đã hoàn toàn làm hỏng toán học kiến thiết trong vài đoạn văn nhưng, ngoài điều đó ra, tôi rất thích nó!

Lean là một ngôn ngữ thuần hàm giống như Haskell, mặc dù nó có một vài thuộc tính làm cho nó có khả năng trở thành một ngôn ngữ lập trình thuận tiện hơn nhiều. Thứ nhất, Lean là nghiêm ngặt (strict), trong khi Haskell là lười (lazy). Sự nghiêm ngặt có nghĩa là các đối số của hàm được đánh giá trước khi lệnh gọi xảy ra, trong khi ở Haskell, việc đánh giá các đối số được trì hoãn cho đến khi giá trị thực sự cần thiết. Vì vậy, trong Haskell, việc viết các biểu thức đắt đỏ và truyền chúng vào các hàm là miễn phí, vì chúng sẽ chỉ thực sự được tính toán nếu chúng được sử dụng. Nhưng nó cũng có nghĩa là việc tính toán có thể xảy ra ở những nơi rất đáng ngạc nhiên trong chương trình. Đây là một chủ đề gây tranh cãi nhưng, mặc dù tôi đánh giá cao sự thanh lịch của tính lười, chà, nó có thể làm cho hiệu suất của các chương trình khó suy luận.

Tiếp theo, Lean có một số phần "đường cú pháp" (sugar) thú vị. Ký hiệu monadic do của nó chứa các vòng lặp for, câu lệnh return và câu lệnh break. Nếu bạn muốn lập trình theo phong cách mệnh lệnh, bạn có thể làm điều đó khá hợp lý!

Cuối cùng, Lean có một tối ưu hóa nơi nó sẽ thực hiện các cập nhật đột biến (mutating updates) cho các đối tượng miễn là số lượng tham chiếu của chúng bằng một. Vì vậy, bạn có thể đột biến một mảng tại chỗ hiệu quả như trong một ngôn ngữ mệnh lệnh, miễn là bạn cẩn thận không để có tham chiếu đến nó ở nơi khác. Thật không may, Lean không có bất kỳ khía cạnh nào của hệ thống kiểu tuyến tính (linear type system) mà tôi biết, vì vậy nó không giúp bạn đảm bảo rằng chỉ có một tham chiếu duy nhất đến một giá trị. Đó là một điểm sắc bén mà một chỉnh sửa nhỏ trong mã có thể làm hỏng hoàn toàn hiệu suất của nó bằng cách giữ một tham chiếu đến một mảng lớn ở đâu đó không dễ thấy. Nhưng nó có nghĩa là nếu bạn đang cố gắng tối ưu hóa hiệu suất của thứ gì đó, bạn có nhiều công cụ hơn theo ý mình.

Đây là một ví dụ về một số điều này, từ bộ giải mã zstd mà tôi đã phác thảo:

Tập trung vào dòng 9. Có một chỉ mục mảng ở đó, đó chính xác là kiểu nơi các bất biến ngầm định tồn tại: blockBytes tốt nhất là không nên trống! Các ngôn ngữ giống C sẽ cung cấp cho bạn hành vi không xác định trong trường hợp đó. Các ngôn ngữ hiện đại sẽ ném lỗi khi chạy, hoặc chỉ cung cấp cho bạn một giá trị tùy chọn để tránh điều đó. Lean có một lựa chọn khác: chứng minh rằng nó không trống. Đó là những gì dòng 10 làm. blockBytes.property là thực tế rằng nó dài bằng lần đọc được yêu cầu, tức là chính xác là blockHeader.contentSize byte. blockHeader.contentSize_rle là thế này:

Đó là một bằng chứng cho thấy, khi kiểu là rle, contentSize luôn là một. Với những sự thật đó, Lean có thể tìm ra phần còn lại.

Đó là một bằng chứng thực sự ngắn và có lẽ tôi có thể tự tìm ra điều đó, nhưng chúng ta có thể nhắm cao hơn nhiều:

Tôi đã viết một triển khai thuật toán xây dựng bảng FSE từ RFC. RFC chứa các "vector kiểm thử" cho nó: ba đầu ra mẫu từ các xác suất đã cho. Rõ ràng những thứ đó đi vào các bài kiểm thử đơn vị. Nhưng, trong Lean, chúng ta cũng có thể chứng minh các thuộc tính phổ quát của hàm:

Nhắc lại điều đó bằng lời:

Giả sử rằng hàm xây dựng bảng, khi được cung cấp hằng số "độ chính xác" và danh sách xác suất ký hiệu, tạo ra một giá trị, thì:

Đây là những giả định tinh vi mà một vòng lặp giải mã tối ưu hóa yêu cầu, và những thứ chỉ có thể là ngầm định hoặc chỉ là các chú thích trong các hệ thống kiểu yếu hơn. Chứng minh các mệnh đề mạnh như vậy là một phần của nỗ lực gấp 10 lần mà bản tổng kết seL4 đã mô tả, và là một rào cản lớn đối với việc áp dụng các kiểu phụ thuộc trong phần mềm thông thường. Một số LLM hiện có thể thực hiện tự động trong khoảng 20 phút, và chỉ sử dụng một phần hạn ngạch đăng ký $20/tháng. Nó có lẽ sẽ là tiêu chuẩn vào năm tới. Tôi phải thừa nhận rằng họ cần thay đổi mã tạo bảng khi thực hiện việc đó: tôi đã sử dụng quá nhiều Id.run (tức là chuyển sang chế độ mệnh lệnh) và điều đó khó hơn cho bộ máy chứng minh làm việc cùng. (Nhưng Lean đang làm việc về vấn đề đó.) Tôi đã xác nhận rằng các chứng minh kiểm tra kiểu và không có "sorry" nào.

Kết hợp các kiểu phụ thuộc và LLM không phải là một ý tưởng mới, nhưng chưa có nhiều nghiên cứu về việc áp dụng sự kết hợp này vào kỹ thuật phần mềm hàng ngày. Cần nhiều kinh nghiệm hơn nữa. Các kiểu rất mạnh có thể khuếch đại phạm vi thay đổi vì chúng phải được truyền ra thông qua tất cả các kiểu dẫn xuất. Có lẽ nỗ lực chứng minh mở rộng kém trong các hệ thống lớn hơn, đến mức ngay cả các LLM hiện đại cũng không thể theo kịp. Lean là một ngôn ngữ cấp cao, và điều đó không phù hợp với mọi thứ. (Bộ giải mã Zstandard đồ chơi của tôi chậm hơn 10 lần so với zstd trên dòng lệnh.) Tuy nhiên, tự động hóa chứng minh đã ở đây và chúng ta, về mặt thực tế, có một loại ngôn ngữ lập trình mới. Điều đó thật thú vị!

(Tôi không xuất bản mã vì, thẳng thắn mà nói, đối với một trường hợp nhỏ, được xác định rõ như thế này, các LLM có lẽ có thể làm tốt hơn tôi. Tôi đã làm điều này để học Lean một chút và tôi không coi những khám phá của mình là một ví dụ điển hình. Điều này được lấy cảm hứng từ lean-zip, thứ làm được nhiều hơn thế, bao gồm một bộ nén và chứng minh tính khứ hồi!)

Bên lề: hợp ngữ đã được xác minh (verified assembly)

AWS đã tạo ra LNSym: một ngữ nghĩa và trình mô phỏng cho AArch64. Điều đó thật tuyệt. Có lẽ chúng ta có thể sử dụng nó để chứng minh sự tương đương giữa một triển khai hợp ngữ tối ưu hóa của một số hàm và các đối tác Lean của chúng, sau đó sử dụng mã hợp ngữ khi chạy? Sau đó, chúng ta có thể để LLM tối ưu hóa và chúng sẽ không thể đưa ra bất kỳ lỗi chức năng nào. Hợp ngữ đã được xác minh là một lĩnh vực đã được nghiên cứu kỹ trong các triển khai mật mã, nhưng có lẽ bây giờ nó có thể trở nên rẻ hơn?

Tôi đã dành một chút thời gian (chủ yếu là LLM) để thử điều này. Ví dụ popcount nhỏ từ kho lưu trữ sử dụng bv_decide, một bộ giải SAT chứng nhận, và ví dụ đó yêu cầu nhiều bộ nhớ hơn hệ thống của tôi có, điều này không báo hiệu tốt. Các hàm nhỏ hoạt động, và có thể có được một bằng chứng tương đương với các hàm Lean nhỏ, và sau đó sử dụng extern để gọi chúng khi chạy! Nhưng tôi, và một vài LLM, không thể làm cho nó mở rộng thêm nữa.