Thúc đẩy nghiên cứu toán học bằng tìm kiếm chứng minh hình thức dựa trên AI

Khoa học Máy tính > Trí tuệ nhân tạo arXiv:2605.22763 (cs) [Đệ trình ngày 21/5/2026] Tiêu đề: Thúc đẩy nghiên cứu toán học bằng tìm kiếm chứng minh hình thức dựa trên AI Tác giả: George Tsoukalas, Anton Kovsharov, Sergey Shirobokov, Anja Surina, Moritz Firsching, Gergely Bérczi, Francisco J. R. Ruiz, Arun Suggala, Adam Zsolt Wagner, Eric Wieser, Lei Yu, Aja Huang, Miklós Z. Horváth, Andrew Ferrauiolo, Henryk Michalewski, Codrut Grosu, Thomas Hubert, Matej Balog, Pushmeet Kohli, Swarat Chaudhuri Xem bản PDF của bài báo có tiêu đề "Thúc đẩy nghiên cứu toán học bằng tìm kiếm chứng minh hình thức dựa trên AI", của George Tsoukalas và 19 tác giả khác Xem PDF HTML (thử nghiệm) Tóm tắt: Các mô hình ngôn ngữ lớn (LLM) ngày càng xuất sắc trong lập luận toán học, nhưng độ tin cậy hạn chế của chúng đã làm giảm tiện ích trong nghiên cứu toán học. Một giải pháp giảm thiểu là sử dụng LLM để tạo ra các chứng minh hình thức bằng các ngôn ngữ như Lean. Chúng tôi thực hiện đánh giá quy mô lớn đầu tiên về khả năng của phương pháp này trong việc giải quyết các bài toán mở. Tác nhân có năng lực nhất của chúng tôi đã tự động giải quyết 9 trong số 353 bài toán Erdős mở với chi phí vài trăm đô la cho mỗi bài toán, chứng minh 44/492 giả thuyết OEIS và đang được triển khai trong nghiên cứu tổ hợp, tối ưu hóa, lý thuyết đồ thị, hình học đại số và quang học lượng tử. Một tác nhân cơ bản xen kẽ giữa việc tạo ra dựa trên LLM và xác minh dựa trên Lean đã tái tạo thành công các bài toán Erdős nhưng tốn kém hơn đối với các bài toán khó nhất. Những phát hiện này chứng minh sức mạnh của tìm kiếm chứng minh hình thức có sự hỗ trợ của AI và làm sáng tỏ các thiết kế tác nhân cho phép điều đó. Bình luận: Ba tác giả đầu tiên và tác giả cuối cùng có đóng góp ngang nhau. Ba tác giả đầu tiên được sắp xếp ngẫu nhiên. Chủ đề: Trí tuệ nhân tạo (cs.AI) Trích dẫn: arXiv:2605.22763 [cs.AI] (hoặc arXiv:2605.22763v1 [cs.AI] cho phiên bản này) https://doi.org/10.48550/arXiv.2605.22763 Tập trung để tìm hiểu thêm DOI do arXiv cấp thông qua DataCite (đang chờ đăng ký) Lịch sử đệ trình Từ: Swarat Chaudhuri [xem email] [v1] Thứ Năm, 21/5/2026 17:24:57 UTC (1.291 KB) Liên kết toàn văn: Truy cập bài báo: Xem bản PDF của bài báo có tiêu đề "Thúc đẩy nghiên cứu toán học bằng tìm kiếm chứng minh hình thức dựa trên AI", của George Tsoukalas và 19 tác giả khác Xem PDF HTML (thử nghiệm) Nguồn TeX xem giấy phép Ngữ cảnh duyệt hiện tại: cs.AI < trước | tiếp theo > mới | gần đây | 2026-05 Thay đổi để duyệt theo: cs Tài liệu tham khảo & Trích dẫn NASA ADS Google Scholar Semantic Scholar xuất trích dẫn BibTeX Đang tải... Trích dẫn định dạng BibTeX &times; đang tải... Dữ liệu được cung cấp bởi: Đánh dấu Công cụ thư mục Công cụ thư mục và trích dẫn Chuyển đổi Trình khám phá thư mục Trình khám phá thư mục (Trình khám phá là gì?) Chuyển đổi Giấy tờ được kết nối Giấy tờ được kết nối (Giấy tờ được kết nối là gì?) Chuyển đổi Litmaps Litmaps (Litmaps là gì?) Chuyển đổi scite.ai Trích dẫn thông minh scite (Trích dẫn thông minh là gì?) Mã, Dữ liệu, Phương tiện Mã, Dữ liệu và Phương tiện liên quan đến bài viết này Chuyển đổi alphaXiv alphaXiv (alphaXiv là gì?) Chuyển đổi Liên kết đến mã Công cụ tìm mã CatalyzeX cho các bài báo (CatalyzeX là gì?) Chuyển đổi DagsHub DagsHub (DagsHub là gì?) GotitPub Gotit.pub (GotitPub là gì?) Huggingface Hugging Face (Huggingface là gì?) ScienceCast ScienceCast (ScienceCast là gì?) Bản thử nghiệm Bản thử nghiệm Replicate Replicate (Replicate là gì?) Spaces Hugging Face Spaces (Spaces là gì?) Spaces TXYZ.AI (TXYZ.AI là gì?) Các bài báo liên quan Công cụ đề xuất và tìm kiếm Liên kết đến Influence Flower Influence Flower (Influence Flowers là gì?) Công cụ đề xuất cốt lõi CORE Recommender (CORE là gì?) Tác giả Địa điểm Tổ chức Chủ đề Về arXivLabs arXivLabs: các dự án thử nghiệm với cộng tác viên cộng đồng arXivLabs là một khuôn khổ cho phép các cộng tác viên phát triển và chia sẻ các tính năng arXiv mới trực tiếp trên trang web của chúng tôi. Cả cá nhân và tổ chức làm việc với arXivLabs đều đã chấp nhận và tuân thủ các giá trị của chúng tôi về sự cởi mở, cộng đồng, sự xuất sắc và quyền riêng tư dữ liệu người dùng. arXiv cam kết với những giá trị này và chỉ làm việc với các đối tác tuân thủ chúng. Bạn có ý tưởng cho một dự án sẽ mang lại giá trị cho cộng đồng arXiv không? Tìm hiểu thêm về arXivLabs. Những tác giả nào của bài báo này là người xác nhận? | Tắt MathJax (MathJax là gì?)