PSI công bố chứng minh giả thuyết Aaronson-Ambainis được kiểm chứng bằng máy

Physical Superintelligence thông báo vào ngày 6 tháng 11 năm 2026 rằng một hệ thống nghiên cứu nội bộ chạy các phiên bản của một mô hình Anthropic chưa công khai đã tìm ra chứng minh cho giả thuyết Aaronson-Ambainis, một bài toán về máy tính lượng tử vẫn chưa được giải quyết kể từ năm 2008.

Hệ thống tạo ra một chứng minh hoàn chỉnh vào ngày thứ ba của quá trình chạy trên hạ tầng riêng của PSI, và trợ lý chứng minh Lean đã chấp nhận chứng minh đó. Sau đó, PSI giao cho hệ thống các bài toán mở có liên quan; hệ thống cải thiện kết quả hai lần trước khi Lean chấp nhận phiên bản cuối cùng. Bản thảo và bản hình thức hóa bằng Lean 4 được công khai.

Giả thuyết nói gì về khả năng tăng tốc lượng tử

Câu hỏi đặt ra là khi nào máy tính lượng tử có thể nhanh hơn máy tính cổ điển theo cấp số nhân. Thuật toán phân tích thừa số năm 1994 của Shor dựa vào cấu trúc: đầu vào chứa một quy luật lặp lại mà thuật toán có thể khai thác. Kết quả của PSI đề cập đến trường hợp đối lập, với đầu vào ngẫu nhiên hoặc không có cấu trúc, vốn thường không có quy luật như vậy.

Trong mô hình truy vấn, thuật toán cổ điển đọc một bit ở mỗi truy vấn, còn một truy vấn lượng tử có thể được trải rộng dưới dạng chồng chập trên nhiều vị trí của đầu vào. Phần giải thích của PSI liên hệ mô hình này với đa thức: sau T truy vấn lượng tử, xác suất thuật toán trả lời có là một đa thức bị chặn theo các bit đầu vào, có bậc tối đa là 2T. Vì vậy, mô phỏng thuật toán lượng tử trở thành bài toán ước lượng đa thức đó mà không cần đọc số bit đầu vào tăng theo cấp số nhân.

Trong bài báo ban đầu, Scott Aaronson và Andris Ambainis đưa ra giả thuyết rằng mọi đa thức bậc thấp bị chặn đều có một biến có ảnh hưởng rất lớn. Họ chứng minh rằng, nếu giả thuyết này đúng, mọi thuật toán lượng tử T truy vấn đều có thể được mô phỏng trên hầu hết đầu vào bằng một thuật toán cổ điển thực hiện số truy vấn đa thức theo T. Hệ quả là số truy vấn cổ điển tăng theo đa thức, chứ không phải theo cấp số nhân, với mọi sai số xấp xỉ và tỷ lệ đầu vào bị loại trừ cố định; kết quả này không loại trừ khả năng máy tính lượng tử có ưu thế theo cấp số nhân đối với những bài toán có cấu trúc phù hợp.

Về mặt hình thức, kho lưu trữ xét một đa thức thực p có bậc tối đa là d, với giá trị nằm trong khoảng từ 0 đến 1 trên khối lập phương rời rạc. Nếu phương sai của đa thức trên đầu vào ngẫu nhiên phân bố đều ít nhất bằng ε, thì có một tọa độ có độ ảnh hưởng ít nhất là (8√15 / (125π⁴)) · ε^(5/2) / d⁶, và do đó ít nhất là (ε/d)⁷. Độ ảnh hưởng là mức thay đổi bình phương kỳ vọng của p khi bit ở tọa độ đó bị đảo.

Quá trình xây dựng và kiểm chứng chứng minh

Lập luận này dựa trên kế hoạch của Shachar Lovett và Jiapeng Zhang, vốn sử dụng các chứng chỉ phân số và các tập mức, nhưng thay thế một bất đẳng thức mà kế hoạch đó để ngỏ dưới dạng giả thuyết bằng một bất đẳng thức mới áp dụng cho mọi cặp. Một định thức tạo ra phép ghép một-một giữa các cấu hình đầu vào. PSI cho biết phép ghép này vượt trội hơn phép ghép trong Bổ đề Cánh bướm yếu hơn của David Reimer, vì nó còn giới hạn số lần các cấu hình được ghép có cùng giá trị ở mỗi tọa độ — một giới hạn cần thiết cho bất đẳng thức mới.

