Anthropic ra mắt FlashProve, công cụ tạo bằng chứng mật mã cho suy luận AI

Anthropic đã phát hành FlashProve vào ngày 2 tháng 11 năm 2026: một nguyên mẫu nghiên cứu mã nguồn mở sử dụng bằng chứng mật mã để chứng minh rằng phản hồi của mô hình ngôn ngữ được tạo ra từ bộ trọng số đã cam kết mà không tiết lộ các trọng số đó. Công ty cho biết tốc độ tạo bằng chứng cho Meta’s Llama 4 Maverick đạt 110 token mỗi giây.

Nghiên cứu này giải quyết một khoảng trống trong việc xác minh AI được lưu trữ trên máy chủ. Một câu trả lời có chất lượng cao không cho biết mô hình nào đã tạo ra nó: dịch vụ định tuyến có thể thay thế bằng một hệ thống khác, người đánh giá có thể nhận được mô hình khác với mô hình dự kiến dùng để thử nghiệm, hoặc kẻ tấn công có thể chỉnh sửa luồng token. Người dùng khó có thể kiểm tra bằng cách chạy lại mô hình vì bộ trọng số được giữ kín và yêu cầu phần cứng rất lớn.

Ràng buộc phản hồi với bộ trọng số ẩn

FlashProve sử dụng lập luận tri thức súc tích không tiết lộ thông tin, hay zkSNARK, trong một thiết kế chỉ dựa trên phần mềm thay vì phụ thuộc vào phần cứng đáng tin cậy. Trong giai đoạn ngoại tuyến, nhà cung cấp công bố một cam kết ngắn xác định chính xác một bộ trọng số, đồng thời giữ bí mật các trọng số đó. Với từng cặp lời nhắc và phản hồi đã hoàn tất, hệ thống tạo ra bằng chứng cho thấy các token đầu ra là kết quả từ mô hình đã cam kết. Bất kỳ ai có cam kết, lời nhắc và phản hồi đều có thể kiểm tra bằng chứng mà không cần truy cập bộ trọng số.

Các thuộc tính dự kiến gồm tính đầy đủ, tính vững chắc, tính không tiết lộ thông tin và tính súc tích. Một bằng chứng trung thực phải được chấp nhận, còn việc chứng nhận một mệnh đề sai phải đòi hỏi phá vỡ những giả định mật mã được tin cậy rộng rãi. Việc kiểm tra bằng chứng không được làm lộ bộ trọng số hay các giá trị tính toán trung gian. Thiết kế này cũng che giấu những mạng con chuyên gia nào đã chạy cho từng token, dù bản thân kiến trúc mô hình vẫn được công khai.

Cách triển khai tận dụng cấu trúc hỗn hợp chuyên gia của Maverick. Khối lượng công việc của bên tạo bằng chứng tỷ lệ với khoảng 17 tỷ tham số được kích hoạt cho mỗi token, thay vì toàn bộ 400 tỷ tham số, đồng thời vẫn che giấu lựa chọn chuyên gia. Các phần bộ trọng số được truyền trực tiếp từ bộ nhớ máy chủ, giúp bên tạo bằng chứng hoạt động trên một GPU 80 GB cùng với khoảng 290 GB bộ nhớ máy chủ.

Anthropic mô tả các ứng dụng tiềm năng gồm kiểm tra tính toàn vẹn cho khách hàng, đánh giá độc lập, công cụ quản lý và thực thi yêu cầu sử dụng mô hình đã được phê duyệt. Chứng nhận suy luận có thể xác nhận rằng các yêu cầu được xử lý bằng mô hình được khai báo, nhưng không thể chứng minh rằng cùng phần cứng đó không đồng thời được dùng để huấn luyện một mô hình khác. Sự khác biệt này giới hạn những gì các chứng nhận như vậy có thể chứng minh về việc tuân thủ các yêu cầu dựa trên cách sử dụng năng lực tính toán.

Hiệu năng tạo bằng chứng và độ trễ bổ sung khi suy luận

