Tencent Hunyuan hôm nay thông báo rằng tác nhân nghiên cứu Hyra, dựa trên mô hình Hy3, đã tìm ra một cấu trúc then chốt và đưa ra lời giải hoàn chỉnh cho một bài toán mở trong lĩnh vực tổ hợp cộng đã bỏ ngỏ hơn nửa thế kỷ.
Hiện bản thảo tiền công bố, cấu trúc tường minh và chứng minh hình thức đều đã được công khai:
Bài báo: https://arxiv.org/abs/2607.27199
Chứng minh hình thức Lean: https://github.com/linhaowei1/sum-diff-proof
Bài toán được phát biểu như sau:
Trước hết, lấy một tập hợp số nguyên hữu hạn A có ít nhất hai phần tử. Cộng từng cặp phần tử bất kỳ trong đó, thu thập tất cả các kết quả khác nhau để được “tập tổng” (A+A); trừ từng cặp phần tử bất kỳ, thu thập tất cả các kết quả khác nhau để được “tập hiệu” (A-A).
Vì mỗi kết quả trùng lặp chỉ được tính một lần, một câu hỏi tự nhiên là: sau phép cộng và phép trừ, tập hợp này sẽ mở rộng bao nhiêu lần?
Các nhà toán học dùng hai đại lượng để đo mức độ mở rộng này:
Đại lượng thứ nhất là hệ số mở rộng của tập tổng, đại lượng thứ hai là hệ số mở rộng của tập hiệu. Bất đẳng thức kinh điển về tập tổng và tập hiệu cho biết:
Để đo số mũ này, có thể định nghĩa
Do đó, bất đẳng thức kinh điển cho ta . Câu hỏi thực sự là: 2 chỉ là một cận trên rộng, hay là số mũ tối ưu có thể tiến tới tùy ý?
Trong hơn nửa thế kỷ, các nhà toán học không ngừng xây dựng những tập hợp mới nhằm làm cho C (A) lớn nhất có thể. Cấu trúc ban đầu năm 1969 đạt khoảng 1.0290, đến năm 1973 tăng lên 1.0598, và cấu trúc năm 2013 tiếp tục đạt 1.1259. Trong gần một năm qua, nhiều hoạt động tìm kiếm có AI hỗ trợ đã nâng con số này lên 1.1449. Trong một thử nghiệm khám phá nội bộ được ghi lại trong bài báo, Codex (GPT-5.5), với sự hướng dẫn của con người, lại nâng con số này lên 1.2851.
Hyra và Hy3 đã tiến thêm một bước mang tính quyết định. Hệ thống đưa ra một họ các tập hợp số nguyên hữu hạn được xây dựng tường minh, thỏa mãn
Điều này có nghĩa là: với bất kỳ mục tiêu nào gần 2 đến đâu, ta đều có thể xây dựng một tập hợp tương ứng sao cho số mũ vượt qua mục tiêu đó. Vì vậy, 2 thực sự là cận trên đúng của bài toán này.
Trước đó, các nhà nghiên cứu như Georgiev, Gómez-Serrano, Tao Terence và Wagner từng sử dụng AlphaEvolve để tối ưu thuật toán tìm kiếm và các tập hợp ứng viên. Những phương pháp này phụ thuộc vào việc liệt kê tường minh các tập hợp hữu hạn. Khi quy mô tăng, chi phí tính toán và bộ nhớ nhanh chóng tăng cao, đồng thời cũng khó chuyển tiếp một cách tự nhiên sang một cấu trúc tiệm cận có thể chứng minh.
Theo giới thiệu, trước tiên Tencent Hunyuan sử dụng Hyra để nâng kết quả tốt nhất trong tìm kiếm hữu hạn từ khoảng 1.14 lên 1.21, sau đó chuyển sang sử dụng ngôn ngữ tự nhiên để đề xuất các cấu trúc và lập luận toán học. LLM judge được dùng để cung cấp phản hồi cho quá trình khám phá.
Sau khoảng 24 giờ chạy, Hyra đã đề xuất ý tưởng cốt lõi của bài báo: sử dụng cấu trúc chữ số thập nhị phân và một cấu trúc tinh tế để kiểm soát tập hiệu, sau đó kết hợp với cơ sở cộng đối xứng trên nhóm tuần hoàn và định lý phần dư Trung Hoa, khiến tập tổng mở rộng với tốc độ gần bình phương. Đội ngũ chính thức đã kiểm tra độc lập và hoàn thiện toàn bộ chứng minh, đồng thời đưa ra chứng minh hình thức bằng Lean 4.