Anthropic công bố FlashProve: bằng chứng mật mã cho suy luận LLM

Anthropic vừa công bố FlashProve, một nguyên mẫu mã nguồn mở cho phép chứng minh bằng mật mã rằng một phản hồi của mô hình ngôn ngữ thực sự được sinh ra bởi đúng bộ trọng số mà nhà cung cấp đã cam kết — chứ không phải một mô hình bị thay thế ngầm, hay một luồng token đã bị kẻ tấn công can thiệp.

Vấn đề xuất phát từ một thực tế đơn giản: khi trò chuyện trực tiếp với một người, ta có nhiều cách để chắc chắn đó là họ. Khi trò chuyện với một mô hình AI, ta gần như không có cách nào. Người dùng hiện nay không thể kiểm chứng phản hồi đến từ đúng mô hình mà nhà phát triển tuyên bố.

Provable inference là gì và vì sao quan trọng

Provable inference (tạm dịch: suy luận có thể chứng minh) là hướng nghiên cứu cho phép người dùng có tài nguyên tính toán hạn chế, và không biết gì về trọng số, vẫn xác minh được một phản hồi do đúng mô hình được yêu cầu tạo ra.

Công cụ cốt lõi ở đây là zkSNARK (zero-knowledge succinct argument of knowledge — lập luận ngắn gọn, không tiết lộ thông tin). Cơ chế hoạt động gồm hai bên: nhà cung cấp mô hình (prover) và người dùng (verifier). Prover gửi kèm phản hồi một tệp bằng chứng ngắn, người dùng kiểm tra nhanh trên CPU. Nếu phản hồi lệch khỏi mô hình đã chỉ định, bước kiểm tra sẽ thất bại. Điểm mấu chốt: bằng chứng không tiết lộ bất kỳ thông tin nào về trọng số của mô hình.

Nhóm tác giả nêu bốn tình huống mà kỹ thuật này có ích:

• Kiểm soát tốc độ phát triển AI (pacing): cơ quan quản lý có thể yêu cầu bằng chứng rằng phần cứng thực sự đang phục vụ suy luận bằng đúng mô hình, thay vì âm thầm dùng mô hình rẻ hơn để dồn tài nguyên cho huấn luyện.
• Phát hiện can thiệp: máy chủ suy luận trở thành mục tiêu hấp dẫn; kẻ tấn công có thể chèn phản hồi độc hại lẫn vào luồng phản hồi thật. Bằng chứng gắn với một cam kết (commitment) cụ thể về trọng số, nên không thể giả mạo.
• Nguồn gốc văn bản: chứng minh rằng một mô hình biên (frontier model) thực sự đã được dùng để làm việc gì đó, ví dụ quét lỗ hổng cho một thư viện phần mềm.
• Phê duyệt mô hình: cơ quan quản lý có thể buộc nhà cung cấp chỉ phục vụ các mô hình đã được phê duyệt.

Tác giả cũng phân biệt rõ với hướng tiếp cận dựa trên trusted execution environment (môi trường thực thi tin cậy, tức giải pháp phần cứng). FlashProve đi theo hướng thuần phần mềm, dựa trên độ khó của các bài toán tính toán — nghĩa là kẻ tấn công không thể tạo bằng chứng sai hợp lệ trừ khi phá được các giả định mật mã phổ biến. Hai hướng này bổ sung cho nhau.

Hiệu năng của FlashProve

Kết quả đo trên Llama 4 Maverick, mô hình mixture-of-experts (MoE) 400 tỷ tham số với khoảng 17 tỷ tham số được dùng mỗi token, dùng bộ trọng số 4-bit công khai:

• Pha offline (cam kết trọng số) chạy một lần cho mỗi mô hình, mất khoảng 39 phút.
• Pha online trên một lô 24 yêu cầu mất khoảng 223 giây, tức 110 token/giây, mỗi bằng chứng nặng 18,78 MB.
• Verifier chỉ cần CPU: tải cam kết khoảng 6,5 MB, mỗi lần kiểm tra mất 17 giây trên 24 luồng (21 giây trên một luồng).

So sánh với suy luận thường: chạy vLLM với bản FP8 của cùng mô hình trên tám GPU H100, thời gian tạo bằng chứng cho một lô 24 yêu cầu chậm hơn khoảng 72 lần (dao động 66-77 lần giữa các lần chạy), và khoảng 94 lần khi vLLM chạy ở mức tải cao nhất mà nhóm thử.

Để thấy mức tiến bộ, có thể nhìn vào các công trình trước: zkLLM (2024) chứng minh mô hình LLaMA-2-13B với khoảng 15 phút cho đầu vào 2.048 token; VerInf từng chứng minh đúng Llama 4 Maverick nhưng mất 14,3 giờ cho 1.000 token với bằng chứng 93,6 GB và gần một ngày để xác minh. FlashProve đạt 110 token/giây với bằng chứng 19 MB kiểm tra trong vài giây.

