Anthropic mở mã FlashProve: bằng chứng mật mã cho biết model nào thực sự đang trả lời bạn, 110 token/giây trên một GPU H100

Bài nghiên cứu của Anthropic mang tên “Progress on provable inference for large language models” đề ngày 2/11/2026; phần lớn báo chí đưa tin vào ngày 3/11. Bài giới thiệu FlashProve, một hệ thống mã nguồn mở cho phép nhà cung cấp model chứng minh, bằng một bằng chứng mật mã chứ không phải một lời hứa, rằng câu trả lời nào đó được sinh ra từ đúng một bộ trọng số (weights) cụ thể. Trọng số vẫn được giữ kín. Người kiểm tra không cần GPU.

Các con số nổi bật lấy từ bài viết và bản báo cáo kỹ thuật dài 23 trang, và chính chúng là lý do để đọc kỹ đợt phát hành này. Trên một GPU NVIDIA H100, FlashProve tạo bằng chứng cho Llama 4 Maverick, model mixture-of-experts (hỗn hợp chuyên gia, viết tắt MoE) 400 tỷ tham số của Meta, với tốc độ khoảng 110 token/giây. Mỗi bằng chứng nặng 18,78 MB và một CPU 24 nhân kiểm tra xong trong 17 giây. Hệ thống duy nhất trước đó từng chứng minh cùng model này mà Anthropic biết, dự án mở VerInf, mất 14,3 giờ để chứng minh 1.000 token trên một máy DGX Spark, sinh ra bằng chứng 93,6 GB và cần gần một ngày để kiểm tra.

Những gì được phát hành

Năm sản phẩm, tất cả theo giấy phép Apache 2.0:

bản thân bài blog;
một báo cáo kỹ thuật do các tác giả là người viết: Roy Rinberg và Alex Allain của Anthropic, Alessandro Chiesa (EPFL và StarkWare), Miranda Christ (MIT), Rahul Dalal (Succinct), Giacomo Fenzi và Guy Weissenberg (EPFL), Ben Mayer (MIT);
một bản đặc tả giao thức dài hơn nhiều do Claude viết, mà nhóm tác giả thừa nhận “chưa rà soát kỹ”, kèm lời hứa sẽ có bài báo được duyệt cẩn thận sau;
mã chạy được trong kho anthropics/FlashProve, phiên bản 0.16.0: một prover (bộ tạo bằng chứng) chạy trên GPU, một verifier (bộ kiểm tra) nhanh viết bằng C++, và một verifier chậm hơn viết bằng Lean;
các chứng minh Lean cho những phát biểu an toàn ở tầng cao nhất, cùng một công cụ trực quan hoá định lý để người kiểm toán đọc.

Tệp README nói thẳng về hiện trạng một cách hiếm thấy. Kho mã là “một sản phẩm nghiên cứu: không được bảo trì, không nhận đóng góp”, và trang giới hạn đã biết ghi rằng các hệ thống AI dưới sự chỉ đạo của con người đã viết gần như toàn bộ phần mềm, chứng minh Lean lẫn tài liệu, và tự chạy các bài kiểm thử được báo cáo. TechCrunch cho biết chưa có kế hoạch triển khai hệ thống này tại Anthropic hay bất kỳ phòng thí nghiệm nào khác. Chính Anthropic mô tả bài viết là “tiến độ trung gian, không phải một chương trình nghiên cứu đã hoàn tất”, chia sẻ “với mục tiêu rõ ràng là để người khác xem, lấy về và cải tiến”.

Bài toán mà nó nhắm tới

Khi gọi một model qua API, bạn chỉ thấy token. Bạn không thấy bộ trọng số nào đã sinh ra chúng. Một dịch vụ định tuyến (router) có thể lặng lẽ tráo sang model rẻ hơn để tiết kiệm tiền. Một đơn vị chạy benchmark có thể tráo sang model đắt hơn để thổi phồng điểm số. Kẻ tấn công chiếm được máy chủ suy luận có thể can thiệp vào luồng token và ẩn mình giữa các câu trả lời thật. Anthropic bổ sung một tình huống mà chỉ một phòng thí nghiệm tiền tuyến mới nghĩ đến: khi model đủ khả năng tự cải tiến và tự triển khai, “một model tiên tiến hơn có thể chạy thay chỗ model đã được cấp phép và tự giới thiệu mình là model yếu hơn, để né các bộ phân loại và cơ chế giám sát lẽ ra áp lên nó.”