Kho lưu trữ chia chứng minh sơ cấp thành bốn phần: suy ra bất đẳng thức cho mọi cặp từ định thức và phép song ánh; lấy tích phân trên các tập mức; tính trung bình theo các tọa độ; và thiết lập một chặn cho hàng bằng một chặn độ nhạy tại từng điểm. Kết hợp lại, các bước này cho ra chặn tường minh về độ ảnh hưởng.

Theo bản kiểm toán được ghi lại trong kho lưu trữ, quá trình phát triển hình thức không có chỗ giữ chỗ cho chứng minh hay tiên đề được bổ sung. Các khai báo của chứng minh được kiểm tra lại qua kernel của Lean và lean4lean, một bản triển khai độc lập của bộ kiểm tra kiểu Lean. Trong một lần chạy trong môi trường hộp cát, chương trình đối chiếu sử dụng kernel nanoda và Lean đã chấp nhận bốn định lý cuối cùng; trên một máy thứ hai, chương trình chấp nhận một lời giải nhỏ đúng và bác bỏ bốn lời giải cố ý sai.

Những bước kiểm tra này có các giới hạn rõ ràng. Người đọc vẫn phải xác nhận rằng phát biểu hình thức khớp với giả thuyết đã được công bố. Bài báo viết cho người đọc không được tự thân kiểm chứng bằng máy; trong khi đó, kernel và trình biên dịch của Lean, các định nghĩa của Mathlib và những máy được dùng để kiểm tra vẫn là một phần của nền tảng tin cậy.

Vai trò của con người và đánh giá của chuyên gia

David Turturean, thành viên đội ngũ kỹ thuật của PSI, đã phát triển và vận hành hệ thống nghiên cứu, xác định phạm vi bài toán, hướng dẫn mô hình đóng gói bản nháp đầu tiên, xem xét bản nháp đó và chịu trách nhiệm về tính chính xác của bài báo. Kho lưu trữ nêu rõ rằng các mô hình AI đã tạo ra các phát biểu toán học, bản nháp đầu tiên và bản hình thức hóa bằng Lean. Jim Halverson đã kiểm tra chứng minh, còn Phiala Shanahan nhận xét về bản hình thức hóa.

Thông báo này được đưa ra sau bài báo nộp ngày 19 tháng 8 năm 2026 của Guy Blanc, Jordan Docter, Carmen Strassle và Li-Yang Tan. Các tác giả đó đã giải quyết hệ quả về mô phỏng cổ điển đối với các thuật toán lượng tử song song, chứng minh rằng một thuật toán có t truy vấn và d vòng có thể được mô phỏng trên hầu hết đầu vào bằng t^(O(d²)) truy vấn cổ điển. PSI cho biết cả bốn tác giả đều đã đọc toàn bộ chứng minh, gửi nhận xét và đang chuẩn bị một bản trình bày ngắn gọn hơn dành cho chuyên gia.

Trong đánh giá được PSI công bố, các nhà nghiên cứu viết: “Đây là một kết quả vô cùng quan trọng. Nó giải quyết một phỏng đoán có từ hàng chục năm trước, với những hệ quả quan trọng đối với bản chất của các bài toán có thể đạt được tăng tốc lượng tử. Chứng minh này dựa trên và mở rộng một số hướng nghiên cứu trong lĩnh vực phân tích hàm Boolean và tổ hợp xác suất. Mọi thứ được kết hợp với nhau theo một cách khá kỳ diệu.”

Phép thử trước mắt có tính cụ thể khác thường: các kernel độc lập có thể chạy lại lập luận đã được mã hóa, trong khi các chuyên gia vẫn cần xác nhận rằng mệnh đề được mã hóa khớp với phỏng đoán của Aaronson và Ambainis, đồng thời đánh giá những phần của bài báo nằm ngoài Lean. Sự phân chia đó quyết định những gì các bước kiểm tra bằng máy xác lập được và những gì vẫn cần đến sự thẩm định toán học của con người.