OpenAI mô hình mới Astra ra mắt lần đầu: một hơi giải quyết 10 bài toán khó chưa lời giải trong suốt một thập kỷ

Theo Động Sát Beating theo dõi, OpenAI lần đầu tiên chính thức công bố mô hình chủ lực tiếp theo Astra. Phiên bản nội bộ đã đạt được kết quả mới trên 10 bài toán lý thuyết toán học và khoa học máy tính lý thuyết chưa được giải quyết trong thời gian dài. Kết luận cốt lõi của các bài toán này không có tiến triển trong ít nhất 10 năm, đa số thời gian bế tắc còn lâu hơn.

Một số bài toán trong đó đã được giải quyết trực tiếp hoặc bác bỏ. Astra lần đầu tiên xây dựng được nhóm không sofic, trả lời một câu hỏi mở cốt lõi trong lý thuyết nhóm; nó cũng bác bỏ giả thuyết cứng nhắc Connes, và giải quyết 3 bài toán Erdős. Các kết quả còn lại bao gồm các giới hạn mới và chứng minh độ khó liên quan đến xếp chồng hình cầu, lý thuyết mã hóa, độ phức tạp lượng tử và mật mã hậu lượng tử.

OpenAI cho biết, số Token mà mô hình sử dụng để tìm ra 10 kết quả này, quy đổi theo giá API Sol, khoảng 2000 USD.

Các lập luận toán học này được tạo ra bởi Astra. Con người sau đó hỗ trợ sắp xếp thành bài báo, mô hình tiếp tục chuyển từng chứng minh thành chứng chỉ Lean, để máy tính từng bước xác minh suy luận có hợp lệ hay không. OpenAI đã công khai bài báo, chứng chỉ chứng minh và quá trình suy luận của mô hình.