STARK: 3 bài toán mở ra khả năng giảm lượt kiểm tra từ 200 xuống 148

Ba bài toán toán học nhằm giảm số lượt kiểm tra trong các bằng chứng STARK đã được công bố. Trang bài toán đưa ra phép tính cho thấy, trong một số điều kiện nhất định, số lượt kiểm tra cần thiết để đạt mức bảo mật 100 bit có thể giảm từ 200 xuống 148. Con số này phụ thuộc vào việc chứng minh mục tiêu và phân tích đầy đủ tính bảo mật.

Trang bài toán chính thức của provably.fast nêu ba mục tiêu. Mỗi mệnh đề được cố định trong Lean, công cụ chứng minh định lý toán học; chỉ những chứng minh đã qua đánh giá độc lập mới được công nhận là lời giải. Hiện cả ba mục tiêu đều chưa được giải quyết.

STARK là hệ thống bằng chứng không tiết lộ kiến thức dựa trên hàm băm. Mã Reed–Solomon được dùng để xác minh độ tin cậy của dữ liệu trong hệ thống này. Bộ xác minh kiểm tra các tổ hợp ngẫu nhiên để xác nhận dữ liệu được gửi có đủ gần với một mã hợp lệ hay không.

Các bài toán tập trung giới hạn số “giá trị thử thách xấu” có thể khiến dữ liệu sai trông giống dữ liệu hợp lệ. Nếu giảm được giới hạn trên của các giá trị này, có cơ sở để giảm số lượt kiểm tra ngẫu nhiên cần thiết. Tuy nhiên, chỉ cải thiện giới hạn trên không đồng nghĩa kích thước bằng chứng hay mức bảo mật thực tế sẽ thay đổi.

Các mục tiêu được chia theo khoảng tỷ lệ đồng thuận của mã. T1 hướng tới việc hạ giới hạn trên bậc hai đã biết xuống giới hạn trên tuyến tính trong khoảng giữa ngưỡng bậc nhất và ngưỡng Johnson. T2 đặt mục tiêu chứng minh giới hạn trên bậc hai trên một phạm vi rộng hơn, nằm dưới ngưỡng bậc nhất.

T3 xem xét giới hạn trên của miền đánh giá dùng để tạo bằng chứng. Với trường hợp đầu tiên có tỷ lệ đồng thuận 5/8 và tỷ lệ 1/2, trang bài toán yêu cầu chứng minh giới hạn trên 16n trong điều kiện số giá trị thử thách xấu của cấu hình hiện tại có thể lên tới 114n/16.

Ví dụ về số lượt kiểm tra trên trang dựa vào các điều kiện cụ thể: phương pháp FRI, tỷ lệ 1/2, n=2²⁰ và trường 124 bit. Theo phép tính này, hiện cần 200 lượt kiểm tra để đạt mức bảo mật 100 bit; nếu trường hợp đầu tiên của T3 được chứng minh, con số có thể giảm xuống 148. Trang bài toán giải thích phép tính chỉ giới hạn ở số lượt kiểm tra và việc áp dụng thực tế cần phân tích đầy đủ tính bảo mật.

Nghiên cứu trước đây đã kết nối các giới hạn trên toán học với kích thước bằng chứng trong những triển khai thực tế. Bản thảo tiền ấn phẩm do Quang Dao, Scott Duke Kominers và Justin Thaler đăng ký ngày 17 tháng 9 báo cáo rằng, với cùng mục tiêu bảo mật, bằng chứng hộ chiếu ProveKit giảm 79.4KB (11.1%), bằng chứng cuối đã nén của ZisK giảm 13.2KB (4.63%) và bằng chứng phụ CPU của LambdaVM giảm 59.8KB (4.85%). Các kết quả này thuộc về những triển khai và cấu hình cụ thể trong bài nghiên cứu.

Phạm vi áp dụng vẫn có giới hạn. Một bài nghiên cứu riêng công bố ngày 9 tháng 10 đưa ra phản ví dụ cho thấy khoảng cách gần dưới ngưỡng Johnson không tồn tại trong trường nhị phân. Phần giải thích bối cảnh của các bài toán cho biết kết quả này không giải quyết hay bác bỏ các mục tiêu hiện tại, vốn đặt điều kiện trường có đặc số đủ lớn.

Cả con người lẫn tác nhân AI đều có thể tham gia các bài toán; những đóng góp như ý tưởng, bổ đề, phản ví dụ và chứng minh sẽ được ghi nhận. Việc công bố các kết quả toán học đã được hình thức hóa cũng đang tiếp diễn, chẳng hạn OpenAI công bố kết quả toán học từ các mô hình nội bộ cùng một phần hình thức hóa bằng Lean.

Hiện chưa có kết quả cho thấy cả ba bài toán đã được giải hoặc kích thước bằng chứng trong các triển khai STARK thực tế đã giảm thêm. Ngay cả khi chứng minh được các giới hạn trên toán học, vẫn cần phân tích riêng tính bảo mật và kích thước bằng chứng của giao thức được áp dụng để xác nhận hiệu quả thực tế.