Thử Thách Chưng Cất Toán Học – Lý Thuyết Cân Bằng

Nghiên cứu toán học theo truyền thống liên quan đến một số ít các nhà toán học chuyên nghiệp làm việc chặt chẽ về các vấn đề khó khăn. Tuy nhiên, từ lâu tôi đã tin rằng có một cách bổ sung để làm toán, trong đó người ta làm việc với một cộng đồng rộng lớn gồm những người có đầu óc toán học về các vấn đề có thể không sâu sắc như các vấn đề mà người ta thường làm, nhưng vẫn có mối quan tâm toán học; và các công nghệ hiện đại, bao gồm AI, phù hợp hơn để đóng góp loại quy trình làm việc sau này. "Các dự án Polymath" là một ví dụ về loại hình hợp tác rộng lớn này, nơi các nền tảng internet như blog và wiki được sử dụng để tạo điều kiện cho sự hợp tác như vậy. Vài năm sau, các dự án chính thức hóa hợp tác (chẳng hạn như dự án chính thức hóa phỏng đoán đa thức Freiman-Ruzsa của Marton, được thảo luận trước đây trên blog này ở đây) đã trở nên phổ biến trong một số vòng tròn. Và vào năm 2024, tôi đã khởi động Dự án Lý thuyết Cân bằng (ETP) (được thảo luận trên blog này tại đây và ở đây), kết hợp sự chặt chẽ của chính thức hóa Lean với "AI lỗi thời tốt" (dưới dạng chứng minh định lý tự động) để giải quyết (với xác minh chính thức) hơn 22 triệu vấn đề đúng sai trong đại số phổ quát.

Tiếp tục tinh thần này, Damek Davis và tôi đang khởi động một dự án mới, dưới hình thức một thử thách cạnh tranh thử nghiệm do Quỹ SAIR tổ chức (nơi tôi phục vụ với tư cách là thành viên hội đồng quản trị, và đang cung cấp hỗ trợ kỹ thuật và tính toán). Ý tưởng về thách thức này, được thúc đẩy một phần bởi bài báo gần đây của Honda, Murakami và Zhang , là để đo lường mức độ mà 22 triệu kết quả đại số phổ quát đúng sai thu được bởi ETP có thể được "chưng cất" thành một "bảng cheat" ngắn, có thể đọc được bằng con người, tương tự như cách một học sinh trong một lớp toán đại học có thể chắt lọc kiến thức học được từ lớp đó thành một tờ giấy duy nhất mà học sinh được phép đưa vào một kỳ thi.

Dưới đây là một vấn đề điển hình trong đại số phổ quát mà ETP đã có thể trả lời:

Bài 1 Giả sử rằng ${*: M \times M \rightarrow M}$ là một phép toán nhị phân ${x * (y * z) = (z * w) * w}$ dành cho tất cả mọi người ${x,y,z,w}$ . Điều đó có đúng ${x * (y * x) = (x * y) * z}$ với tất cả mọi người ${x,y,z}$ không?

Một vấn đề như vậy có thể được giải quyết bằng cách thao tác đại số phương trình ban đầu để suy ra phương trình đích, hoặc bằng cách tìm một phản ví dụ cho phương trình đích vẫn thỏa mãn phương trình ban đầu. Có nhiều kỹ thuật khác nhau để đạt được một trong hai điều này, nhưng loại vấn đề này rất khó, và thậm chí không thể quyết định trong một số trường hợp; xem bài báo này của các cộng tác viên ETP để thảo luận thêm. Tuy nhiên, nhiều vấn đề trong số này có thể được giải quyết bằng một số nỗ lực của con người, bởi các chứng minh định lý tự động hoặc bởi các hệ thống AI biên giới; ví dụ ở đây là một giải pháp do AI tạo ra cho vấn đề trên.