Đánh giá của Anthropic sử dụng một phiên bản chuyển đổi 4 bit của mô hình, được công khai rộng rãi. Một máy chủ có một H100 và 24 lõi CPU tạo bằng chứng cho một lô gồm 24 yêu cầu trong khoảng 223 giây, tạo ra bằng chứng 18,78 MB cho mỗi yêu cầu. Bước tạo cam kết ngoại tuyến mất khoảng 39 phút.

Ở phía xác minh, máy khách tải xuống một cam kết có dung lượng khoảng 6,5 MB và kiểm tra bằng chứng bằng CPU, không cần GPU. Anthropic đo được thời gian xác minh là 17 giây với 24 luồng và 21 giây với một luồng, bao gồm cả các bước kiểm tra trong giai đoạn ngoại tuyến.

Các số liệu này cho thấy quy trình kiểm tra chỉ dùng CPU khác biệt với thao tác tạo bằng chứng nặng hơn nhiều. Trong phép so sánh của Anthropic với suy luận FP8 trên tám H100 chạy vLLM, việc tạo bằng chứng cần lượng thời gian trên mỗi GPU cao hơn khoảng 72 lần cho cùng một lô yêu cầu và cao hơn khoảng 94 lần ở mức tải vLLM cao nhất được thử nghiệm. Vì vậy, tốc độ xử lý này đi kèm chi phí đáng kể so với việc phục vụ mô hình mà không tạo bằng chứng.

Xác minh hình thức và những giới hạn thực tiễn

Kho lưu trữ FlashProve bao gồm một công cụ tạo bằng chứng, một trình xác minh C++ tốc độ cao, một trình xác minh Lean chậm hơn, các chứng minh Lean cho những mệnh đề toán học cấp cao nhất và một công cụ trực quan hóa định lý tương tác, theo giấy phép Apache 2.0. Kho này ghi rõ phiên bản 0.16.0 là sản phẩm nghiên cứu không còn được bảo trì và không tiếp nhận đóng góp.

Các phần việc với Lean xem xét tính đầy đủ, tính vững chắc và tính không tiết lộ thông tin trong mô hình oracle ngẫu nhiên. Những mệnh đề hình thức vẫn cần được xem xét thủ công để xác định liệu chúng có diễn đạt đúng các bảo đảm dự kiến hay không. Trình xác minh Lean được kết nối hình thức với định lý về tính vững chắc, nhưng trình xác minh C++ dành cho mục đích sử dụng thường xuyên không có bảo đảm hình thức; thay vào đó, nó được thử nghiệm để kiểm tra xem kết quả có khớp với trình xác minh Lean hay không.

Tài liệu về các giới hạn đã biết của dự án ghi nhận 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 và tài liệu, đồng thời chạy các thử nghiệm được báo cáo. Chưa có cuộc kiểm tra bảo mật độc lập nào được thực hiện, và việc thử nghiệm khả năng che giấu bộ trọng số cũng như chống lại bằng chứng đối kháng vẫn còn hạn chế.

Các bằng chứng áp dụng cho phiên bản số nguyên chính xác của bộ trọng số khi giải mã tham lam. Suy luận dấu phẩy động hoặc giải mã bằng lấy mẫu có thể khác với phép tính được chứng minh, còn các thử nghiệm lỗi tổng quát không bao quát những lời nhắc được thiết kế có chủ đích để tấn công. Ngữ cảnh bị giới hạn ở 1.024 token, trong khi các cuộc tấn công dựa trên thời gian và những kênh kề khác nằm ngoài phạm vi bảo đảm. Việc tạo bằng chứng sau khi suy luận còn dẫn đến tính toán lại, bảo đảm bị trì hoãn và tính không xác định, so với việc tạo bằng chứng đồng thời với suy luận.

Để suy luận có thể chứng minh trở thành bước kiểm tra thường quy đối với lưu lượng được phục vụ, phần việc còn lại tập trung vào những khoảng trống mà bản phát hành này cho thấy: giảm chi phí chứng minh, hỗ trợ các phương thức giải mã ít hạn chế hơn và ngữ cảnh dài hơn, đồng thời gắn kết chặt chẽ hơn bản triển khai nhanh với giao thức hình thức.