Gặp gỡ @duveZK, kỹ sư zkVM tại Nexus. Anh ấy đã học logic và khoa học máy tính, và hiện đang làm việc về xác minh chính thức, chứng minh không biết và hạ tầng hỗ trợ AI có thể xác minh.

Tanner tập trung vào việc xác minh chính thức cho AI. "Khi AI được triển khai trong các hệ thống quan trọng, đầu ra không đáng tin cậy có thể gây ra thảm họa. Độ chính xác có thể chứng minh có nghĩa là các đảm bảo chính thức và mật mã—để đảm bảo an toàn, quyền riêng tư và công bằng."

Ông ấy đặc biệt hào hứng với sự giao thoa giữa PL, AI và ZK. "Có một động lực thực sự trong việc sử dụng AI để hỗ trợ xác minh chính thức—đào tạo LLM trên dữ liệu Lean để tạo ra toán học và phần mềm đã được xác minh."

Đọc toàn bộ cuộc phỏng vấn tại đây: