FlashProve cho phép xác minh mật mã đối với đầu ra suy luận của LLM

Các nhà nghiên cứu của Anthropic và cộng sự học thuật đã phát hành FlashProve, một nguyên mẫu mã nguồn mở sử dụng bằng chứng kiến thức không (zero-knowledge proofs) để xác minh đầu ra của các mô hình ngôn ngữ lớn. Được công bố vào tháng 11 năm 2026, hệ thống này cho phép người dùng xác nhận rằng một phản hồi được tạo ra bởi một tập hợp trọng số mô hình cụ thể mà không cần tiết lộ các trọng số đó hoặc yêu cầu tài nguyên tính toán đáng kể cho việc xác minh.

Điều gì đã xảy ra

Nhóm nghiên cứu, bao gồm các chuyên gia từ Anthropic, EPFL, MIT và Succinct, đã giới thiệu FlashProve nhằm giải quyết những vấn đề ngày càng tăng về niềm tin trong triển khai AI. Khi các mô hình trở thành một phần không thể thiếu của hạ tầng kỹ thuật số, người dùng gặp khó khăn trong việc xác minh rằng mô hình phục vụ họ chính là mô hình họ đã yêu cầu. Các dịch vụ định tuyến có thể thay thế bằng các mô hình rẻ hơn, hoặc kẻ tấn công có thể can thiệp vào luồng token. FlashProve cung cấp một giải pháp mật mã, trong đó nhà cung cấp tạo ra một bằng chứng kèm theo phản hồi, và người dùng có thể nhanh chóng xác minh bằng chứng này.

Phiên bản đánh dấu tiến độ hướng tới mục tiêu công khai của Anthropic là tạo ra một nguyên mẫu cho suy luận có thể chứng minh được trước ngày 30 tháng 9 năm 2026. Mặc dù công ty trước đây đã đạt được mục tiêu này thông qua một dự án khác liên quan đến máy chủ tin cậy, FlashProve đưa ra một phương pháp chỉ dựa trên phần mềm, sử dụng các lập luận ngắn gọn về kiến thức không (zkSNARKs). Nhóm đã phát hành mã thực thi, báo cáo kỹ thuật và các hiện vật xác minh chính thức dưới giấy phép Apache 2.0 để khuyến khích cộng đồng cải thiện.

Hệ thống cho thấy hiệu suất thực tế đối với các mô hình lớn. Đối với Llama 4 Maverick, một mô hình hỗn hợp chuyên gia (mixture-of-experts) với 400 tỷ tham số và lượng tử hóa 4-bit, một GPU H100 đơn lẻ tạo ra các bằng chứng với tốc độ khoảng 110 token mỗi giây. Kích thước bằng chứng kết quả là khoảng 19 MB cho một yêu cầu gồm 1.024 token. Mặc dù quy trình này mất thời gian gấp 70 đến 95 lần so với suy luận tiêu chuẩn sử dụng vLLM, nó đại diện cho một bước tăng tốc đáng kể so với các hệ thống mã nguồn mở trước đây, vốn chậm hơn nhiều bậc độ lớn.

Cách hoạt động

FlashProve dựa trên zkSNARK, một công cụ mật mã cho phép bên chứng minh thuyết phục bên xác minh rằng một phép tính đã được thực hiện đúng cách mà không tiết lộ bất kỳ dữ liệu đầu vào nào ngoài kết quả. Trong bối cảnh này, "phép tính" là quá trình lan truyền thuận (forward pass) của mạng nơ-ron. Hệ thống hoạt động theo hai giai đoạn. Đầu tiên, trong giai đoạn ngoại tuyến (offline), nhà cung cấp mô hình công bố một cam kết (commitment), đóng vai trò như một dấu vân tay duy nhất cho các trọng số mô hình cụ thể. Cam kết này cố định chính xác các trọng số trong khi vẫn giữ chúng ẩn.

Trong giai đoạn trực tuyến (online), khi người dùng gửi một prompt, nhà cung cấp chạy mô hình và tạo ra một tệp bằng chứng. Tệp này chứng nhận rằng mô hình đã cam kết tạo ra các token đầu ra cụ thể cho input đã cho. Người dùng, đóng vai trò là bên xác minh, kiểm tra bằng chứng này bằng cách sử dụng cam kết, prompt và phản hồi. Vì bằng chứng rất ngắn gọn, việc xác minh nhanh hơn theo hàm mũ so với việc chạy lại mô hình và có thể được thực hiện trên CPU tiêu chuẩn trong vài giây. Quan trọng hơn, tính chất kiến thức không đảm bảo rằng bằng chứng không tiết lộ bất kỳ điều gì về các trọng số mô hình độc quyền.

