Các mô hình AI đang bắt đầu giải quyết các bài toán cấp cao

Cuối tuần qua, Neel Somani, một kỹ sư phần mềm, cựu nhà nghiên cứu lượng tử và là người sáng lập công ty khởi nghiệp, đang kiểm tra các kỹ năng toán học của mô hình mới của OpenAI thì anh ấy có một khám phá bất ngờ. Sau khi dán vấn đề vào ChatGPT và để nó suy nghĩ trong 15 phút, anh ấy đã đưa ra giải pháp đầy đủ. Anh ấy đã đánh giá bằng chứng và chính thức hóa nó bằng một công cụ có tên là Harmonic – nhưng tất cả đều được kiểm tra.

Somani nói: “Tôi tò mò muốn thiết lập một đường cơ sở về thời điểm LLM có thể giải quyết các bài toán mở một cách hiệu quả so với những gì họ gặp khó khăn”. Điều ngạc nhiên là khi sử dụng mẫu mới nhất, ranh giới bắt đầu được đẩy lên một chút.

Chuỗi suy nghĩ của ChatGPT thậm chí còn ấn tượng hơn, rung chuyển các tiên đề toán học như công thức Legendre, định đề Bertrand và định lý Ngôi sao David. Cuối cùng, mô hình này đã tìm thấy một bài đăng về Math Overflow từ năm 2013, nơi nhà toán học Harvard Noam Elkies đã đưa ra một giải pháp hay cho một vấn đề tương tự. Nhưng bằng chứng cuối cùng của ChatGPT khác với công trình của Elkies ở những điểm quan trọng và đưa ra giải pháp hoàn chỉnh hơn cho một phiên bản của bài toán do nhà toán học huyền thoại Paul Erdős đặt ra, người có bộ sưu tập khổng lồ các bài toán chưa được giải đã trở thành nền tảng chứng minh cho AI.

Đối với bất kỳ ai còn hoài nghi về trí thông minh của máy móc thì đó là một kết quả đáng ngạc nhiên – và nó không phải là kết quả duy nhất. Các công cụ AI đã trở nên phổ biến trong toán học, từ các LLM định hướng chính thức hóa như Aristotle của Harmonic đến các công cụ đánh giá tài liệu như nghiên cứu sâu của OpenAI. Nhưng kể từ khi phát hành GPT 5.2 — mà Somani mô tả là “có kỹ năng suy luận toán học tốt hơn so với các phiên bản trước đó” — khối lượng lớn các vấn đề được giải quyết đã trở nên khó bỏ qua, đặt ra những câu hỏi mới về khả năng của các mô hình ngôn ngữ lớn trong việc vượt qua giới hạn kiến ​​thức của con người.

Somani đang xem xét các bài toán Erdős, một tập hợp hơn một nghìn giả thuyết của nhà toán học Hungary được lưu giữ trực tuyến. Các bài toán đã trở thành mục tiêu hấp dẫn cho toán học do AI điều khiển, thay đổi đáng kể cả về chủ đề và độ khó. Lô giải pháp tự động đầu tiên xuất hiện vào tháng 11 từ một mô hình do Gemini cung cấp có tên là AlphaEvolve – nhưng gần đây hơn, Somani và những người khác đã nhận thấy GPT 5.2 rất thành thạo với toán học cấp cao.

Kể từ Giáng sinh, 15 vấn đề đã được chuyển từ “mở” sang “đã giải quyết” trên trang web Erdős – và 11 trong số các giải pháp đã ghi nhận cụ thể các mô hình AI đã tham gia vào quá trình này.

Nhà toán học đáng kính Terence Tao có cái nhìn sâu sắc hơn về tiến trình trên trang GitHub của mình, đếm tám vấn đề khác nhau trong đó các mô hình AI đã đạt được tiến bộ tự chủ có ý nghĩa đối với vấn đề Erdős, cùng với sáu trường hợp khác mà tiến trình được thực hiện bằng cách định vị và xây dựng dựa trên nghiên cứu trước đó. Còn lâu nữa các hệ thống AI mới có thể thực hiện toán học mà không cần sự can thiệp của con người, nhưng rõ ràng là các mô hình lớn có một vai trò quan trọng.

Trên Mastodon, Tao phỏng đoán rằng bản chất có thể mở rộng của hệ thống AI khiến chúng “phù hợp hơn để được áp dụng một cách có hệ thống cho ‘cái đuôi dài’ của các vấn đề khó hiểu của Erdő, nhiều vấn đề trong số đó thực sự có giải pháp đơn giản”.

Tao tiếp tục: “Do đó, nhiều vấn đề Erdős dễ dàng hơn này hiện có nhiều khả năng được giải quyết bằng các phương pháp hoàn toàn dựa trên AI hơn là bằng các phương pháp kết hợp hoặc con người”.

Một động lực khác là sự thay đổi gần đây theo hướng chính thức hóa, một nhiệm vụ tốn nhiều công sức giúp cho việc xác minh và mở rộng lý luận toán học trở nên dễ dàng hơn. Việc chính thức hóa không yêu cầu sử dụng AI hoặc thậm chí cả máy tính, nhưng một loạt công cụ tự động mới đã giúp quá trình này trở nên dễ dàng hơn nhiều. “Trợ lý chứng minh” mã nguồn mở Lean, được phát triển tại Microsoft Research vào năm 2013, đã được sử dụng rộng rãi trong lĩnh vực này như một cách chính thức hóa bằng chứng— và các công cụ AI như Aristotle của Harmonic hứa hẹn sẽ tự động hóa phần lớn công việc chính thức hóa.

Đối với người sáng lập Harmonic Tudor Achim, bước đột phá đột ngột trong việc giải quyết các bài toán Erdős không quan trọng bằng việc các nhà toán học vĩ đại nhất thế giới đang bắt đầu coi trọng những công cụ đó. Achim nói: “Tôi quan tâm nhiều hơn đến thực tế là các giáo sư toán và khoa học máy tính đang sử dụng (các công cụ AI). “Những người này có danh tiếng cần bảo vệ, vì vậy khi họ nói rằng họ sử dụng Aristotle hoặc họ sử dụng ChatGPT, đó là bằng chứng thực sự.”