Câu đó không hề trừu tượng với công ty này. Một ngày trước bài viết, hồ sơ IPO sửa đổi của Anthropic nói với SEC rằng công ty “có thể sắp” chạm ngưỡng mà Chính sách Mở rộng Có trách nhiệm (RSP) của họ gọi là “tiến bộ tăng tốc đột biến nhờ AI”, điều chưa có trong bài phân tích hồ sơ S-1 trước đây của blog này. FlashProve được giới thiệu như một mảnh ghép trong bộ công cụ mà một phòng thí nghiệm như vậy cần, để biết trọng số nào đang thực sự chạy trên máy chủ của chính mình.

Bài viết cũng gắn công trình này với một cam kết công khai. Lộ trình An toàn Tiền tuyến của Anthropic từng hứa “một nguyên mẫu provable inference trước ngày 30/9/2026”. Một chú thích cuối trang giải thích phần chữ nhỏ: cam kết đó đã được hoàn thành bằng một dự án khác, chuyên ký số luồng suy luận và tính toán lại trên một máy chủ tin cậy; và bản cập nhật RSP ngày 19/10 đã đổi tên mục tiêu thành “inference verification” (xác minh suy luận), vì cụm “provable inference” gợi ý một hướng đi hẹp hơn mức công ty hiện cho là cần thiết. FlashProve theo đuổi cùng mục tiêu đó bằng một phương pháp khác, thuần phần mềm.

Cơ chế hoạt động, nói theo ngôn ngữ lập trình viên

FlashProve là một zkSNARK, viết tắt của zero-knowledge succinct argument of knowledge (lập luận tri thức ngắn gọn không tiết lộ), xây theo đúng cách các hệ chứng minh dựa trên hàm băm hiện đại được xây: một interactive oracle proof (IOP) được nén bằng cam kết Merkle rồi biến thành phi tương tác bằng phép biến đổi Fiat-Shamir. Giả định mật mã duy nhất là hàm nén bên trong hàm băm BLAKE2 hành xử như một hàm ngẫu nhiên. Không đường cong elliptic, không cần thiết lập tin cậy, và có khả năng kháng máy tính lượng tử. Báo cáo cho biết đây cũng là công thức đang chạy các mạng rollup thương mại như Starknet.

Về vận hành, có hai pha:

Cam kết (offline, một lần cho mỗi model). Nhà cung cấp mã hoá trọng số, băm thành một cam kết ngắn, và chứng minh rằng phần mã hoá đó hợp lệ. Với Maverick, bước này mất khoảng 39 phút và nhà cung cấp lưu 2,15 GB. Cam kết dùng được cho khoảng 16 triệu yêu cầu trước khi phải tạo lại. Phía khách tải về chừng 6,5 MB, một lần duy nhất.
Chứng minh (online, theo từng yêu cầu). Với mỗi câu trả lời, prover chứng tỏ rằng model đã cam kết, chạy trên prompt này, cho ra đúng token này. Mỗi yêu cầu là một cửa sổ 1.024 token và mỗi bằng chứng xác nhận một token, tức lựa chọn greedy của model ngay sau prompt. Prover gom tối đa 64 yêu cầu thành một lô, mở cam kết trọng số một lần cho cả lô, và xuất ra một bằng chứng 18,78 MB cho mỗi yêu cầu.

Ba quyết định kỹ thuật giải thích tốc độ. Thứ nhất, khối lượng việc của prover tỷ lệ với số chuyên gia thực sự được kích hoạt, khoảng 17 tỷ trong 400 tỷ tham số của Maverick cho mỗi token, trong khi bằng chứng vẫn giấu kín chuyên gia nào đã được chọn. Thứ hai, chứng minh được làm sau khi đã trả lời (post-hoc): văn bản hoàn chỉnh được đọc lại trong một lượt song song, giống pha prefill, thay vì từng token một như pha decode. Thứ ba, hệ thống vừa trên một GPU 80 GB bằng cách để 232 GB trọng số 4-bit trong khoảng 290 GB RAM của máy chủ và truyền vào GPU theo từng đoạn lớp.

