Scott Aaronson tin chứng minh do AI tạo ra là đúng, thuật toán Shor không bị ảnh hưởng

Scott Aaronson, đồng đề xuất giả thuyết Aaronson–Ambainis, tin rằng chứng minh do một hệ thống nghiên cứu trí tuệ nhân tạo (AI) tạo ra là đúng. Tuy nhiên, ông cho biết chưa hiểu đầy đủ toàn bộ chứng minh.

Ngày 8, Aaronson viết trên blog cá nhân: “Tôi tin rằng chứng minh là đúng”. Ông cho biết cơ sở cho niềm tin này gồm chứng chỉ Lean kiểm tra từng bước trong chứng minh và việc các nhà nghiên cứu đã xem xét nội dung.

Công ty nghiên cứu AI Physical Superintelligence (PSI) thông báo ngày 6 rằng hệ thống nghiên cứu của mình đã tạo ra chứng minh bằng một mô hình Anthropic chưa được công khai. Hệ thống hoàn tất toàn bộ chứng minh vào ngày thứ ba hoạt động; PSI cho biết sau đó đã cải thiện cận dưới hai lần. TokenPost trước đó đã đưa tin về công bố của PSI.

Tên cụ thể của mô hình chưa được công bố. Aaronson nói ông chưa biết hệ thống nghiên cứu AI và mô hình được dùng bên trong đóng góp bao nhiêu vào chứng minh.

Giả thuyết Aaronson–Ambainis so sánh số lần truy vấn đầu vào của thuật toán lượng tử và thuật toán thông thường khi đầu vào được chọn ngẫu nhiên, không theo quy tắc đặc biệt nào. Nghiên cứu xem xét liệu thuật toán thông thường có thể dùng ít truy vấn hơn đến mức nào để xấp xỉ xác suất trả lời “có” hoặc “không” của thuật toán lượng tử.

Cần phân biệt thời điểm bài toán được nêu ra với thời điểm bài báo được công bố. PSI mô tả giả thuyết này là một bài toán mở từ năm 2008, nhưng bài báo gốc của Aaronson và Andris Ambainis lần đầu được đăng trên arXiv ngày 5 tháng 11 năm 2009.

Phần giải thích nghiên cứu của PSI trình bày định lý rằng một đa thức bị chặn bậc d, có phương sai ít nhất ε, phải có ít nhất một biến có mức ảnh hưởng đáng kể. Cận dưới cho mức ảnh hưởng đó là (8√15/(125π⁴))·ε^(5/2)/d⁶; một cận dưới đơn giản hơn cũng được nêu là (ε/d)^7.

Mức ảnh hưởng của một biến cho biết đầu ra của đa thức thay đổi ra sao khi một bit đầu vào bị đổi. Định lý này không xét liệu máy tính lượng tử có nhanh hơn máy tính thông thường trong mọi phép tính hay không, mà tập trung vào những điều kiện cụ thể về đầu vào và độ phức tạp truy vấn.

Lean là công cụ cho phép viết các mệnh đề và chứng minh toán học bằng ngôn ngữ hình thức, rồi dùng máy tính kiểm tra chúng có tuân theo quy tắc logic hay không. Kho lưu trữ công khai của PSI cho biết Lean đã kiểm tra mệnh đề và chứng minh được hình thức hóa.

Tuy vậy, kho lưu trữ lưu ý người đọc cần tự đối chiếu để xác định mệnh đề hình thức có diễn đạt chính xác giả thuyết ban đầu hay không. Vì vậy, Lean kiểm tra mối liên hệ logic giữa mệnh đề và chứng minh đã nhập vào, chứ không tự động bảo đảm quá trình chuyển bài toán sang ngôn ngữ hình thức là chính xác.

Ngày 7, nhà nghiên cứu Guy Blanc tại MIT cùng các nhà nghiên cứu Jordan Docter, Carmen Strassle và Li-Yang Tan tại Đại học Stanford công bố một bài giải thích logic của chứng minh. Họ cho biết đã nhận chứng minh từ PSI, xem xét nội dung rồi soạn bài giải thích.

Nhóm nghiên cứu cho biết họ cũng dùng một mô hình Anthropic được công khai trong quá trình soạn bài. Họ nói không nhận thù lao từ PSI hay Anthropic.

Các nhà nghiên cứu cho biết không có kế hoạch gửi bài giải thích tới hội nghị hoặc tạp chí học thuật. Việc bài giải thích được công bố không đồng nghĩa chứng minh đã vượt qua bình duyệt.

Aaronson nhấn mạnh không nên diễn giải kết quả này thành tuyên bố rằng ưu thế lượng tử nói chung đã biến mất. Nghiên cứu chỉ tập trung vào một bài toán phán định cụ thể với đầu vào ngẫu nhiên và độ phức tạp truy vấn lượng tử.

Ông giải thích kết quả không ảnh hưởng đến thuật toán Shor dùng để phân tích thừa số nguyên tố, cũng như các mô phỏng lượng tử trong vật lý và hóa học. Nghiên cứu cũng không đánh giá độ an toàn của công nghệ mật mã trong lĩnh vực tài sản mã hóa.

Phạm vi nghiên cứu là chứng minh một giả thuyết toán học cụ thể và kiểm tra hình thức hóa. Nghiên cứu không nêu mối liên hệ trực tiếp với ngành bán dẫn.