Nhóm đánh giá dự kiến công bố mã Lean Yang–Mills của OpenAI trên 2 kho GitHub

Nhóm công tác Yang–Mills dự kiến công bố mã Lean về lý thuyết Yang–Mills lượng tử do OpenAI nộp cùng tài liệu đánh giá qua hai kho GitHub.

Crypto Briefing đưa tin nhóm dự kiến công bố tài liệu vào ngày 10 theo giờ địa phương tại Mỹ. Kho thứ nhất sẽ chứa toàn bộ phần mã Lean OpenAI đã nộp; kho thứ hai sẽ lưu tài liệu đánh giá xác minh của nhóm.

Trong tuyên bố thứ hai công bố ngày 3 tháng 11, nhóm cho biết đang xem xét liệu các định nghĩa trong mã và cách đặt vấn đề có phù hợp với tiêu chuẩn vật lý, toán học hay không, đồng thời kiểm tra chứng minh bằng ngôn ngữ tự nhiên có khớp với mã hay không. Khi đó, nhóm hy vọng công bố tài liệu trong tuần thứ hai của tháng 11 và cho biết sẽ thông báo trước một ngày.

OpenAI cho biết ngày 9 tháng 9 rằng họ đã tạo ra một chứng minh bằng ngôn ngữ tự nhiên về sự tồn tại của lý thuyết Yang–Mills. Ngày 18 tháng 9, công ty cho biết đã tạo thêm một chứng minh bằng ngôn ngữ tự nhiên riêng về sắc động lực học lượng tử.

OpenAI hoàn tất việc hình thức hóa chứng minh Yang–Mills bằng Lean vào ngày 16 tháng 10. Crypto Briefing đưa tin OpenAI lần đầu liên hệ với David J. Gross, nhà khoa học đoạt giải Nobel, trong cùng ngày và nhóm công tác được thành lập để tiến hành đánh giá độc lập.

OpenAI từng công bố các sản phẩm AI trong toán học và khoa học máy tính, nhưng trước đó yêu cầu chuyên gia đánh giá kết quả về vật lý. Trong thông báo ngày 26 tháng 10, công ty cho biết nhóm công tác sẽ tự đưa ra kết luận và không đại diện cho quan điểm của OpenAI.

Nhóm công tác cũng cho biết họ không chịu trách nhiệm trước OpenAI. Cấu trúc này tách biệt vai trò của công ty đưa ra kết quả với bên đánh giá.

Lean là công cụ cho phép viết các định nghĩa và lập luận toán học dưới dạng mã để máy tính kiểm tra từng bước chứng minh. Khi lời giải bằng ngôn ngữ tự nhiên được chuyển thành mã hình thức, máy tính có thể xác minh từng bước có tuân theo các quy tắc đã định hay không.

Tuy nhiên, việc mã hợp lệ về mặt logic chưa đủ để kết luận rằng nó chứng minh chính xác bài toán giới học thuật đặt ra. Nếu định nghĩa hoặc cách đặt vấn đề khác với chuẩn mực, máy tính vẫn có thể chứng minh đúng câu trả lời cho một câu hỏi khác. Vì vậy, nhóm công tác cũng xem xét liệu cách đặt vấn đề trong mã có khớp với bài toán hay không.

Lý thuyết Yang–Mills lượng tử là nền tảng của sắc động lực học lượng tử, lý thuyết mô tả tương tác mạnh. Lý thuyết Yang–Mills thuần túy nghiên cứu tương tác của gluon mà không bao gồm quark, còn sắc động lực học lượng tử có cả quark.

Bài toán Thiên niên kỷ của Viện Toán học Clay yêu cầu chứng minh cả sự tồn tại của lý thuyết Yang–Mills trong không gian bốn chiều lẫn sự tồn tại của khoảng cách khối lượng. Khoảng cách khối lượng là độ chênh lệch dương giữa trạng thái năng lượng cơ bản và trạng thái năng lượng kế tiếp.

Chứng minh của OpenAI đưa ra tuyên bố về sự tồn tại của lý thuyết. Nhóm công tác cho biết khoảng cách khối lượng và hiện tượng giam hãm quark vẫn là những vấn đề chưa được giải quyết.

Trong tuyên bố tháng 10, nhóm cho biết cách tiếp cận của OpenAI dựa trên phương pháp chuẩn hóa mạng lưới Wilson và các phương pháp nhóm tái chuẩn hóa của Balaban. Nhóm cũng nói rằng chứng minh dài và phức tạp, nên cần thời gian để hiểu phương pháp cũng như ý nghĩa vật lý của nó.

Toàn bộ tài liệu chứng minh OpenAI nộp dài 1.147 trang. Nhóm công tác cho biết sẽ công bố tài liệu đánh giá cùng toàn bộ chứng minh do AI tạo ra khi họ đủ tin tưởng vào tính chính xác của kết quả.