Cái giá được nêu rõ. So với vLLM chạy bản FP8 của cùng model trên tám H100, việc chứng minh một lô 24 yêu cầu mất khoảng 72 lần lâu hơn tính trên mỗi GPU so với prefill thường (dao động 66 đến 77 giữa các lần chạy), và khoảng 94 lần so với vLLM ở mức tải cao nhất đã thử. Một yêu cầu được chứng minh riêng lẻ xong trong 58 giây, nhưng thông lượng rơi xuống 17,6 token/giây. Khi chạy theo lô, mỗi yêu cầu chờ khoảng năm phút để có bằng chứng.

Ngưỡng an toàn trong README rất cụ thể: nhà cung cấp gian dối sẽ bị bắt, trừ xác suất khoảng q/2^124 + 2^-101 sau q lần truy vấn hàm băm, với mục tiêu an toàn 128 bit.

Xác minh hình thức, và điểm dừng của nó

Cách nhóm tự đặt vấn đề: Claude tối ưu hoá giỏi “nhưng thường đưa ra những quyết định khó đánh giá, nhất là trong các hệ thống lớn và phức tạp”. Lời giải của họ là phát biểu giao thức cùng ba tính chất, tính đầy đủ (completeness), tính đúng đắn (soundness) và tính không tiết lộ (zero knowledge), trong trợ lý chứng minh Lean, để người rà soát chỉ cần kiểm tra các phát biểu định lý có khớp ý định hay không, thay vì phải đọc hàng nghìn dòng mã mật mã.

Báo cáo rất cẩn trọng về điều này mua được gì và không mua được gì:

Soundness chỉ phụ thuộc vào verifier. Verifier viết bằng Lean, chạy được, đã được chứng minh là chỉ chấp nhận những gì định lý soundness chấp nhận. Verifier C++ nhanh hơn “không mang bảo đảm hình thức nào”; nó cho kết quả trùng với bản Lean trên mọi bằng chứng trong bộ kiểm thử, nhưng đó là kiểm thử, không phải chứng minh.
Prover chạy GPU là mã C++ do một agent AI sinh ra từ biểu diễn Lean, chưa được chứng minh là tương đương. Lỗi ở đó có thể làm hỏng completeness hoặc rò rỉ thông tin trọng số, nhưng không thể giả mạo bằng chứng.
Zero knowledge mới chỉ được chứng minh hình thức khi các yêu cầu được xử lý từng cái một, chưa phải theo lô, trong khi theo lô mới là chế độ đạt 110 token/giây.
Mọi chứng minh đều nằm trong mô hình oracle ngẫu nhiên. Đó là chuẩn mực trong mật mã ứng dụng, nhưng vẫn là một giả định heuristic, không phải định lý về BLAKE2.

So với những gì đã có

Phần công trình liên quan trong bài viết đọc như một lược sử ngắn của zkML (zero-knowledge machine learning). ZKML năm 2024 chứng minh GPT-2 ở khoảng 0,006 token/giây; zkLLM cùng năm đạt chừng 2,5 token/giây trên LLaMA-2-13B theo lô trên một A100; DeepProve, hệ thống đã qua phản biện hiện nay, báo cáo 2,9 token/giây với GPT-2 và 31 khi chạy phân tán; VerInf, trên chính Maverick, đạt khoảng 0,02. Đối chiếu thương mại gần nhất là Attestable, công bố 53 đến 77 token/giây cho model dày đặc (dense) Gemma 4 31B trên một H100 nhưng chưa phát hành mã nào. Vì vậy tuyên bố của FlashProve là hai điều cùng lúc: một bước nhảy vài bậc độ lớn trên một model lớn gấp 30 lần phần lớn mục tiêu học thuật trước đó, và bản triển khai mở đầu tiên ở quy mô này.

Cách Anthropic tự đánh giá: chi phí phụ trội “khoảng 2 bậc độ lớn” so với suy luận thường là “thấp hơn nhiều so với dự đoán trước đây”, và kết quả này hẳn sẽ chuyển sang được các kiến trúc khác. Đó là một dự báo, chưa phải một kết quả.

Vì sao đáng quan tâm

Với lập trình viên, ý nghĩa trước mắt nằm ở bài toán định tuyến. Các cổng trung gian và dịch vụ gom API đã đứng trước một phần lớn lưu lượng, và nghi vấn rằng một số bên hạ cấp hoặc tráo model đã lan truyền cả năm nay; bài viết của Anthropic dẫn “vendor verifier” của Kimi (Moonshot) như ví dụ cho cách tiếp cận thống kê hiện tại. Một bằng chứng đính kèm mỗi câu trả lời sẽ biến “tin router” thành “kiểm tra bằng chứng”, và việc kiểm tra chạy trong vài giây trên laptop, không cần trọng số. Cùng cơ chế đó cho các đơn vị đánh giá độc lập cách biết chắc model họ kiểm thử đúng là model đang được phục vụ.

Với cơ quan quản lý và cuộc tranh luận về kìm tốc độ phát triển AI, lập luận là bằng chứng cho phép nhà cung cấp chứng tỏ phần cứng của mình đã phục vụ đúng model đã cam kết trong một giai đoạn, mà không phải giao nộp trọng số. Bài viết thẳng thắn rằng điều này chứng minh suy luận đã diễn ra, chứ không chứng minh rằng không có huấn luyện lén ở bên cạnh.

Với chính các phòng thí nghiệm, tình huống phát hiện can thiệp có lẽ là mạnh nhất. Một bằng chứng gắn với cam kết sẽ phát hiện máy chủ bị xâm nhập, hoặc một model tự tráo chỗ, mà không cần tin máy chủ. Chứng minh sau khi trả lời không thể ngăn một câu trả lời xấu đến tay người dùng; nó bảo đảm hành vi can thiệp sẽ bị phát hiện sau đó. Báo cáo xếp đây vào phòng thủ nhiều lớp, bên cạnh các môi trường thực thi tin cậy (TEE), vốn được coi là bổ trợ chứ không cạnh tranh.

Những câu hỏi còn mở

Phạm vi. Ngữ cảnh 1.024 token kém thực tế trò chuyện một đến hai bậc độ lớn. Mỗi bằng chứng xác nhận một token theo giải mã greedy của một model đã lượng tử hoá sang số nguyên; câu trả lời lấy mẫu bằng số thực dấu phẩy động có thể lệch đi một cách chính đáng, và báo cáo trông cậy vào các phương pháp thống kê để tách nhiễu lành tính khỏi can thiệp. Kiến trúc MoE bị lộ, điều một nhà cung cấp có thể coi là bí mật kinh doanh.
Chi phí. Bảy mươi đến chín mươi lăm giây H100 chứng minh cho mỗi giây H100 suy luận là một hoá đơn lớn ở bất kỳ lưu lượng thật nào. Cách triển khai hiển nhiên là lấy mẫu một phần lưu lượng, hoặc chứng minh theo yêu cầu cho những request hệ trọng, chứ không phải chứng minh tất cả.
Mức bảo đảm. Gần như toàn bộ mã và chứng minh do AI viết; tài liệu giao thức chi tiết chưa được rà soát; chưa có kiểm toán an ninh độc lập; tấn công kênh kề (side-channel) lên prover nằm ngoài phạm vi. Các phát biểu Lean là thứ cần kiểm toán, và Anthropic đang đề nghị cộng đồng làm đúng việc đó.
Mức độ đón nhận. Một sản phẩm nghiên cứu “không được bảo trì” từ một phòng thí nghiệm “chưa có kế hoạch triển khai” là một lời mời, không phải một sản phẩm. Router, đơn vị đánh giá hay cơ quan quản lý có nhận lời hay không là câu hỏi mà năm tới sẽ trả lời.