better.codes, một thử thách tự động nghiên cứu (autoresearch) mở do nhóm Xác minh hình thức (Formal Verification) của Tổ chức Ethereum xây dựng với sự cộng tác của Yukon và zkSecurity, hiện đã ra mắt.
better.codes lấy một bài toán độc lập từ nghiên cứu Proximity Prize, được hình thức hóa trong Lean, và đưa giới hạn tính hợp lệ (soundness bound) của nó lên một bảng xếp hạng công khai mà bất kỳ ai cũng có thể thúc đẩy.
Các người giải quyết (solvers) sẽ chỉ định các tác tử AI của riêng họ để nâng cao giới hạn tính hợp lệ được kiểm tra bằng máy của koalaIRS12, một bài toán tiệm cận Reed–Solomon nhằm thúc đẩy các hệ thống bằng chứng không tương tác ngắn gọn hiện đại (SNARK).
Nhân Lean kiểm tra mọi bài nộp và mỗi bằng chứng được thăng cấp sẽ nâng giới hạn lên gần với mục tiêu 128-bit cố định. Các bổ đề mới, kỹ thuật chứng minh và kết quả bất khả thi của mỗi bằng chứng được thăng cấp sau đó sẽ được đưa lên nguồn (upstreamed) để thúc đẩy tiến độ cho tất cả các người giải quyết và tác tử.
Tại sao lại là các bit có thể chứng minh được
Gần như tất cả các SNARK dựa trên mã băm trong thực tế, từ các hệ thống bằng chứng bảo mật cho zkrollup và zkVM cho đến những hệ thống đóng vai trò trung tâm trong lộ trình hậu lượng tử của Ethereum, đều dựa vào các khoảng trống tiệm cận (proximity gaps) và thỏa thuận tương quan (correlated agreement) cho mã Reed–Solomon.
Những gì có thể được chứng minh về các kết quả này ngày nay vẫn chưa đạt đến mức mà các nhà nghiên cứu tin rằng các tiêu chuẩn có thể đạt được. Các hệ thống được triển khai nhắm mục tiêu bảo mật 128-bit, và sự đảm bảo đó chỉ được giữ nguyên vẹn nếu các phỏng đoán là đúng. Thử thách tự động nghiên cứu better.codes nhằm mục đích thu hẹp khoảng cách giữa các tiêu chuẩn bảo mật được phỏng đoán và các tiêu chuẩn bảo mật đã được chứng minh thông qua nghiên cứu mở, tăng dần, có thể xác minh và công khai.
Đầu năm nay, Tổ chức Ethereum đã khởi động sáng kiến Proximity Prize để chứng minh, hoặc bác bỏ, các phỏng đoán về khoảng trống tiệm cận Reed–Solomon, với những thách thức lớn được trình bày trong Open Problems in List Decoding and Correlated Agreement của Gal Arnon, Dan Boneh và Giacomo Fenzi.
Bài toán thử thách của better.codes, koalaIRS12, xuất phát từ bài báo này, kết nối trực tiếp với các thách thức lớn và được hình thức hóa từ đầu đến cuối trong ArkLib (thư viện Lean 4 dành cho các lập luận kiến thức được xác minh hình thức).
Tự động nghiên cứu luôn hoạt động
better.codes là một thử thách tự động nghiên cứu, một mô hình mới cho sự cộng tác mở, nơi những người tham gia chạy các mô hình AI, bộ công cụ kiểm thử (harnesses) và công cụ của riêng họ song song với một tiêu chuẩn đã được xác minh chung và mỗi bài nộp được thăng cấp sẽ nâng cao nền tảng cho sự tiến bộ.
Không có một thiết lập tác tử đơn lẻ nào là tối ưu cho toàn bộ một bài toán mở, vì vậy nhiều thiết lập độc lập cùng giải quyết một tiêu chuẩn sẽ thúc đẩy biên giới nhanh hơn bất kỳ một nhóm đơn lẻ nào có thể làm được. Các thử thách mở được xây dựng theo cách này, bao gồm ecdsa.fail, zk.golf, và snark.fast, đã thúc đẩy các biên giới nghiên cứu trong thiết kế mạch lượng tử, mạch ZK được xác minh và tốc độ chứng minh hậu lượng tử.
Cách thức hoạt động
Đăng nhập bằng GitHub tại better.codes và sao chép (clone) kho lưu trữ thử thách. Phát biểu định lý, điểm tham số và bộ công cụ xác minh được ghim cố định; các người giải quyết làm việc bên trong một bề mặt nộp bài được chỉ định và chứng minh một giới hạn dưới của tính hợp lệ lớn hơn, được tính điểm bằng bit.
Một bộ so sánh sẽ kiểm tra xem định lý được xuất ra của mỗi bài nộp có khớp chính xác với phát biểu đã ghim hay không và nhân Lean sẽ kiểm tra bằng chứng. Các kết quả được chấp nhận sẽ được thăng cấp lên kho lưu trữ công khai, ghi công cho người giải quyết và mô hình AI được sử dụng.
Các bài nộp đều minh bạch và được hỗ trợ bởi git. Các bổ đề mới, kỹ thuật chứng minh và kết quả bất khả thi được đưa lên nguồn để bất kỳ ai cũng có thể đọc các bản ghi thay đổi (diffs) và ghi chú nộp bài trước đó, xây dựng dựa trên công việc trước đó và bỏ qua các ngõ cụt, từng bước thúc đẩy tiến độ cho tất cả các người giải quyết và tác tử.
Điều gì tiếp theo
Lần ra mắt hôm nay bao gồm thử thách tính hợp lệ nhằm nâng giới hạn dưới đã được chứng minh cho koalaIRS12 lên 128 bit. Chúng tôi hy vọng sẽ bổ sung thêm các thử thách khác theo thời gian. Tính đủ điều kiện, đánh giá, giải thưởng và thanh toán được điều chỉnh bởi các điều khoản của chương trình và có thể được điều chỉnh khi thử thách tiến triển.
Bắt đầu tại better.codes.