Các nhà nghiên cứu tiếp cận giới hạn tính toán với Busy Beaver thứ năm
(quantamagazine.org)-
Phần mở đầu
- 40 năm trước, các nhà khoa học máy tính đã tụ họp tại Dortmund, Đức để cạnh tranh tìm ra busy beaver thứ năm
- Busy beaver là những chương trình máy tính đơn giản nhưng có thời gian chạy cực dài
- Các chương trình này có liên quan đến những bài toán chưa giải nổi tiếng của toán học và bắt nguồn từ một vấn đề lâu đời trong khoa học máy tính
- Hai năm trước, nghiên cứu sinh Tristan Stérin đã khởi động thử thách Busy Beaver, với hơn 20 người đóng góp từ khắp thế giới tham gia
- Ngày nay, nhóm đã xác nhận giá trị của BB(5) là 47,176,870
-
Sẽ dừng hay không dừng
- Các chương trình busy beaver được viết dưới dạng chỉ thị cho một máy tính lý thuyết gọi là máy Turing
- Máy Turing thực hiện tính toán bằng cách đọc và ghi 0 và 1 trên một băng vô hạn
- Bài toán dự đoán liệu một máy Turing sẽ dừng hay chạy mãi mãi được gọi là bài toán dừng
- Bài toán dừng không có lời giải tổng quát, điều này khiến cuộc săn busy beaver càng hấp dẫn hơn
-
Sự xuất hiện của con beaver
- Nhà toán học Tibor Radó đã phát minh ra trò chơi busy beaver vào năm 1962
- Trong mỗi nhóm quy tắc, máy Turing chạy lâu nhất được gọi là busy beaver
- BB(n) biểu thị số bước mà máy busy beaver với n quy tắc thực hiện trước khi dừng
-
Đàn beaver của Brady
- Allen Brady đã phát triển các kỹ thuật săn busy beaver trong thập niên 1960 và xác định giá trị của busy beaver thứ tư vào năm 1974
- BB(4) được xác nhận là cỗ máy dừng sau 107 bước
-
Con beaver thứ năm
- Cuộc săn lớn đầu tiên nhằm tìm ra busy beaver thứ năm bắt đầu tại cuộc thi ở Dortmund năm 1984
- Năm 1989, Heiner Marxen đã phát hiện một cỗ máy dừng sau 47,176,870 bước
- Năm 2003, Georgi Georgiev dừng cuộc săn BB(5), để lại 43 máy Turing chưa được giải quyết
-
Kêu gọi mọi thợ săn
- Tristan Stérin đã khởi động thử thách Busy Beaver vào năm 2022, với sự tham gia của các cộng tác viên trên toàn thế giới
- Shawn Ligocki gia nhập nhóm vào năm 2022 và có những đóng góp quan trọng
- Justin Blanchard đã phát triển phương pháp closed tape language, một trong những kỹ thuật mạnh nhất của nhóm
-
Tiếp cận quái vật
- Skelet #1 và #17 là những cỗ máy đặc biệt khó, và nhóm đã kết hợp nhiều ý tưởng khác nhau để giải quyết chúng
- Vào tháng 5 năm 2023, một cộng tác viên ẩn danh có tên mxdys đã hoàn thành chứng minh Coq
-
Nơi những con beaver lang thang
- Nhóm đang viết một bài báo học thuật chính thức, và một số người đang nỗ lực tìm con beaver tiếp theo
- BB(6) có vẻ sẽ khó giải vì các vấn đề tương tự giả thuyết Collatz
Ý kiến của GN⁺
- Bài viết này mang đến một ví dụ hấp dẫn về việc khám phá các giới hạn của khoa học máy tính
- Thử thách Busy Beaver cho thấy tầm quan trọng của nghiên cứu hợp tác
- Việc giải được BB(5) mang ý nghĩa lớn với cộng đồng khoa học máy tính và toán học
- Một dự án có tính chất tương tự là nghiên cứu về giả thuyết Collatz
- Khi áp dụng công nghệ mới hoặc mã nguồn mở, tính hợp tác và khả năng tái lập là rất quan trọng
1 bình luận
Ý kiến trên Hacker News
Có chia sẻ ý kiến về bài đăng trên blog của Scott Aaronson
Tồn tại nhiều biến thể khác nhau của bài toán Busy Beaver
Có chia sẻ câu chuyện về một kỹ sư đã nghỉ việc để nghiên cứu bài toán Busy Beaver
Có đề cập đến chứng minh bằng Coq
Có ý kiến cho rằng bài báo Busy Beaver gốc của Tibor Radó dễ đọc và thú vị
Bài toán dừng của chương trình máy Turing 5-trạng thái 2-màu đã được giải quyết
Có nhắc đến quan niệm sai lầm rằng con người có thể giải quyết bài toán dừng một cách trực giác
Có chia sẻ kinh nghiệm từng viết chương trình để giải bài toán Cutting Stock trong một dự án cá nhân
Có ý kiến cho rằng việc có thể chứng minh một chương trình máy Turing 5-trạng thái có dừng hay không là nhờ may mắn
Theo bài đăng trên blog của Scott Aaronson, có 16,679,880,978,201 máy Turing 5-trạng thái tồn tại
Các giá trị của hàm Busy Beaver được chia sẻ