นักวิจัยเข้าใกล้ขีดจำกัดของการคำนวณด้วย Busy Beaver ตัวที่ห้า
(quantamagazine.org)- Busy Beaver Challenge ที่มีผู้เข้าร่วมมากกว่า 20 คนจากทั่วโลก ได้ยืนยันว่าเลข Busy Beaver ของเครื่องทัวริง 5 กฎคือ BB(5)=47,176,870
- ได้ยืนยันแล้วว่าเครื่องที่ Marxen และ Buntrock ค้นพบในปี 1989 ซึ่งหยุดทำงานหลัง 47,176,870 ขั้น คือ เครื่องหยุดทำงานแบบ 5 กฎ ที่รันได้นานที่สุดจริง
- ทีมงานผสาน แนวทางสายวงศ์, โปรแกรมตัดสินการไม่หยุดทำงาน และ Coq proof assistant เพื่อประมวลผลตัวเลือกนับสิบล้านรายการ
- ผลลัพธ์สุดท้ายเสร็จสมบูรณ์เป็น หลักฐาน Coq 40,000 บรรทัด ที่ mxdys รวมเทคนิคของชุมชนเข้าด้วยกัน และ Yannick Forster ผู้เชี่ยวชาญ Coq จาก Inria เป็นผู้ตรวจทาน
- ใน BB(6) มีเครื่อง 6 กฎชื่อ Antihydra ที่เป็นอุปสรรค โดยมีลักษณะคล้าย Collatz conjecture ทำให้ BB(5) อาจเป็นเลข Busy Beaver ตัวสุดท้ายที่มนุษยชาติจะรู้ค่าได้อย่างแม่นยำ
BB(5) ได้รับการยืนยันแล้ว
- ทีม Busy Beaver Challenge ยืนยันค่าที่แน่นอนของ BB(5) ว่าเป็น 47,176,870
- ค่านี้หมายถึงจำนวนขั้นสูงสุดที่เครื่องทัวริงซึ่งมี 5 กฎและหยุดทำงานได้สามารถรันได้
- การยืนยันใช้ Coq proof assistant โดย Coq รับรองว่าหลักฐานทางคณิตศาสตร์ถูกประกอบขึ้นอย่างปราศจากข้อผิดพลาด
- Cristopher Moore จาก Santa Fe Institute ประเมินว่างานด้านวิศวกรรมเชิงสังคมและวิศวกรรมเชิงคณิตศาสตร์ของงานนี้น่าประทับใจ
- Damien Woods จาก Maynooth University เปรียบความเร็วที่ได้ผลลัพธ์นี้ว่าอยู่ในระดับ “Usain Bolt territory”
- หัวใจสำคัญของ BB(5) ไม่ใช่การประยุกต์ใช้กับสาขาอื่นของวิทยาการคอมพิวเตอร์ แต่คือการเป็นความสำเร็จที่ได้มาบน ขอบเขตของความไม่สามารถคำนวณได้
ปัญหา Busy Beaver และปัญหาการหยุดทำงาน
- ปัญหา Busy Beaver ไม่ได้พิจารณาภาษาโปรแกรมทั่วไป แต่พิจารณา เครื่องทัวริง
- เครื่องทัวริงอ่านและเขียน 0 กับ 1 บนเทปอนันต์ และ head จะเคลื่อนทีละช่องพร้อมทำงานตามตารางกฎ
- แต่ละกฎจะกำหนดการกระทำถัดไปตามค่าที่กำลังอ่านอยู่ว่าเป็น 0 หรือ 1
- เปลี่ยนค่าหรือคงค่าเดิม
- เคลื่อนไปทางซ้ายหรือทางขวา
- ระบุกฎที่จะอ้างอิงถัดไป
- กฎพิเศษกำหนดว่าเครื่องจะหยุดเมื่อใด
- ปัญหาในการตัดสินโดยทั่วไปว่าเครื่องทัวริงเครื่องหนึ่งจะหยุดในที่สุดหรือจะทำงานตลอดไป คือ ปัญหาการหยุดทำงาน
- Alan Turing พิสูจน์แล้วว่าไม่มีวิธีแก้ทั่วไปสำหรับปัญหาการหยุดทำงาน
- การล่า Busy Beaver จึงเป็นการจำแนกเครื่องแต่ละตัวภายในเซตจำกัดที่ตรึงจำนวนกฎไว้ แทนที่จะพยายามแก้สถานะการหยุดทำงานของทุกเครื่องในภาพรวม
Busy Beaver game ของ Radó
- Tibor Radó นิยาม Busy Beaver game ไว้ในบทความปี 1962 โดยจัดกลุ่มเครื่องทัวริงตามจำนวนกฎ
- ในเซตของเครื่องทัวริงทั้งหมดที่มีจำนวนกฎ n ข้อ:
- บางเครื่องทำงานตลอดไป
- บางเครื่องหยุดทำงาน
- ในบรรดาเครื่องที่หยุดทำงาน เครื่องที่รันได้นานที่สุดคือ busy beaver
- จำนวนขั้นที่มันรันได้คือ BB(n)
- การยืนยัน BB(n) ต้องตรวจเวลารันของเครื่องที่หยุดทำงานทั้งหมด และพิสูจน์ว่าเครื่องที่เหลือทั้งหมดไม่หยุดทำงาน
- การวัดเวลารันมักทำได้ด้วยการจำลองบนคอมพิวเตอร์ แต่การพิสูจน์ว่าไม่หยุดทำงานนั้นใกล้เคียงกับการแก้ปัญหาการหยุดทำงานสำหรับเครื่องเฉพาะตัว
- Shawn Ligocki ผู้มีส่วนร่วมใน Busy Beaver Challenge มองว่านี่คือการทำงานบน “ขอบเขตของสิ่งที่ยังไม่รู้”
ตั้งแต่ BB(1) ถึง BB(4)
- BB(1)=1 ตรวจสอบได้ง่าย
- หากกฎแรกกำหนดให้หยุดเมื่ออ่าน 0 ก็จะหยุดตั้งแต่ขั้นแรก
- นอกเหนือจากนั้น เครื่องจะเคลื่อนไปตามเทปที่เต็มไปด้วย 0 ต่อไปเรื่อย ๆ
- แค่มี 2 กฎก็เกิดเครื่องทัวริงที่ต่างกันมากกว่า 6,000 เครื่องแล้ว ส่วน 3 กฎมีระดับหลายล้านเครื่อง และ 4 กฎเพิ่มเป็นหลายพันล้านเครื่อง
- Allen Brady รวม แนวทางสายวงศ์ เข้าไว้ในโปรแกรมคอมพิวเตอร์เพื่อลดความซ้ำซ้อน โดยจัดกลุ่มเครื่องที่มีพฤติกรรมเริ่มต้นเหมือนกัน
- Shen Lin ร่วมกับ Radó พิสูจน์ว่า BB(3)=21 และประกาศผลในปี 1965
- Brady ค้นพบเครื่อง 4 กฎที่หยุดหลัง 107 ขั้นในปี 1966 และพิสูจน์ในปี 1974 ว่านั่นคือ BB(4)
- จากนั้น BB(4) ก็เป็นเลข Busy Beaver ตัวสุดท้ายที่มนุษยชาติรู้มานานกว่า 40 ปี
การล่า Busy Beaver ตัวที่ห้า
- การแข่งขันที่ Dortmund ในปี 1984 คือการล่าครั้งใหญ่ครั้งแรกที่มุ่งสู่ BB(5)
- เครื่องทัวริง 5 กฎมีอยู่เกือบ 17 ล้านล้านเครื่อง และต่อให้ไล่ดูทีละเครื่องด้วยความเร็ว 1 มิลลิวินาทีต่อเครื่องก็ยังต้องใช้เวลากว่า 500 ปี
- เครื่องที่ยุ่งที่สุดที่ผู้เข้าร่วม Dortmund พบ หยุดทำงานหลังรันเกิน 100,000 ขั้น
- ต่อมามีนักวิจัยคนหนึ่งพบเครื่องที่รันเกิน 2 ล้านขั้น
- Heiner Marxen และ Jürgen Buntrock พัฒนาเทคนิคทางคณิตศาสตร์เพื่อเร่งการจำลองเครื่องทัวริง
- ในปี 1989 Marxen รันโปรแกรมบนคอมพิวเตอร์ใหม่อันทรงพลังของบริษัทตลอดช่วงสุดสัปดาห์ และพบเครื่องที่หยุดหลัง 47,176,870 ขั้น
- Buntrock ทำซ้ำผลลัพธ์ได้ และทั้งสองตีพิมพ์บทความในต้นปี 1990
- แม้เครื่องนี้จะเป็น Busy Beaver ตัวที่ห้าจริง แต่การพิสูจน์ว่าเครื่องที่เหลือทั้งหมดไม่หยุดทำงานยังต้องใช้เวลาอีกกว่า 30 ปี
Skelet และเครื่องที่ยังไม่คลี่คลาย
- ช่วงต้นทศวรรษ 2000 นักวิทยาการคอมพิวเตอร์ชาวบัลแกเรีย Georgi Ivanov Georgiev เข้าใกล้การพิสูจน์ BB(5) อย่างมาก
- Georgiev ใช้เวลาวันละหลายชั่วโมงตลอด 2 ปีในการปรับปรุงโปรแกรมสำหรับระบุเครื่องที่ไม่หยุดทำงาน
- โปรแกรมสุดท้ายมีโค้ดแน่น ๆ 6,000 บรรทัด แบบไม่มีคอมเมนต์ และใช้เวลารันมากกว่าหนึ่งสัปดาห์
- โปรแกรมนี้เหลือเครื่องทัวริงที่ยังไม่คลี่คลายอยู่ราว 100 เครื่อง และ Georgiev ลดจำนวนลงด้วยการวิเคราะห์ด้วยมือจนเหลือ 43 เครื่อง
- Georgiev เผยแพร่ผลลัพธ์ทางออนไลน์ในปี 2003 ภายใต้นามแฝง Skelet
- เครื่องยากทั้ง 43 เครื่องนี้จึงถูกเรียกว่า Skelet machines ตามนามแฝงของเขา
- Georgiev บอกว่าหลังทำงานเข้มข้น 2 ปี เขาเหนื่อยล้าจนไม่อาจคิดไอเดียใหม่ ๆ ได้อีก
โครงสร้างการทำงานร่วมกันของ Busy Beaver Challenge
- Tristan Stérin เริ่ม Busy Beaver Challenge ในปี 2022
- โครงการดำเนินไปในรูปแบบความร่วมมือออนไลน์ และเติบโตเป็นชุมชนนานาชาติที่มีผู้เข้าร่วมมากกว่า 20 คน รวมถึงหลายคนที่ไม่มีคุณวุฒิทางวิชาการแบบดั้งเดิม
- Stérin มองว่าการยืนยัน BB(5) ต้องใช้หลักฐานที่มีเอกสารรองรับและทำซ้ำได้
- โปรแกรมของ Georgiev นั้นล้ำหน้า แต่ยากที่นักวิจัยคนอื่นจะตรวจสอบได้
- Stérin แบ่งงานบนพื้นฐานของแนวทางเดิม
- ใช้แนวทางสายวงศ์ของ Brady เพื่อตัดเครื่องที่ซ้ำซ้อนออก
- ระบุเครื่องที่หยุดภายใน 47,176,870 ขั้น
- สำหรับเครื่องที่รันตลอดไป ใช้โปรแกรมอิสระที่บรรจุวิธีพิสูจน์เฉพาะของแต่ละแบบ
- โปรแกรมขั้นแรกที่เขียนขึ้นปลายปี 2021 สร้างรายชื่อเครื่องทัวริงประมาณ 120 ล้านเครื่อง ซึ่งเพียงพอสำหรับตัดสิน BB(5)
- ในจำนวนนั้นราวหนึ่งในสี่หยุดก่อนเครื่องของ Marxen และ Buntrock ส่วน 88 ล้านเครื่อง ยังต้องตรวจสอบต่อ
- Stérin ยังสร้างอินเทอร์เฟซออนไลน์ของ แผนภาพปริภูมิ-เวลา ที่แสดงพฤติกรรมของเครื่องเป็นกริดสองมิติของ 0 และ 1
ภาษาของเทปปิดและการเร่งความร่วมมือ
- Shawn Ligocki เข้าร่วม Busy Beaver Challenge ในปี 2022 และรื้อฟื้น วิธีภาษาของเทปปิด ที่ Marxen เคยสร้างไว้
- วิธีนี้ใช้รูปแบบบนเทปของเครื่องทัวริงเพื่อให้กรอบคณิตศาสตร์แบบรวมสำหรับแสดงว่าเครื่องจะไม่หยุดทำงาน
- Ligocki เขียนบล็อกโพสต์แนะนำเทคนิคนี้ แต่ยังไม่รู้วิธีเขียนโปรแกรมที่ครอบคลุมทุกกรณี
- หลัง Justin Blanchard เข้าร่วมโครงการ เขาได้ลงมือทำให้เป็นจริง และผู้มีส่วนร่วมอีกสองคนก็ช่วยเพิ่มความเร็วในการรันอย่างมาก
- ภายในไม่กี่เดือน วิธีภาษาของเทปปิดก็กลายเป็นหนึ่งในเครื่องมือที่ทรงพลังที่สุดของทีม
- เทคนิคนี้ยังจัดการ 10 เครื่อง จาก 43 Skelet machines ที่ Georgiev ทิ้งไว้ได้ด้วย
- Ligocki มองว่าผลลัพธ์นี้คงไม่เกิดขึ้นจากการมีส่วนร่วมของคนเพียงคนเดียว
Skelet #1, Skelet #17 และ Coq
- Skelet #1 เป็นเครื่องที่สลับระหว่างช่วงที่คาดเดาได้กับช่วงที่ดูโกลาหล
- ในเดือนมีนาคม 2023 Ligocki และ Pavel Kropitz เสริมเทคนิคการจำลองแบบเร่งความเร็วอายุ 30 ปีของ Marxen และ Buntrock เพื่อวิเคราะห์ Skelet #1
- Skelet #1 ต้องผ่านมากกว่า 1 ล้านล้าน × 1 ล้านล้านขั้นจึงเข้าสู่วงจรซ้ำ และวงจรนั้นยาวกว่า 8 พันล้านขั้น
- mei โปรแกรมเมอร์ autodidact วัย 21 ปี เรียนรู้ Coq แล้วแปลหลักฐานหลายชิ้นของ Busy Beaver Challenge ไปเป็น Coq
- mei ยังย้ายหลักฐานการไม่หยุดทำงานของ Skelet #1 จาก Ligocki และ Kropitz ไปเป็น Coq ด้วย ทำให้ผลลัพธ์นั้นมั่นคงยิ่งขึ้น
- Skelet #17 เป็นอีกเครื่องยากที่ Chris Xu สร้างจุดเปลี่ยนสำคัญได้
- หลักฐานของ Xu ยอดเยี่ยมมาก แต่มีสัญชาตญาณทางคณิตศาสตร์ที่ยากต่อการย้ายไปเป็นรูปแบบละเอียดเข้มงวดที่ Coq ต้องการ
- ทีมต้องการหลักฐานที่ทำซ้ำได้อย่างสมเหตุสมผล ไม่ใช่หลักฐานในลักษณะ “รันโปรแกรมไป 6 เดือน”
หลักฐาน Coq 40,000 บรรทัด
- ในเดือนเมษายน 2024 ผู้มีส่วนร่วมหน้าใหม่ที่รู้จักกันเพียงนามแฝง mxdys เข้าร่วมการทำหลักฐาน Coq ให้เสร็จสมบูรณ์
- แม้แต่ทีมเองก็ไม่รู้ว่่า mxdys อยู่ที่ไหนหรือมีภูมิหลังส่วนตัวอย่างไร
- วันที่ 10 พฤษภาคม mxdys โพสต์ใน Discord ว่า “The Coq proof of BB(5) is finished.”
- ภายในไม่กี่สัปดาห์ mxdys รวมเทคนิคและผลลัพธ์ของชุมชนเข้าด้วยกันจนกลายเป็น หลักฐาน Coq 40,000 บรรทัด ฉบับเดียวที่สมบูรณ์
- หลักฐานเผยแพร่ไว้ในรีโพซิทอรี Coq-BB5
- Yannick Forster ผู้เชี่ยวชาญ Coq จาก Inria ตรวจทานหลักฐานนี้ และประเมินว่าไม่ใช่งานที่จัดรูปแบบอย่างเป็นทางการได้ง่าย
- ผลคือได้ยืนยันว่าเครื่อง 47,176,870 ขั้นที่ Marxen และ Buntrock พบเมื่อกว่า 30 ปีก่อน คือ Busy Beaver ตัวที่ห้าจริง
- Georgiev เล่าว่าเขาไม่คิดว่าปัญหานี้จะถูกแก้ได้ภายในช่วงชีวิตของตน
- Allen Brady เสียชีวิตเมื่ออายุ 90 ปีในวันที่ 21 เมษายน 2024 เพียงหนึ่งเดือนก่อนหลักฐานจะเสร็จสมบูรณ์
BB(6) และขอบเขตถัดไป
- ผู้มีส่วนร่วมใน Busy Beaver Challenge เริ่มเตรียมบทความวิชาการอย่างเป็นทางการเพื่ออธิบายผลลัพธ์นี้
- บทความดังกล่าวจะเสริมหลักฐาน Coq ของ mxdys ด้วยหลักฐานที่มนุษย์อ่านเข้าใจได้
- สมาชิกบางส่วนของทีมเริ่มขยับไปยัง Busy Beaver ตัวถัดไป
- mxdys และ Racheline พบอุปสรรคที่ดูเหมือนยากจะข้ามใน BB(6)
- อุปสรรคนี้คือเครื่อง 6 กฎที่มีปัญหาการหยุดทำงานคล้าย Collatz conjecture
- เครื่องนี้ถูกเรียกว่า Antihydra
- ความเชื่อมโยงระหว่างเครื่องทัวริงกับ Collatz conjecture ย้อนกลับไปได้ถึงบทความปี 1993 ของ Pascal Michel แต่ Antihydra ดูเหมือนเป็นเครื่องที่เล็กที่สุดซึ่งยังแก้ไม่ได้หากไม่มีการทะลุกรอบเชิงแนวคิดทางคณิตศาสตร์
- Scott Aaronson มองว่า BB(5) อาจเป็นเลข Busy Beaver ตัวสุดท้ายที่มนุษยชาติจะได้รู้
- ผู้มีส่วนร่วมบางคนวางแผนจะศึกษาปัญหาแปรผันของ Busy Beaver ต่อไป แต่ไม่ใช่ทุกคนที่จะยังอยู่ในทิศทางเดียวกัน
- Stérin ระบุว่า Busy Beaver Challenge ทำให้เขามั่นใจในประสิทธิภาพของการวิจัยแบบร่วมมือออนไลน์ และเขาต้องการพัฒนาเครื่องมือซอฟต์แวร์เพื่อช่วยโครงการความร่วมมือในสาขาคณิตศาสตร์อื่น ๆ
1 ความคิดเห็น
ความคิดเห็นใน Hacker News
มีคอมเมนต์ที่ Scott Aaronson เขียนเกี่ยวกับผลลัพธ์นี้: https://scottaaronson.blog/?p=8088
และยังมีเธรดใหญ่เมื่อต้นปีนี้เกี่ยวกับ “leisure-class beavers” ด้วย:
https://news.ycombinator.com/item?id=40453221
https://news.ycombinator.com/item?id=38113792
https://news.ycombinator.com/item?id=37910297
เดิมที ปัญหา Busy Beaver ก็มีตัวแปรดัดแปลงหลายแบบอยู่แล้ว หนึ่งในนั้นคือ busy beaver เชิงฟังก์ชันที่นิยามด้วย lambda calculus [1]
เพราะวัดขนาดโปรแกรมเป็นบิตแทนจำนวนสถานะ จึงตัดสินค่าได้มากกว่า โดยฝั่งทัวริงแมชชีนตอนนี้มีแค่ 6 ค่า แต่แบบนี้ไปได้ถึง 37 แล้ว ช่องว่างระหว่างค่าสูงสุดที่รู้จักกับค่าที่ใหญ่เกิน Graham's Number ก็ห่างกันเพียง 13 บิตของโปรแกรมเท่านั้น ตัวแปรที่ใกล้เคียงกัน [2] สามารถอธิบายตรง ๆ ด้วย Kolmogorov complexity ได้ และ Mikhail Andreev มองว่าสิ่งนี้สำคัญต่อการประยุกต์ใช้ทฤษฎีสารสนเทศ [3]
[1] https://oeis.org/A333479
[2] https://oeis.org/A361211
[3] https://arxiv.org/pdf/1703.05170
https://oeis.org/A141475 เจออันนี้ แต่ที่นี่สำหรับ 5 กลับออกมาเป็น 27 ล้านล้าน
จำได้ลาง ๆ ว่าเคยดูวิดีโอที่อธิบายนิยามนั้น
เคยทำงานอยู่หลายปีกับวิศวกรคนหนึ่งที่เก่งมหาศาล ฉลาดจนแทบเข้าใจไม่ไหว และไต่ระดับ IC ได้เร็วกว่าใครก็ตามที่ผมเคยเห็นในบริษัทเทคระดับหัวกะทิ
เขาลาออกไปเมื่อหลายปีก่อน พอถามว่าจะทำอะไรต่อ เขาบอกว่าจะไปศึกษาที่ ปัญหา Busy Beaver ผมเลยสงสัยว่าผู้มีส่วนร่วมแบบไม่เปิดเผยตัวตนชื่อ mxdys ที่ปิดงานพิสูจน์เชิงรูปนัยของ BB(5) ในบทความนี้จะใช่คนคนนั้นไหม แต่ก็คงไม่มีวันรู้
ผมไม่เห็นผลตอบแทน และถ้าเป็นปัญญาระดับนั้น ก็น่าเอาไปแก้ปัญหาที่เกี่ยวกับการทำให้โลกดีขึ้นมากกว่า
บทความ Busy Beaver ต้นฉบับของ Tibor Radó ชื่อ “On Non-Computable Functions” จริง ๆ แล้วอ่านค่อนข้างง่ายและสนุก
เวอร์ชันสมัยใหม่ที่มีคำอธิบายประกอบเพิ่มเติมอยู่ที่นี่: https://data.jigsaw.nl/Rado_1962_OnNonComputableFunctions_Re...
สิ่งที่โดดเด่นตรงนี้คือหลักฐานพิสูจน์เป็น Coq proof
เลยสงสัยว่านี่จะเป็นครั้งแรกหรือไม่สำหรับหลักฐานพิสูจน์สำคัญที่ถูกทำขึ้นในตัวช่วยพิสูจน์ทฤษฎีบทตั้งแต่ต้น แทนที่จะเป็นการย้ายหลักฐานที่รู้อยู่แล้วเข้าไปใน theorem prover ภายหลัง ก่อนหน้านี้ก็มีหลักฐานพิสูจน์ที่ใช้คอมพิวเตอร์ช่วยอยู่แล้ว แต่กรณีทฤษฎีบทสี่สีหรือข้อคาดการณ์ของ Kepler นั้นเพิ่งถูกย้ายไปสู่สภาพแวดล้อมการตรวจพิสูจน์เชิงรูปนัยทีหลัง
ปัญหาหลักคือทั้งตัวตัดสินและหลักฐานแบบทำมือยังไม่ได้จัดระเบียบและค่อนข้างน่าสงสัยอยู่บ้าง โดยเฉพาะ Skelet #1 ต้องใช้โปรแกรมเฉพาะทางเพื่อเร่งไปจนถึงแพตเทิร์นสุดท้าย [0] และ Skelet #17 นั้น Xu ต้องเขียนเหตุผลแน่น ๆ ยาว 7 หน้าเพื่อพิสูจน์ว่าไม่หยุดทำงาน [1] หลักฐานพิสูจน์ Coq ฉบับเต็มให้ความน่าเชื่อถือที่ผลลัพธ์เหล่านี้จำเป็นต้องมีอย่างยิ่ง
[0] https://www.sligocki.com/2023/03/13/skelet-1-infinite.html
[1] https://discuss.bbchallenge.org/t/skelet-17-does-not-halt/18...
https://github.com/ccz181078/Coq-BB5/blob/main/BB52Theorem.v
https://en.m.wikipedia.org/wiki/Four_color_theorem
ผมอาจเข้าใจคำว่า “สภาพแวดล้อมการตรวจพิสูจน์เชิงรูปนัย” ไม่ตรงนัก แต่เท่าที่ทราบ ทฤษฎีบทสี่สีก็เป็นสิ่งที่ถูกพิสูจน์ด้วยคอมพิวเตอร์ตั้งแต่แรก Kempe เคยพยายามพิสูจน์ไว้เดิมแต่มีข้อบกพร่อง แม้มันจะช่วยวางเครื่องมือพื้นฐานบางส่วนให้กับหลักฐานภายหลัง และสุดท้ายทฤษฎีบทนี้ก็ดูเหมือนจะถูกพิสูจน์ด้วยคอมพิวเตอร์
Busy Beaver ตัวนี้ถูกค้นพบในปี 1990 และเป็นไปได้มากว่าการไล่เรียงเครื่องทั้งหมดขนาด 5 ก็เกิดขึ้นไม่นานหลังจากนั้น
ขอแสดงความยินดีกับทีม ตอนนี้ก็ถือว่าปัญหาการหยุดของโปรแกรม เครื่องทัวริง 5 สถานะ 2 สัญลักษณ์ ภายใต้เทปว่างถูกแก้แล้ว
สงสัยว่ามีใครเคยลองใช้เทคนิคเดียวกันกับกรณี 2 สถานะ 4 สัญลักษณ์หรือยัง โดยทั่วไปสัญลักษณ์มักทรงพลังกว่าสถานะ แต่ระดับนั้นก็น่าจะพอรับมือได้ และอาจมีผลลัพธ์ที่คาดไม่ถึงด้วย ส่วน 6 สถานะ 2 สัญลักษณ์ กับ 2 สถานะ 5 สัญลักษณ์ ดูเหมือนทั้งคู่จะจัดการยาก และอาจยากถึงขั้นพิสูจน์ได้ว่าแก้ยากก็ได้ อีกอย่าง มีแนวคิดที่ทั้งเหลวไหลแต่กลับแพร่หลายอย่างประหลาดว่ามนุษย์อาจหยั่งรู้คำตอบของปัญหาการหยุดได้ด้วยตาในใจหรือกลศาสตร์ควอนตัมในสมอง แต่แน่นอนว่าในการพิสูจน์ครั้งนี้ไม่มีอะไรแบบนั้นมาเกี่ยวข้อง
เท่าที่ทราบ แค่ตัวตัดสินที่ใช้อยู่ตอนนี้ก็เพียงพอจะพิสูจน์ได้แล้วว่าเคสที่เหลือทั้งหมดของ 2×4 ไม่หยุด ดังนั้นถ้าไม่มีข้อผิดพลาดใหญ่ในการออกแบบตัวตัดสิน ก็จะได้ว่า Σ(2,4) = 2,050 และ S(2,4) = 3,932,964 จากแชมป์ปัจจุบัน เพียงแต่ผลลัพธ์ยังไม่ได้ถูกรวบรวมไว้ในที่เดียว
สำหรับ 2×5 มี Hydra และสำหรับ 6×2 มี Antihydra ซึ่งทั้งคู่คำนวณลูปเดียวกัน ต่างกันแค่จุดเริ่มต้นกับเงื่อนไขการหยุดเท่านั้น ข้อคาดเดามาตรฐานคือ ลูปนี้มีการแจกแจงสม่ำเสมอใน mod 2 โดยเกี่ยวข้องกับปัญหา 3/2 ของ Mahler และถ้าพิสูจน์ข้อคาดเดานั้นได้ ก็จะได้ขอบบนและขอบล่างของสัดส่วนสะสมของ 0 และ 1 ซึ่งแทบจะแน่ใจได้ว่าจะพิสูจน์การไม่หยุดของทั้งสองเครื่องได้ แน่นอนว่ายังไม่มีวิธีพิสูจน์ที่รู้จัก
พวกเขาใช้ตัวสร้างบทพิสูจน์บนฐานทฤษฎีตรรกะชื่อ Aleph* และในเวลานั้นก็เป็นที่รู้กันมาแล้ว 1,500 ปีว่า ZFC ไม่สามารถสถาปนา BB(18) ได้ เมื่อเทียบกับปี 2024 โปรแกรมใดก็ตามก่อนยุค Aleph* ไม่สามารถแม้แต่ในทางทฤษฎีจะถูกใช้ตรวจสอบบทพิสูจน์แบบ brute force เพื่อแก้ BB(18) ได้ ต่างจากทุกวันนี้ที่ในทางทฤษฎีเรายังสามารถไล่เรียงและตรวจสอบบทพิสูจน์ใน ZFC เพื่อแก้ BB(??) ได้
จุดยืนที่ว่า “มนุษย์หยั่งรู้คำตอบของปัญหาการหยุดได้” หมายถึงอะไรทำนองนี้ เท่าที่รู้ก็ไม่มีเหตุผลเชิงทฤษฎีที่หนักแน่นว่าประวัติศาสตร์อนาคตแบบนี้เป็นไปไม่ได้ และเพราะ busy beaver คำนวณไม่ได้ มนุษย์จึงต้องพัฒนาทฤษฎีใหม่เพื่อสร้างโปรแกรมที่จำเป็น ผลงานของผลลัพธ์นี้ย่อมต้องยกให้บางสิ่ง และเมื่อในเวลานั้นยังไม่มีโปรแกรมนั้นอยู่ ก็จะยกให้การคำนวณอย่างเดียวไม่ได้
สงสัยว่าเป็นไปได้ไหมที่โปรแกรมไม่หยุดทั้งหมดที่มีความยาว 5 จะบังเอิญล้วน พิสูจน์ได้ว่าไม่หยุด
“ข้อเท็จจริงที่ว่า Σ(5) = 1,915 และ S(5) = 2,358,064 จะไม่มีวันถูกพิสูจน์ หรือถ้าพบขอบล่างที่ใหญ่กว่า ก็ให้นำค่านั้นมาแทนในการคาดการณ์นี้ได้”
เหตุผลคือมีโอกาสสูงที่ธรรมชาติได้ฝังปัญหาที่จับต้องยากพอ ๆ กับข้อคาดเดา Goldbach อย่างน้อยหนึ่งปัญหาไว้ท่ามกลางเครื่อง 5 สถานะที่ยังค้างอยู่ พูดอีกอย่างคือ มีโอกาสสูงที่จะมีรูปแบบเวียนซ้ำแบบไม่หยุดที่เกินความสามารถในการรับรู้ของเรา โชคดีที่คำทำนายนี้ไม่กลายเป็นจริง แต่ก็เฉียดไปเพียงสถานะเดียว
[0] Allen Brady, "The Busy Beaver Game and the Meaning of Life", in Rolf Herken (ed.), The Universal Turing Machine: A Half-Century Survey, Oxford University Press, 1988, pp. 259–277. This chapter can also be found in the 2nd ed., Springer, 1995, pp. 237–254.
ถ้าเป็นเชิงปฏิบัติ คนอื่นก็ตอบไปแล้ว ถ้าเป็นเชิงคณิตศาสตร์ ถ้า BB(5) ตัดสินไม่ได้ก็คงน่าประหลาดใจมาก เพราะ 5 สถานะ 2 สัญลักษณ์เล็กเกินกว่าจะเข้ารหัสพฤติกรรมที่ตัดสินไม่ได้ได้
อย่างไรก็ตาม จากผลของทฤษฎีบทความไม่สมบูรณ์ ย่อมต้องมี n บางค่าที่คณิตศาสตร์มาตรฐานไม่สามารถพิสูจน์ค่า BB(n) ได้ ในช่วงไม่กี่ปีที่ผ่านมา มีหลายคนศึกษาว่าจะหาค่า n ดังกล่าวและกดให้ต่ำลงได้แค่ไหน โดยสถิติปัจจุบัน[0]คือ 745 สถิตินี้น่าจะกดลงได้อีก แต่ถึงอย่างนั้นก็ยังห่างมากระหว่างค่ามากที่สุดที่เรารู้คือ 5 กับค่าน้อยที่สุดที่เรารู้ว่าไม่อาจรู้ได้คือ 745
[0] เผื่อสงสัยว่า “คณิตศาสตร์มาตรฐาน” คืออะไร ปัจจุบันสถิตินี้ใช้ได้กับทั้ง ZFC และ PA ดังนั้นอย่างน้อยสำหรับ PA ก็น่าจะกดให้ต่ำลงได้อีกดูมีความเป็นไปได้ จนถึงตอนนี้ดูเหมือนว่ายังไม่มีใครพบวิธีที่ดีกว่า ZFC สำหรับ PA แต่ก็น่าจะเป็นไปได้ไม่ใช่หรือ?
“เมื่อสี่วันก่อน mxdys และ Racheline ซึ่งเป็นผู้มีส่วนร่วมอีกสองคน ได้ค้นพบกำแพงที่ดูเหมือนข้ามได้ยากสำหรับ BB(6): เครื่อง 6 กฎที่ปัญหาการหยุดมีลักษณะคล้ายข้อคาดเดา Collatz อันโด่งดังว่าจัดการยาก ความเชื่อมโยงระหว่างเครื่องทัวริงกับข้อคาดเดา Collatz ย้อนกลับไปได้ถึงงานของนักคณิตศาสตร์ Pascal Michel ในปี 1993 แต่เครื่องใหม่ที่ชื่อ ‘Antihydra’ ดูเหมือนจะเป็นเครื่องที่เล็กที่สุดซึ่งไม่น่าจะแก้ได้หากไม่มีความก้าวหน้าเชิงแนวคิดทางคณิตศาสตร์”
เคยเขียนโปรแกรมแก้ปัญหา การตัดชิ้นวัสดุคงคลัง(https://en.wikipedia.org/wiki/Cutting_stock_problem) เป็นโปรเจกต์ส่วนตัว
สต็อกมีการตัดชิ้นส่วนรูป /---/, /---|, |---| และเพราะไม่อยากสิ้นเปลืองวัสดุตรงการตัด 45 องศา จึงใช้โปรแกรมที่มีอยู่เดิมไม่ได้ หรือไม่ก็ไม่อยากใช้ คำอธิบายที่ว่า Brady ตัดทอนซับทรีของการค้นหาที่ความแตกต่างไม่สำคัญออกไปเพื่อเพิ่มประสิทธิภาพการค้นหา BB(4) นั้นน่าสนใจ เพราะค่อนข้างคล้ายกับสิ่งที่ฉันทำตอนเร่งความเร็วโปรแกรมของตัวเอง
ตามบล็อกของ Scott Aaronson บอกว่า เครื่องทัวริง 5 สถานะ มีอยู่ 16,679,880,978,201 เครื่อง
สงสัยว่ารู้ไหมว่ามีกี่เปอร์เซ็นต์ที่หยุด แก้ไข: จำนวนเครื่องทัวริง n สถานะคือ (4n + 1)^(2n) เจอข้อมูลสำหรับ n เล็ก ๆ ที่คล้ายกับการวิเคราะห์ที่อยากได้แล้ว: https://github.com/LukasKalbertodt/beaver
หาไม่เจอบนเว็บ bbchallenge.org แต่เครื่องทั้งหมดถูกจำแนกไว้แล้ว
โดยสรุปแล้ว บทพิสูจน์ค่อนข้างสั้น เมื่อรวมช่องว่างและคอมเมนต์แล้วมี Coq 19,000 บรรทัด
จากประสบการณ์ของผม ถ้าแปลงเป็นบทความวิชาการแบบดั้งเดิม ก็น่าจะสั้นกว่าเวอร์ชัน Coq มาก แน่นอนว่าความยาวของบทพิสูจน์ไม่ใช่มาตรวัดความยากหรือความซับซ้อน แต่ก็ใช้เป็นเกณฑ์คร่าว ๆ ได้มาก
เมื่อพูดถึงขีดจำกัดของความรู้มนุษย์ เรามักนึกถึงทฤษฎีบทที่พิสูจน์ได้แต่ซับซ้อนเกินไปจนไม่มีมนุษย์คนใดเข้าใจได้ทั้งหมด บางทีบทพิสูจน์ที่ซับซ้อนที่สุดที่เรามีก็คือ การจัดประเภทกลุ่มอย่างง่ายเชิงจำกัด ซึ่งยาวหลายพันถึงหลายหมื่นหน้า และอาจมีคนบนโลกนี้แทบไม่มีเลย หรืออาจไม่มีแม้แต่คนเดียว ที่เข้าใจทั้งหมดอย่างสมบูรณ์
อย่างที่บทความบอกไว้ BB(6) อาจตัดสินไม่ได้ก็ได้ แต่ก็อาจเป็นไปได้เช่นกันว่ามีบทพิสูจน์ยาวหลายล้านหน้าที่เกินเอื้อมสำหรับมนุษยชาติ