PSI công bố chứng minh giả thuyết tính toán lượng tử được nêu năm 2008 bằng mô hình Anthropic

Công ty nghiên cứu AI Physical Superintelligence (PSI) công bố chứng minh giả thuyết Aaronson–Ambainis, được nêu năm 2008. Kết quả cho thấy trong một dạng bài toán với đầu vào ngẫu nhiên, máy tính lượng tử không thể giảm số lần truy vấn đầu vào theo cấp số nhân.

Trong công bố ngày 6, PSI cho biết hệ thống nghiên cứu chạy trên hạ tầng riêng đã sử dụng một mô hình Anthropic chưa được nêu tên. Hệ thống dùng nhiều phiên chạy của cùng mô hình, tạo ra chứng minh hoàn chỉnh vào ngày thứ ba và vượt qua kiểm tra bằng Lean.

PSI cho biết sau đó họ tiếp tục giao bài toán cho hệ thống và cải thiện kết quả hai lần. Phiên bản cuối cùng cũng vượt qua kiểm tra Lean. Công ty không tiết lộ tên cụ thể của mô hình được sử dụng.

Giả thuyết do Scott Aaronson và Andris Ambainis nêu ra đặt câu hỏi liệu máy tính lượng tử có thể giảm số lần đọc đầu vào theo cấp số nhân so với máy tính thông thường khi xử lý dữ liệu ngẫu nhiên, không có cấu trúc đặc biệt hay không. Đầu vào trong bài toán là một chuỗi dài gồm các bit 0 và 1; phép tính dùng chuỗi này để đưa ra câu trả lời 'có' hoặc 'không'.

Máy tính thông thường đọc một bit của chuỗi mỗi lần truy vấn. Thuật toán lượng tử có thể dùng trạng thái chồng chập trên nhiều vị trí để xử lý thông tin từ nhiều vị trí trong một lần truy vấn.

Xác suất thuật toán lượng tử trả lời 'có' có thể được biểu diễn bằng một đa thức của các bit đầu vào. PSI xây dựng chứng minh dựa trên kết quả nghiên cứu trước đó, theo đó đa thức biểu diễn xác suất này có bậc không vượt quá hai lần số lượt truy vấn.

Theo chứng minh, máy tính thông thường có thể xấp xỉ xác suất trả lời của thuật toán lượng tử với sai số nhỏ trên phần lớn các chuỗi ngẫu nhiên. Số lượt truy vấn cần thiết chỉ tăng theo một đa thức bậc cố định của số lượt truy vấn mà thuật toán lượng tử sử dụng, thay vì tăng theo cấp số nhân.

Trọng tâm toán học của giả thuyết là 'mức ảnh hưởng' của một bit đầu vào lên đầu ra của đa thức. Mức ảnh hưởng được tính bằng bình phương độ thay đổi của đầu ra khi lật một bit, rồi lấy trung bình trên mọi đầu vào.

PSI đưa ra cận dưới cho thấy với một đa thức không hằng, bậc thấp và có giá trị trong khoảng từ 0 đến 1, tồn tại một bit đầu vào có mức ảnh hưởng ít nhất khoảng 0,0025 × v^2,5 / d^6. Trong đó, v là phương sai của đầu ra và d là bậc của đa thức.

Kết quả này không có nghĩa mọi phép tính của máy tính lượng tử đều không nhanh hơn. Đây là kết quả lý thuyết chỉ so sánh số lượt truy vấn đầu vào trong một dạng bài toán phân loại có hoặc không trên dữ liệu ngẫu nhiên.

Thuật toán Shor phân tích nhanh các số lớn thành thừa số nguyên tố bằng cách khai thác chu kỳ ẩn trong bài toán. PSI cho biết phần lớn trường hợp tăng tốc lượng tử nổi bật đã biết đều dựa vào cấu trúc như vậy, trong khi đầu vào ngẫu nhiên hầu như không có mẫu tương tự.

Tháng 8 năm 2026, các nhà nghiên cứu tại Đại học Stanford đã chứng minh một trường hợp đặc biệt của giả thuyết này đối với thuật toán lượng tử truy vấn đầu vào qua một số vòng song song cố định. PSI cho biết hiện có bốn nhà nghiên cứu đang xem xét toàn bộ chứng minh.

Trong thư gửi PSI, các nhà nghiên cứu đánh giá đây là “một thành tựu lớn giải quyết một giả thuyết đã tồn tại hàng chục năm”. Họ cũng cho biết chứng minh kết nối nhiều hướng nghiên cứu về phân tích hàm Boolean và tổ hợp xác suất.

PSI cho biết chứng minh được phát triển dựa trên cách tiếp cận của Shachar Lovett và Jiapeng Zhang. Nhóm nghiên cứu thay một bất đẳng thức mà hai nhà nghiên cứu này để lại bằng bất đẳng thức mới, rồi dùng định thức để ghép cặp các cấu hình đầu vào.

PSI cho biết người phụ trách nghiên cứu đã phát triển hệ thống, xác định bài toán để hệ thống thực hiện, xem xét bản thảo do AI viết và chịu trách nhiệm về tính chính xác. Một cố vấn đã kiểm tra chứng minh, còn một cố vấn khác xem xét phần hình thức hóa bằng Lean.

Bài báo và mã hình thức hóa bằng Lean đã được đăng trên kho mã nguồn công khai. Kho này cho biết mã không có chỗ giữ chỗ cho chứng minh còn thiếu hay tiên đề bổ sung, đồng thời đã được kiểm tra lại bằng hai cách triển khai nhân Lean độc lập.

Lean kiểm tra các mệnh đề được hình thức hóa trong mã và các bước logic của chứng minh. Kho mã nguồn lưu ý người đọc cần đối chiếu mệnh đề trong mã với định nghĩa bài toán để xác nhận nó khớp với giả thuyết ban đầu. ChainNews ABMedia đưa tin bài báo chưa trải qua phản biện học thuật. Một ví dụ khác về AI hình thức hóa bài toán toán học khó là việc OpenAI công bố chứng minh cho phương trình Navier–Stokes.