Để đảm bảo độ tin cậy của các tuyên bố mật mã, nhóm đã sử dụng Lean, một ngôn ngữ xác minh chính thức. Họ cung cấp các tuyên bố cấp cao có thể kiểm toán trong Lean cho các đảm bảo an ninh, cùng với một trình trực quan hóa tương tác cho các định lý. Phương pháp này chống lại sự phức tạp của tối ưu hóa tự động bằng cách cung cấp các đảm bảo chặt chẽ về mặt toán học rằng giao thức hoạt động đúng như đặc tả.

Chi tiết chính

• FlashProve đạt tốc độ tạo bằng chứng khoảng ~110 token/giây cho Llama 4 Maverick (400B tham số) trên một GPU H100 đơn lẻ.
• Kích thước bằng chứng xấp xỉ 19 MB cho mỗi yêu cầu 1.024 token, cho phép truyền tải và lưu trữ hiệu quả.
• Hệ thống sử dụng trọng số lượng tử hóa 4-bit và số học nguyên trong giai đoạn prefill để tối ưu hóa hiệu suất.
• Việc xác minh chỉ yêu cầu cam kết, prompt và phản hồi, cho phép người dùng kiểm tra tính hợp lệ mà không cần truy cập vào trọng số mô hình.
• Tất cả mã nguồn, bằng chứng Lean và tài liệu đều được phát hành dưới giấy phép Apache 2.0 để tạo điều kiện cho việc kiểm toán và cải thiện từ bên ngoài.
• Giải pháp chỉ dựa trên phần mềm, phụ thuộc vào độ khó tính toán thay vì môi trường thực thi tin cậy hoặc phần cứng chuyên dụng.

Tại sao điều này quan trọng

Đối với các kỹ sư phần mềm và lãnh đạo kỹ thuật, FlashProve giới thiệu một lớp toàn vẹn mới cho các ứng dụng AI. Nó giải quyết vấn đề thay thế mô hình, nơi một dịch vụ định tuyến của bên thứ ba có thể đổi một mô hình cao cấp lấy một mô hình rẻ hơn. Bằng cách đính kèm một bằng chứng mật mã vào mỗi phản hồi, các nhà cung cấp có thể đưa ra các đảm bảo có thể xác minh được cho khách hàng. Điều này đặc biệt liên quan đến các đội ngũ bảo mật nội bộ cần đảm bảo rằng chỉ các mô hình đã được phê duyệt và an toàn đang chạy trong môi trường sản xuất, ngăn chặn các agent rogue hoặc máy chủ bị xâm nhập phục vụ các đầu ra độc hại.

Công nghệ này cũng có tác động đến tuân thủ quy định và tốc độ phát triển AI. Các cơ quan quản lý có thể yêu cầu nhà cung cấp nộp các bằng chứng chứng minh rằng phần cứng đang được sử dụng cho suy luận trên các mô hình đã được phê duyệt thay vì cho việc huấn luyện trái phép. Điều này cho phép giám sát mà không cần tiết lộ các trọng số độc quyền hoặc yêu cầu cơ quan quản lý phải sở hữu tài nguyên tính toán khổng lồ. Ngoài ra, các nhà phát triển có thể sử dụng các bằng chứng này để chứng minh sự thận trọng cần thiết, chẳng hạn như chứng minh rằng một mô hình frontier cụ thể đã quét mã để tìm lỗ hổng, tăng thêm độ tin cậy cho các tuyên bố bảo mật.

Bạn có thể làm gì

• Xem xét mã nguồn mở FlashProve và báo cáo kỹ thuật để hiểu chi tiết triển khai của zkSNARK cho LLM.
• Thử nghiệm với trình xác minh nhanh C++ và trình xác minh chính xác có thể chứng minh được bằng Lean được cung cấp để kiểm thử xác thực bằng chứng trên hạ tầng của riêng bạn.
• Đánh giá sự đánh đổi giữa chi phí tạo bằng chứng (gấp 70-95 lần thời gian suy luận) và lợi ích bảo mật cho trường hợp sử dụng cụ thể của bạn.
• Cân nhắc xem suy luận có thể chứng minh được có thể tích hợp vào stack định tuyến hoặc giám sát AI hiện tại của bạn như thế nào để ngăn chặn việc thay thế mô hình.
• Khám phá các hiện vật chính thức hóa Lean để kiểm toán nền tảng toán học của các đảm bảo an ninh do hệ thống cung cấp.
• Theo dõi các phát triển tiếp theo trong lĩnh vực machine learning kiến thức không khi cộng đồng xây dựng dựa trên nền tảng được cấp phép Apache 2.0 này.