AI tìm chương trình lượng tử đã kiểm chứng bằng Lean

Mốc thời gian máy tính lượng tử giải được các bài toán khoa học đột phá phụ thuộc vào cả phần cứng lẫn thuật lượng. Bản preprint ngày 6/11/2026 của Google DeepMind và Google Quantum AI (https://arxiv.org/abs/2611.09822) cho rằng cải tiến thuật lượng thường mất nhiều năm cộng tác chuyên gia, nên nhóm thử dùng mô hình ngôn ngữ lớn để rút ngắn vòng lặp tìm kiếm rồi kiểm chứng.

Nghiên cứu này làm gì

Thay vì chỉ thử nghiệm trên máy tính cổ điển với các trường hợp nhỏ, nhóm đặt mục tiêu tạo ra chương trình lượng tử mà hiện chưa máy nào kiểm thử được đầy đủ. Để làm vậy, họ xây một thư viện chương trình lượng tử ngay trong trình chứng minh định lý Lean. Các tác tử mô hình ngôn ngữ lớn đề xuất chương trình mới theo một đặc tả vấn đề đã được hình thức hóa, rồi hệ thống tự kiểm tra tính đúng đắn và ước lượng chi phí. Chương trình đạt yêu cầu mới được ghi nhận, còn lỗi hoặc thiếu bằng chứng thì bị loại.

Bản chất cách đánh giá này là thay thế việc chạy thử bằng bằng chứng toán học. Thay vì quan sát chương trình chạy ra sao trên vài ví dụ cổ điển, nhóm yêu cầu một bản chứng minh xác nhận rằng chương trình thực hiện đúng phép biến đổi đã nêu với sai số cho trước. Việc tính toán chi phí cũng nằm trong chứng minh: số qubit, số cổng T và cổng Toffoli được xác định ở mức cổng cụ thể. Tác giả xem đó là lý do kết quả có thể tin cậy hơn mô phỏng thuần túy.

Họ kiểm chứng và cộng tác thế nào?

Thư viện Lean và đặc tả chính thức

Mọi chương trình trong thư viện được biên dịch xuống mức cổng, gồm cổng Clifford+T, đo ở giữa mạch và truyền tín hiệu cổ điển, rồi được chứng minh đúng ở mức đó. Đặc tả nêu điều kiện phải thỏa: phép biến đổi tìm được phải xấp xỉ phép lý thuyết theo sai số ε = 10^-2 với mọi trạng thái hợp lệ, còn mọi qubit trung gian bắt đầu ở trạng thái |0⟩ mỗi lần chạy, không mang theo trạng thái tài nguyên chuẩn bị sẵn từ lần trước. Với mô phỏng động lực dừng, bài còn nêu rõ thành phần hệ thống gồm electron, proton và tham số lưới.

Nhiều tác tử cùng làm việc

Nhóm mô tả các tác tử làm việc theo đội, chia sẻ kết quả và kiến thức qua một wiki nội bộ, đồng thời trình bày ý tưởng trong những hội nghị mà hệ thống tổ chức. Ở chiều khác, kết quả được đối chiếu với chương trình tham khảo đã biết và kiểm tra bằng chạy số trên máy tính cổ điển khi vẫn làm được. Khi bài toán vượt quá khả năng mô phỏng cổ điển, phần việc còn lại là đưa ra bằng chứng hình thức đủ mạnh để chấp nhận hoặc từ chối một ứng viên.

Kết quả nhóm báo cáo

Nhóm nêu các mức cải thiện so với mốc tham chiếu trước đó: tìm kiếm song song tăng tới 1,4 lần; toán học lượng tử đạt 290 lần; các mô phỏng liên quan tới phản ứng tổng hợp hạt nhân, quang hóa học và chuyển hóa thuốc lần lượt tốt hơn 11, 8 và 2,5 lần. Những con số này do chính tác giả báo cáo, dùng để so sánh chi phí với mốc trước đây, không phải hiệu năng đo trên máy lượng tử. Bài cũng đưa ra các bài toán ở quy mô mà máy tính cổ điển khó kiểm thử trực tiếp, như mô phỏng động lực dừng hay hệ men Cytochrome P450.

Một ví dụ chi phí: mạch arcsin

Bảng số liệu trong bài lấy mạch tính hàm arcsin làm ví dụ. Mốc tham chiếu, vốn là giới hạn dưới, dùng 110.144 cổng Toffoli, 440.576 cổng T và 245 qubit, tương đương chi phí không gian–thời gian khoảng 1,08×10^8. Phiên bản Kickmix giảm còn 1.038 Toffoli và 4.152 cổng T trên 100 qubit; bản viết lại bằng Lean 4 còn xuống 776 Toffoli và 3.698 cổng T. Bài giải thích phần lớn cổng T tiêu vào khâu tra hệ số, và cách viết lại dùng mạch tích trong để cắt bớt chi phí này.

Ý nghĩa thực tế theo bài

Bài đặt kết quả trong bối cảnh nhiều ứng dụng tiềm năng được ước tính cần hàng nghìn qubit logic đã hiệu chỉnh, chạy từ 10^9 tới 10^15 phép logic, trong khi bộ xử lý chịu lỗi sớm mới ở khoảng một triệu phép. Theo tác giả, thu hẹp khoảng cách này phụ thuộc vào việc giảm dần số qubit và số cổng mà mỗi thuật toán tiêu tốn, bên cạnh việc cải thiện phần cứng và hiệu chính lỗi. Các chương trình có chi phí thấp hơn, dù mới ở dạng chứng minh, được xem là đóng góp cho hướng đó.

Mặt khác, tác giả nhấn mạnh việc kết hợp trí tuệ con người và trí tuệ nhân tạo ở quy mô lớn, nhưng vẫn đặt dưới sự chặt chẽ của chứng minh toán học. Con người cung cấp ý tưởng, nhận xét và các kiểm tra số, còn hệ thống tự động hoá vòng lặp đề xuất, chứng minh và phản hồi. Theo nhóm, cách này cho phép thiết kế thuật toán ngay cả khi chưa máy tính nào, cổ điển hay lượng tử, đủ sức chạy thử chúng, rút ngắn con đường tới tính toán lượng tử thực dụng.

Giới hạn cần ghi nhớ

Trước hết, đây là bản preprint: bài được gửi lên arXiv ngày 6/11/2026 với mã 2611.09822v1 và không nêu tạp chí hay hội nghị đã phản biện, nên kết quả chưa qua đánh giá độc lập của giới chuyên môn. Thứ hai, các mức cải thiện là so với mốc tham chiếu do bài xác định, không phải so sánh với phần cứng lượng tử đang vận hành. Bài cũng không báo cáo việc chạy các chương trình tìm được trên máy lượng tử thật, nên đây là một kết quả đang chờ kiểm chứng.

Phần nội dung được cung cấp không trình bày thời gian, chi phí tính toán hay số lượng con người để vận hành toàn bộ quy trình, cũng không so sánh với phương pháp tìm kiếm thuật toán khác ngoài các mốc đã nêu. Mức tổng quát của thư viện Lean khi mở rộng sang bài toán lớn hơn vẫn là câu hỏi chưa có trả lời. Vì vậy, nên xem đây là kết quả sơ bộ đang chờ phản biện, với tài liệu đầy đủ tại https://arxiv.org/abs/2611.09822. Các con số trong bài vì vậy cần được đọc kèm bối cảnh này.

Nguồn tham khảo

Shirobokov, S., Jaderberg, B., Hristova, K. và cộng sự, Discovering formally verified quantum programs with AI, bản preprint arXiv:2611.09822v1, 6/11/2026: https://arxiv.org/abs/2611.09822
Bài viết khác: /blog/ · Sổ tay hạ tầng AI: /books/ai-infra-book/

Đọc thêm các bài công nghệ khác và sách AI Infra mã nguồn mở.