Cách hệ thống hoạt động

Giao thức gồm hai pha:

1. Pha offline: prover công bố một cam kết về trọng số mô hình — một "dấu vân tay" ngắn cố định đúng một bộ trọng số, trong khi bản thân trọng số vẫn được giữ kín. Cam kết này dùng được cho khoảng 16 triệu yêu cầu, sau đó phải cam kết lại.
2. Pha online: với mỗi yêu cầu, prover tạo tệp bằng chứng chứng minh rằng mô hình đã cam kết, khi chạy trên prompt này, sinh ra đúng những token đó.

Bốn tính chất mà tệp bằng chứng đảm bảo:

• Completeness: bằng chứng trung thực luôn được chấp nhận.
• Soundness: gần như không thể tạo bằng chứng hợp lệ cho một phát biểu sai.
• Zero-knowledge: không tiết lộ trọng số, giá trị trung gian hay expert nào được kích hoạt ở mỗi lớp. Kiến trúc mô hình (không gồm trọng số) không được giấu.
• Succinctness: bằng chứng ~19 MB, kiểm tra trong vài giây trên CPU 24 nhân.

Về kỹ thuật, FlashProve dựa trên một interactive oracle proof (IOP) — đối tượng lý thuyết thông tin — được biên dịch thành bằng chứng mật mã nhờ hàm băm, kết hợp các công cụ như kiểm tra độ gần mã (code proximity test) với ràng buộc tuyến tính và lookup argument. Cách tối ưu chính gồm: khối lượng tính toán của prover tỷ lệ với số expert thực sự chạy (~17 tỷ tham số thay vì 400 tỷ); bằng chứng theo lô sau khi sinh văn bản (post-hoc, giống cơ chế prefill); và chia trọng số theo từng đoạn lớp để vừa một GPU 80 GB cùng khoảng 290 GB bộ nhớ host.

Tin cậy nhờ kiểm chứng hình thức

Mã mật mã nổi tiếng dễ lỗi. Để người dùng tin được đoạn mã phát hành, nhóm dùng Lean, một trợ lý chứng minh hình thức, để đặc tả giao thức và ba tính chất bảo mật cấp cao (completeness, soundness, zero-knowledge) theo cách máy kiểm tra được, trong random oracle model.

Bản phát hành gồm năm thành phần: bài blog, báo cáo kỹ thuật, tài liệu đặc tả giao thức (do Claude viết), mã thực thi (một prover, hai verifier gồm bản C++ nhanh và bản Lean chứng minh đúng), cùng các chứng minh Lean kèm công cụ trực quan tương tác. Tất cả phát hành theo giấy phép Apache 2.0.

Nhóm cũng thẳng thắn nêu các giới hạn: không đảm bảo hình thức cho mã thực thi nhanh; bằng chứng dựa trên mô hình số nguyên với greedy decoding (nên phản hồi từ bản dấu phẩy động hoặc sampling có thể lệch); chưa xét tấn công kênh bên (side channel) như đo thời gian tạo bằng chứng; và hiện chỉ chứng minh ngữ cảnh tối đa 1.024 token, khá ngắn so với cửa sổ ngữ cảnh hàng trăm nghìn đến hàng triệu token của các mô hình biên.

Góc nhìn

Với các kỹ sư và doanh nghiệp Việt Nam đang tích hợp LLM vào sản phẩm, FlashProve chưa phải công cụ dùng ngay — mức phụ trội 70-95 lần so với suy luận thường và giới hạn 1.024 token khiến nó phù hợp với kiểm toán và xác minh chọn mẫu hơn là phục vụ toàn bộ lưu lượng. Tuy nhiên, mô hình mã nguồn mở theo Apache 2.0 và chứng minh Lean có thể kiểm tra độc lập là điểm đáng chú ý: doanh nghiệp có thể tự chạy verifier trên CPU thường để xác minh nhà cung cấp, thay vì phải tin hoàn toàn.

Đáng quan tâm hơn là hướng đi. Khi chi phí chứng minh giảm từ nhiều giờ xuống còn vài trăm giây trong khoảng hai năm, các hợp đồng cung cấp AI có thể sớm bao gồm điều khoản về bằng chứng suy luận — đặc biệt với khách hàng cần tuân thủ quy định hoặc cần chắc chắn mô hình đắt tiền đã được dùng đúng như cam kết. Các nhóm làm sản phẩm AI tại Việt Nam nên theo dõi hướng này, ít nhất để hiểu rằng "tin vào output" sẽ dần được thay bằng "kiểm chứng output".