Tuy nhiên, các mô hình AI này rất tốn kém và không tiết lộ nhiều thông tin chi tiết về việc câu trả lời của chúng đến từ đâu. Thay vào đó, nếu người ta thử một mô hình nhỏ hơn và rẻ hơn, chẳng hạn như một trong nhiều mô hình nguồn mở có sẵn, hóa ra các mô hình này về cơ bản hoạt động không tốt hơn cơ hội ngẫu nhiên, trong đó khi được yêu cầu nói liệu câu trả lời cho một câu hỏi như trên là đúng hay sai, họ chỉ trả lời đúng khoảng 50% thời gian.

Nhưng, tương tự như cách một học sinh gặp khó khăn với tài liệu cho một lớp học toán có thể thực hiện tốt hơn trong một kỳ thi khi được cung cấp hướng dẫn đúng đắn, hóa ra các mô hình giá rẻ như vậy có thể thực hiện ít nhất là tốt hơn một chút trong nhiệm vụ này (với tỷ lệ thành công tăng lên khoảng 55%-60%) nếu được nhắc nhở đúng hoặc "cheat sheet".

“Giai đoạn 1” của thử thách chưng cất, mà chúng tôi đã đưa ra hôm nay, yêu cầu các thí sinh thiết kế một bảng cheat (có kích thước tối đa 10 kilobyte) có thể tăng hiệu suất của các mô hình này đối với các vấn đề đúng sai ở trên lên mức cao nhất có thể. Chúng tôi đã cung cấp một “sân chơi ”để kiểm tra cheat sheet của một người (hoặc một số ít cheat sheet ví dụ) một số mô hình giá rẻ chống lại 1200 vấn đề công khai (1000 trong số đó được chọn ngẫu nhiên, và khá dễ dàng, cùng với 200 vấn đề“khó”đã được chọn để chống lại các chiến lược rõ ràng hơn để giải quyết những câu hỏi này); một video ngắn giải thích cách sử dụng sân chơi có thể được tìm thấy .

Giai đoạn nộp bài sẽ kết thúc vào ngày 20 tháng 4, sau đó chúng tôi sẽ đánh giá các bài nộp dựa trên một tập hợp con các câu hỏi kiểm tra riêng. 1000 bài nộp hàng đầu sẽ tiến tới giai đoạn thứ hai mà chúng tôi hiện đang trong quá trình thiết kế, sẽ liên quan đến các mô hình nâng cao hơn, nhưng cũng là nhiệm vụ khó khăn hơn không chỉ cung cấp câu trả lời đúng sai, mà còn là bằng chứng hoặc phản ví dụ cho vấn đề.

Cuộc thi sẽ được điều phối trên kênh Zulip này, nơi tôi hy vọng sẽ có một cuộc thảo luận sôi nổi và nhiều thông tin.

Tôi hy vọng rằng các bài nộp chiến thắng sẽ nắm bắt được các kỹ thuật hiệu quả nhất để giải quyết những vấn đề này và/hoặc cung cấp các kỹ thuật giải quyết vấn đề chung cũng có thể áp dụng cho các loại vấn đề toán học khác. Chúng tôi bắt đầu với bộ dữ liệu dự án lý thuyết cân bằng cho cuộc thi thí điểm này do tính khả dụng và phổ độ khó của nó, nhưng nếu loại quá trình chưng cất này dẫn đến kết quả thú vị, người ta chắc chắn có thể chạy trên nhiều loại khác của các lớp vấn đề toán học để có được một số dữ liệu thực nghiệm về cách chúng có thể được giải quyết dễ dàng, đặc biệt là sau khi chúng tôi học hỏi từ cuộc thi thí điểm này về cách khuyến khích sự tham gia và chia sẻ các phương pháp hay nhất.

SAIR cũng sẽ đưa ra một số thách thức toán học khác trong những tháng tới có tính chất hợp tác hơn so với thách thức cạnh tranh cụ thể này; hãy theo dõi để biết thêm thông báo.