AlphaProof Nexus của Google DeepMind giải quyết các bài toán toán học tồn tại hàng thập kỷ chỉ với vài trăm USD.

NGHIÊN CỨU AI Google Deepmind's AlphaProof Nexus giải quyết các bài toán toán học tồn đọng hàng thập kỷ chỉ với vài trăm đô la. Matthias Bastian Ngày 25/5/2026 GPT-Image-2 được tạo bởi THE DECODER Những điểm chính Google Deepmind đã phát triển AlphaProof Nexus, một khuôn khổ tự động giải quyết 9 trong số 353 bài toán Erdős mở cùng với các giả thuyết phức tạp khác, với chi phí suy luận chỉ vài trăm đô la cho mỗi bài toán. Hệ thống này dựa vào mô hình ngôn ngữ Gemini 3.1 Pro để tạo ra các bước chứng minh bằng Lean, một ngôn ngữ lập trình hình thức được sử dụng để xác minh toán học, cho phép đưa ra các giải pháp chặt chẽ và có thể kiểm tra bằng máy. Mặc dù phần lớn các bài toán Erdős vẫn nằm ngoài khả năng của AI, các nhà nghiên cứu của Deepmind coi hệ thống này là một công cụ có giá trị để hỗ trợ nghiên cứu toán học. AlphaProof Nexus kết hợp việc tạo chứng minh dựa trên LLM với xác minh bằng máy để giải quyết các bài toán nghiên cứu toán học đã làm khó các nhà toán học trong nhiều thập kỷ. Khuôn khổ mới AlphaProof Nexus của Google Deepmind đã tự động giải quyết 9 trong số 353 bài toán Erdős mở mà nó đã thử, bao gồm hai câu hỏi đã không có lời giải trong 56 năm. Hệ thống này cũng đã chứng minh 44 trong số 492 giả thuyết mở từ Bách khoa toàn thư trực tuyến về các dãy số nguyên (OEIS), giải quyết một câu hỏi tồn đọng 15 năm về các hàm Hilbert trong hình học đại số, và cải thiện một giới hạn đã biết trong tối ưu hóa lồi. Chi phí suy luận chỉ vài trăm đô la cho mỗi bài toán, theo báo cáo nghiên cứu. Không giống như các phương pháp (có thể) chỉ dựa vào ngôn ngữ tự nhiên như giải pháp gần đây của OpenAI, mô hình ngôn ngữ cơ bản trong AlphaProof Nexus – trong trường hợp này là Gemini 3.1 Pro – không phải tự mình thực hiện toàn bộ chuỗi logic. Thay vào đó, nó tạo ra các bước chứng minh bằng ngôn ngữ hình thức của Lean, và trình biên dịch kiểm tra từng bước. Các thông báo lỗi được đưa trực tiếp trở lại cho lần thử tiếp theo. Bằng cách đó, LLM được củng cố bởi phản hồi tượng trưng, một mạng lưới an toàn bù đắp những điểm yếu đã biết của các mô hình ngôn ngữ khi nói đến lý luận logic. Con người chỉ can thiệp vào cuối cùng để kiểm tra kết quả. Bốn tác nhân, một kết quả đáng ngạc nhiên Hệ thống bao gồm bốn biến thể tác nhân với độ phức tạp tăng dần. Đơn giản nhất, Tác nhân (A), triển khai các tác nhân phụ độc lập chạy trên Gemini 3.1 Pro theo các vòng lặp: mô hình ngôn ngữ tạo ra các bước chứng minh, trình biên dịch Lean kiểm tra chúng, và các thông báo lỗi được đưa trở lại cho lần thử tiếp theo. Tác nhân (B) bổ sung các truy vấn vào AlphaProof, hệ thống dựa trên học tăng cường của Google cho toán học Olympic, có thể điền vào các đoạn chứng minh còn thiếu. Tác nhân (C) giới thiệu một thành phần tiến hóa. Lấy cảm hứng từ AlphaEvolve, các tác nhân phụ chia sẻ một tập hợp chung các bản phác thảo chứng minh. Các tác nhân đánh giá được xây dựng trên Gemini 3.0 Flash chấm điểm các bản phác thảo này về tính hợp lý và tính mới, sau đó xếp hạng chúng bằng hệ thống Elo. Tác nhân (D) được trang bị đầy đủ kết hợp tất cả các khả năng này. Tác nhân (D) đã được sử dụng cho các bài toán Erdős. Nhưng một phân tích hậu kỳ đã đưa ra một bất ngờ: Tác nhân (A) đơn giản nhất, chỉ sử dụng LLM và phản hồi của trình biên dịch, cũng có thể chứng minh tất cả chín bài toán Erdős đã được giải, mặc dù tốn kém hơn đối với những bài khó nhất. Các nhà nghiên cứu cho rằng thành công của tác nhân đơn giản là nhờ hai yếu tố: sự cải thiện nhanh chóng của các mô hình ngôn ngữ nền tảng và "sức mạnh của phản hồi từ trình biên dịch trong việc định hướng suy luận của LLM". Hiện tại, tác nhân được trang bị đầy đủ vẫn chiếm ưu thế trong các tác vụ khó nhất, nhưng lợi thế đó có thể thu hẹp khi các LLM ngày càng tốt hơn. Các nhà nghiên cứu cho rằng điều này cho thấy một xu hướng rộng hơn, mô tả "một sự chuyển dịch liên tục từ các hệ thống được đào tạo chuyên biệt sang các vòng lặp tác nhân đơn giản khi các LLM trở nên có năng lực hơn". Tỷ lệ giải quyết so với chi phí cho sáu trong số chín bài toán Erdős đã được giải: Đối với các tác vụ dễ hơn như erdos_26, cả bốn biến thể tác nhân đều đạt tỷ lệ thành công cao. Đối với các bài toán khó hơn như erdos_125 hoặc erdos_152, xuất hiện những khoảng cách rõ ràng. Tác nhân được trang bị đầy đủ (D) đôi khi đạt được kết quả với ít lần thử hơn, nhưng tác nhân đơn giản (A) cũng thành công nếu có đủ ngân sách. | Hình ảnh: Tsoukalas et al. **Hữu ích ngay cả khi không có bằng chứng hoàn chỉnh** Thành công của hệ thống tập trung vào các lĩnh vực như tổ hợp, tối ưu hóa lồi và lý thuyết số, nơi thư viện toán học Mathlib của Lean đã trưởng thành và các bài toán được chia thành các mục tiêu phụ có thể quản lý được. Hầu hết các bài toán Erdős vẫn nằm ngoài tầm với, "chưa kể đến các bài toán đòi hỏi lý thuyết mới rộng lớn", các nhà nghiên cứu viết. Các tác nhân cũng thừa hưởng sự không đáng tin cậy của các mô hình ngôn ngữ nền tảng. Tuy nhiên, họ nhận thấy giá trị vượt ra ngoài các bài toán đã được giải. Các nhà toán học làm việc với hệ thống báo cáo rằng ngay cả những nỗ lực chứng minh thất bại cũng làm sâu sắc thêm sự hiểu biết của họ về một bài toán, hoặc như các tác giả đã nói, "tìm kiếm bằng chứng hình thức do AI điều khiển không chỉ có thể phục vụ để giải quyết vấn đề mà còn để làm sâu sắc thêm sự hiểu biết của con người". Vì các bản phác thảo là hình thức, các chuyên gia có thể tập trung vào các mục tiêu phụ chưa được giải quyết thay vì kiểm tra lại toàn bộ lập luận từ đầu. Các tác nhân cũng chứng tỏ hiệu quả trong việc phát hiện các hình thức hóa sai sót trong tài liệu. "Xác minh hình thức có thể đóng vai trò là bộ lọc để xác định những bằng chứng nào xứng đáng được con người xem xét", các tác giả viết. Hệ thống này đã được sử dụng trong nghiên cứu đang diễn ra về quang học lượng tử và lý thuyết đồ thị, theo bài báo. Tất cả các bằng chứng Lean và các bằng chứng ngôn ngữ tự nhiên được chọn đều có sẵn trên GitHub. Cách AlphaProof Nexus giải bài toán Erdős #125: Tác nhân nhận một tệp Lean trong đó bằng chứng thực tế đã được thay thế bằng một khoảng trống (a), xem các lần thử trước với xếp hạng Elo và một kế hoạch hiện tại trong lời nhắc (b), sau đó chia nhỏ bằng chứng từng bước, gọi AlphaProof cho các mục tiêu phụ và tinh chỉnh các bước thất bại bằng cách phân tách chúng thành các bổ đề cho đến khi tất cả các mục tiêu được chứng minh (c). | Hình ảnh: Tsoukalas et al.