-
Giới thiệu về o3 và FrontierMath
- o3 là mô hình ngôn ngữ mới của OpenAI, đạt 25% điểm số trên tập dữ liệu bí mật FrontierMath.
- FrontierMath là bộ dữ liệu kín gồm các bài toán toán khó do Epoch AI công bố.
- Tập dữ liệu này bao gồm các bài như "Tìm số này!" và đòi hỏi đáp án rõ ràng có thể kiểm tra tự động.
-
Độ khó của bộ dữ liệu FrontierMath
- Các bài toán trong FrontierMath cũng không điển hình ngay cả với các nhà toán học nghiên cứu, và một số bài đòi hỏi kiến thức ở trình độ tiến sĩ.
- Các bài toán trong tập này tập trung vào việc tìm ra con số hơn là xây dựng chứng minh toán học.
- Vì các nhà toán học nghiên cứu thường dành nhiều thời gian để tìm chứng minh hoặc ý tưởng, FrontierMath trở thành dữ liệu quan trọng trong nghiên cứu toán của AI.
-
Năng lực toán học của AI
- AI hiện đang giải tốt các bài toán cấp trung học và được dự đoán sẽ sớm vượt qua cả bài thi toán đại học.
- Tuy nhiên, việc tạo ra ý tưởng đột phá ở mức cao hơn bậc cử nhân vẫn còn là một thách thức lớn.
- Việc o3 đạt 25% điểm số là rất đáng chú ý, nhưng có ý kiến cho rằng một số bài thuộc cấp độ sinh viên đại học.
-
Vai trò của AI trong nghiên cứu toán học
- Trong nghiên cứu toán học, trọng tâm quan trọng là giải quyết bài toán kiểu "Hãy chứng minh định lý này!".
- AlphaProof của DeepMind đã giải được 4 bài trong số các bài thi Olympic Toán Quốc tế 2024, và một số bài đã được xác nhận bằng chứng minh Lean đầy đủ.
- Để AI đóng góp nhiều hơn trong nghiên cứu toán, nó cần có khả năng giải thích chứng minh theo cách mà con người có thể hiểu được.
-
Triển vọng tương lai
- Để AI đóng góp nhiều hơn trong nghiên cứu toán, nó cần có khả năng giải thích chứng minh theo cách mà con người có thể hiểu được.
- Sự tiến bộ của AI diễn ra rất nhanh, nhưng con đường phía trước vẫn còn dài.
- Thời điểm AI vượt qua ngưỡng bậc đại học vẫn còn chưa chắc chắn.
1 bình luận
Ý kiến Hacker News
Trong một chuỗi Reddit, trong ba mức độ khó thì 25% là T1 (dễ nhất) và 50% là T2. Trong năm bài toán công khai mà tác giả xem, có hai bài ở mức T1 và hai bài ở mức T2. Glazer mô tả T1 là "bài toán cấp IMO/đại học", nhưng tác giả bài viết không coi đó là bài toán ở cấp đại học. LLM đã làm những việc khiến tác giả không khỏi ngạc nhiên.
Tôi đã thử dùng ChatGPT để hiểu đại số tuyến tính, nhưng trong toán học thực tế nó thường mắc lỗi rất ngớ ngẩn, như lấy chỉ mục vượt quá số chiều của vector, thử phân rã ma trận cho một vô hướng, hoặc cố nhân các ma trận có kích thước không tương thích.
O1 phát hiện lỗi tốt hơn 4o, nhưng vẫn mắc rất nhiều sai lầm ngớ ngẩn. Khi không có người có một chút kiến thức hỗ trợ, việc tạo ra kết quả ổn định là rất khó.
Trong một bài phát biểu của Akshay Venkatesh, mọi người đã thảo luận về tương lai của nghề "toán học" khi việc chứng minh lý thuyết tự động trở nên phổ biến hơn. Ông cũng nói về cách tiến bộ của suy luận tự động có thể làm thay đổi cách hình thành và thực hiện toán học nghiên cứu.
Với tư cách là cha mẹ có con trai 18 tuổi muốn học toán, tác giả lo lắng tự động hóa có thể khiến nghề này mất đi. Tuy nhiên, họ băn khoăn liệu LLM có thể thay thế hoàn toàn hay không. Vì LLM không có thời gian và tài nguyên vô hạn để giải mọi thứ, nên họ tin rằng vai trò con người vẫn còn.
Mặc dù chưa chắc có thể xây dựng một bộ đề gồm những bài toán mà LLM giải được gần như toàn bộ, tác giả không tin nó sẽ trở thành một người giải quyết vấn đề tổng quát thay thế được suy luận của con người. Lập luận của họ là đến khi AI phát triển được một thứ lý tính xã hội độc lập kiểu con người, suy luận vẫn chưa thật sự khả thi.
Tác giả nêu ví dụ về những lỗi cơ bản của ChatGPT. Ví dụ, trong khi dẫn xuất công thức hiệu suất của Stop-and-Wait ARQ, nó giải thích một bước sai; và khi được yêu cầu tạo tam đoạn luận để luyện tập, nó đưa ra một tam đoạn luận thiếu nhất quán.
Họ nêu khả năng tập dữ liệu FrontierMath đã bị nhiễu. Nếu OpenAI đã biết trước các câu hỏi, họ nghĩ rằng phiên bản tiếp theo có thể đạt trên 80% trong bài kiểm tra FrontierMath.
Họ đang đối mặt với vấn đề tương tự như trong nghiên cứu lượng tử: để chứng minh có tiến triển, phải thực hiện các phép tính không thể làm được trên máy tính truyền thống. Khi ChatGPT đạt 25%, câu hỏi được đặt ra là liệu 25% đó có đến từ các câu hỏi tương đồng với bộ dữ liệu huấn luyện hay không.
Có mối lo về việc các mô hình ngôn ngữ có thể đưa ra "chứng minh" cho giả thuyết Riemann. Toán học có thể cố gắng xác minh các chứng minh như vậy, nhưng điều đó có thể tốn rất nhiều thời gian.
Máy móc sẽ không tham gia IMO 2025. IMO không có khái niệm "giám khảo"; điểm được quyết định qua thương lượng giữa đội trưởng của từng quốc gia và các giám khảo. Không có ai muốn ở lại thêm nhiều giờ chỉ để chấm bài của AI.