OpenAI công bố 722 bản thảo toán học, hiện còn 719 bản

Trong số 722 bản thảo toán học do OpenAI công bố, hiện kho lưu trữ còn 719 bản. Khoảng 42% kết quả hàng đầu đã được hình thức hóa bằng Lean, nhưng giới toán học vẫn đang đánh giá toàn bộ kết quả.

Trong thông báo ngày 6 tháng 10, OpenAI cho biết mô hình nội bộ tiên tiến của công ty đã tạo ra các kết quả nghiên cứu toán học. Kho lưu trữ công khai nhóm 722 bản thảo thành 372 nhóm kết quả và cho biết mô hình được giao khoảng 4.000 bài toán. Lịch sử thay đổi của kho ghi nhận 3 bản thảo bị rút và 14 bản được chỉnh sửa.

Các bản thảo đề cập đến nhiều lĩnh vực như lý thuyết số, hình học đại số, giải tích và khoa học máy tính lý thuyết. OpenAI cũng công bố một số bản hình thức hóa chứng minh bằng Lean, 10 bản tóm tắt lập luận và ước tính lượng tính toán. Công ty cho biết mỗi kết quả cần lượng tính toán tương đương trung bình khoảng 3 giờ sử dụng tính năng “suy nghĩ” của ChatGPT Pro. Tên mô hình và bản thân mô hình không được công bố.

Lean là công cụ biểu diễn mệnh đề toán học bằng ngôn ngữ hình thức và dùng máy tính kiểm tra các bước chứng minh có tuân theo quy tắc logic hay không. Theo kho lưu trữ của OpenAI, khoảng 42% kết quả hàng đầu hiện đã được hình thức hóa. Lịch sử thay đổi ghi nhận 300 trong số 719 kết quả đã được hình thức hóa tính đến ngày 7 tháng 10.

Tỷ lệ hình thức hóa không đồng nghĩa với độ chính xác của toàn bộ bản thảo. Lean kiểm tra quy trình chứng minh cho mệnh đề hình thức được nhập vào, nhưng không tự xác định mệnh đề đó có khớp với kết quả mà bài báo nêu hay các giả định và phạm vi áp dụng có phù hợp hay không. OpenAI cũng cho biết các kết quả chưa được hình thức hóa trong kho lưu trữ có thể còn vấn đề.

Bên cạnh việc kiểm chứng, phạm vi công khai quy trình nghiên cứu cũng là vấn đề được quan tâm. OpenAI cho biết trong thông báo rằng công ty đã tham khảo khuyến nghị của nhóm cố vấn độc lập, đồng thời đăng tải quy trình sửa bản thảo, trích dẫn và một số thông tin về phương pháp lên kho lưu trữ. Tuy nhiên, công ty không công bố mô hình và toàn bộ câu lệnh, khiến các nhà nghiên cứu bên ngoài khó tái tạo kết quả trong cùng điều kiện.

Trong tuyên bố ngày 6 tháng 10, Nhóm Cố vấn Toán học và AI (AGMAI) cho biết đợt công bố này là bước khởi đầu cho quá trình tìm hiểu kết quả và đưa chúng vào tri thức toán học. Nhóm nhấn mạnh việc đã thảo luận với OpenAI không có nghĩa là họ đánh giá mức độ ảnh hưởng của các kết quả hoặc bảo đảm quy trình công bố. Nhóm cũng cho rằng các nhà toán học cần có khả năng tự phát triển câu hỏi và cách tiếp cận, thay vì chỉ xem xét kết quả từ những bài toán do công ty AI lựa chọn.

Chỉ dựa vào số lượng bản thảo và tỷ lệ hình thức hóa thì chưa thể xác định tầm quan trọng hay ý nghĩa học thuật của từng kết quả. Khi OpenAI công bố 722 bản thảo, mới chỉ một số chứng minh được hình thức hóa bằng Lean và toàn bộ kết quả chưa hoàn tất kiểm chứng. Những thay đổi được ghi nhận sau đó gồm việc rút và chỉnh sửa một số bản thảo, cùng quá trình hình thức hóa thêm một số chứng minh.