Nghiên cứu
Học cách khám phá toán học thú vị: Định nghĩa mới về giá trị của các định lý
(giờ Việt Nam)
Tóm tắt AI
Nghiên cứu đề xuất phương pháp đo lường độ thú vị của định lý toán học dựa trên tỷ lệ giữa độ dài chứng minh và phát biểu, đồng thời huấn luyện mô hình 27B để dự đoán độ khó chứng minh hiệu quả hơn các mô hình hiện nay.
Chính văn · Bản dịch AI
Tóm tắt: Gần đây, các Mô hình Ngôn ngữ Lớn (LLM) ngày càng có khả năng giải quyết các bài toán toán học nâng cao, bao gồm nhiều bài toán đã tồn tại hàng thập kỷ. Điều này mở ra cánh cửa cho việc mở rộng tri thức toán học ở quy mô chưa từng có. Tuy nhiên, mặc dù các LLM có thể đưa ra giả thuyết và chứng minh ngày càng nhiều định lý, vẫn chưa rõ liệu tri thức toán học mới này có thú vị hay hữu ích hay không. Chúng tôi định nghĩa tính thú vị nội tại của một định lý là tỷ lệ giữa độ dài chứng minh và độ dài phát biểu của nó. Chúng tôi chỉ ra rằng điều này tương quan mạnh mẽ với thước đo ngoại lai về tính hữu dụng hạ nguồn của một định lý. Chúng tôi xác định độ khó của một chứng minh dựa trên một tập hợp các tiền đề là một nguyên hàm hữu ích để tính toán các chỉ số này, và huấn luyện một mô hình 27B dự đoán độ khó chứng minh chính xác hơn các mô hình đa năng tiên tiến. Việc tối ưu hóa theo thước đo của chúng tôi tạo ra một mô hình có khả năng tạo ra các định lý thú vị hơn, đồng thời giảm sự trùng lặp đáng kể hoặc toàn bộ với Mathlib từ 91,9% xuống 30,6%, cho thấy khả năng tạo ra nhiều toán học ngoài phân phối (out-of-distribution) hơn. Chúng tôi chứng minh rằng hệ thống của mình có thể tạo ra các định lý ứng viên, chọn ra những định lý thú vị nhất trong số đó và xây dựng lặp đi lặp lại trên một thư viện toán học tự mở rộng. Các chỉ số này cung cấp một tín hiệu thực tế và có thể định lượng để xếp hạng các giả thuyết và hướng dẫn tìm kiếm chứng minh trong các thư viện toán học hình thức. Khung làm việc của chúng tôi cung cấp một con đường hướng tới các thư viện toán học tự mở rộng, được máy xác minh, có thể chọn ra các phát biểu đáng giá mà không cần dựa vào các mục tiêu do con người cung cấp.
| Chủ đề: | Học máy (cs.LG); Trí tuệ nhân tạo (cs.AI) |
| Trích dẫn là: | arXiv:2609.28603 [cs.LG] |
| (hoặc arXiv:2609.28603v1 [cs.LG] cho phiên bản này) | |
| https://doi.org/10.48550/arXiv.2609.28603 DOI do arXiv cấp thông qua DataCite (đang chờ đăng ký) |
Lịch sử gửi bài
Từ: Niket Patel [xem email] [v1] Thứ Tư, 23 tháng 9 năm 2026 16:06:29 UTC (536 KB)
Bài viết được AI dịch và tổng hợp tự động từ Hugging Face Daily Papers. Liên kết bài gốc ở phía trên. AIHOT.vn luôn dẫn nguồn đầy đủ — nếu bạn thấy điểm cần chỉnh sửa, hãy gửi ý kiến tại trang phản hồi.