OpenAI công bố kết quả phản bác ETH, Anthropic cũng đưa tài liệu hình thức hóa lên mạng

OpenAI công bố kết quả phản bác Giả thuyết Thời gian mũ (ETH) cùng tài liệu hình thức hóa bằng Lean. Anthropic cũng đăng bài nghiên cứu liên quan và tài liệu hình thức hóa lên kho mã nguồn.

Ngày 26 tháng 10, OpenAI cho biết hệ thống của công ty đã đưa ra kết quả phản bác ETH và chứng minh được hình thức hóa đã được Lean kiểm chứng. Một nhóm chuyên gia bên ngoài sẽ đánh giá ý nghĩa và phạm vi áp dụng của kết quả. OpenAI cũng thông báo thành lập nhóm hợp tác gồm các nhà khoa học máy tính để kiểm chứng và giải thích kết quả. Thông báo chính thức của OpenAI trình bày kết quả và kế hoạch đánh giá.

Anthropic đã đăng bài nghiên cứu do Claude viết cùng tài liệu hình thức hóa liên quan lên kho mã nguồn công khai. Kho này giới thiệu thuật toán đếm số nghiệm thỏa mãn và dự án hình thức hóa liên quan đến ETH. Tuy nhiên, chỉ dựa vào mô tả trong kho công khai thì chưa thể kết luận rằng việc đánh giá độc lập của chuyên gia đã hoàn tất.

Giả thuyết Thời gian mũ (ETH) là một giả thuyết trong lý thuyết độ phức tạp tính toán, cho rằng không thể giải 3-SAT trong thời gian nhanh hơn mức tăng theo hàm mũ của số biến. 3-SAT đặt câu hỏi liệu có cách gán giá trị cho các biến để khiến mọi điều kiện trong một biểu thức đều đúng hay không, trong đó mỗi điều kiện gồm tối đa ba hạng tử logic. Điểm cốt lõi của tuyên bố lần này không phải là giải bài toán trong thời gian đa thức, mà là đưa ra một thuật toán thời gian bán mũ, có tốc độ tăng chậm hơn thời gian mũ.

Thuật toán thời gian bán mũ có thể nhanh hơn thuật toán thời gian mũ, nhưng điều đó không bảo đảm tốc độ thực tế sẽ hữu dụng ngay. Vì vậy, kết quả này không có nghĩa là mọi phép tính khó đều có thể được xử lý nhanh. Nó cũng không đồng nghĩa với việc đã giải được bài toán P so với NP, vốn đặt câu hỏi liệu mọi bài toán có thể kiểm tra lời giải nhanh có thể được giải nhanh hay không.

Tài liệu về phạm vi hình thức hóa của OpenAI mô tả một thuật toán đếm chính xác số nghiệm thỏa mãn của các biểu thức logic được mã hóa theo một cách cụ thể. Tài liệu phân biệt rằng cận thời gian chạy được hình thức hóa bằng Lean có thể khác với cận trong bản thảo được công bố riêng. Kho của Anthropic cũng giới thiệu máy Turing tất định dùng để đếm số nghiệm thỏa mãn và tài liệu hình thức hóa liên quan đến ETH.

Kiểm chứng bằng Lean là quy trình để máy tính kiểm tra chứng minh của một mệnh đề đã được hình thức hóa. Bản thân việc kiểm chứng này không xác định liệu mệnh đề đã hình thức hóa có mô tả chính xác bài toán ban đầu hay không, cũng không xác định ý nghĩa của kết quả trong bối cảnh nghiên cứu trước đây. Những vấn đề đó cần được đánh giá riêng thông qua việc thẩm định chứng minh toán học và phạm vi áp dụng của kết quả.

Giả thuyết Thời gian mũ từ lâu được dùng làm tiền đề cho các kết quả có điều kiện về độ khó của bài toán trong lý thuyết đồ thị, sinh học tính toán và cơ sở dữ liệu. OpenAI cho biết ngay cả khi tuyên bố vượt qua đánh giá độc lập, vẫn cần nghiên cứu thêm để chuyển kết quả thành thuật toán nhanh hơn hoặc cải thiện có tính thực tiễn. Khả năng các tiền đề trong nghiên cứu hiện có thay đổi cần được phân biệt với tuyên bố rằng các bài toán ứng dụng sẽ trở nên dễ hơn ngay lập tức.

ETH, tên viết tắt của Giả thuyết Thời gian mũ, trùng với mã giao dịch của Ethereum (ETH), nhưng trong bài này thuật ngữ chỉ giả thuyết thuộc lý thuyết độ phức tạp tính toán. Nghiên cứu không liên quan đến mạng Ethereum; các kết quả được công bố cũng không đưa ra căn cứ cho thấy hệ mật mã của Bitcoin (BTC) hay Ethereum đã bị phá vỡ. Quá trình đánh giá độc lập đang tiếp tục dựa trên chứng minh và tài liệu hình thức hóa hiện được công khai.