ความคืบหน้าของความร่วมมือระหว่างมนุษย์·AI·ตัวช่วยพิสูจน์ ในปัญหา ‘Claude Cycles’ ของ Knuth

 (twitter.com/BoWang87)
2 คะแนน โดย GN⁺ 2026-03-30 | 1 ความคิดเห็น | แชร์ทาง WhatsApp
  • ส่วนที่ยังไม่ถูกแก้ของ ปัญหาการแยกแบบ Hamiltonian ที่ Donald Knuth เสนอ ได้รับการขยายการแก้ไขด้วยความร่วมมือระหว่างมนุษย์และ AI
  • Claude ค้นพบวิธีแก้สำหรับค่า m คี่ จนถูกตั้งชื่อว่า “Claude’s Cycles” และต่อมาพบว่า 996 จาก 11,502 วงจร สามารถทำให้เป็นกรณีทั่วไปสำหรับทุกค่า m คี่ได้
  • Dr. Ho Boon Suan ใช้ GPT-5.4 Pro ทำ บทพิสูจน์ยาว 14 หน้าและการตรวจสอบเชิงคำนวณถึง m=2000 สำหรับกรณี m คู่ที่ m≥8
  • Dr. Keston Aquino-Michaels ค้นพบวิธีประกอบที่เรียบง่ายซึ่งใช้ได้ทั้ง m คี่และคู่ ด้วย เวิร์กโฟลว์แบบหลายเอเจนต์ของ GPT และ Claude
  • Dr. Kim Morrison ทำการตรวจสอบเชิงรูปนัยของคำตอบของ Knuth ด้วย Lean proof assistant จนเกิดเป็น ระบบนิเวศความร่วมมือระหว่างมนุษย์·AI·เครื่องมือพิสูจน์ ที่สมบูรณ์

การขยายความร่วมมือเพื่อแก้ปัญหา Claude’s Cycles

  • ส่วนที่ยังไม่ถูกแก้ของ ปัญหาการแยกแบบ Hamiltonian ที่ Donald Knuth เสนอ ได้รับการแก้ด้วยความร่วมมือระหว่างมนุษย์และ AI
    • ในช่วงแรก Claude ใช้เวลาค้นหาราวหนึ่งชั่วโมงเพื่อหาวิธีแก้สำหรับ m คี่ และ Knuth ได้ตั้งชื่อสิ่งนี้ว่า “Claude’s Cycles”
  • ต่อมาในบทความฉบับอัปเดต มีการระบุว่าในกรณีฐาน m=3 มี Hamiltonian cycle อยู่ทั้งหมด 11,502 วงจร และในจำนวนนั้น 996 วงจร สามารถทำให้เป็นกรณีทั่วไปสำหรับทุกค่า m คี่ได้
    • Knuth ยืนยันว่าในจำนวนนั้นมี 760 แบบแยก “ชนิด Claude” ที่ใช้ได้จริง
  • สำหรับกรณี m คู่ นั้น Claude ยังทำไม่สำเร็จ แต่ Dr. Ho Boon Suan ใช้ GPT-5.4 Pro เขียน บทพิสูจน์ยาว 14 หน้า สำหรับกรณี m≥8 และทำ การตรวจสอบเชิงคำนวณถึง m=2000
  • จากนั้น Dr. Keston Aquino-Michaels ได้ค้นพบวิธีประกอบที่เรียบง่ายซึ่งใช้ได้กับทั้ง m คี่และ m คู่ ผ่าน เวิร์กโฟลว์แบบหลายเอเจนต์ที่ใช้ GPT และ Claude ร่วมกัน
  • Dr. Kim Morrison ได้นำคำตอบสำหรับกรณีคี่ของ Knuth ไปทำให้เป็นรูปนัยและตรวจสอบใน Lean proof assistant
    • ผลลัพธ์คือเกิด ระบบนิเวศความร่วมมือทางคณิตศาสตร์ที่สมบูรณ์ ซึ่งมนุษย์, ระบบ AI หลายตัว และ เครื่องมือพิสูจน์เชิงรูปนัย ทำงานร่วมกันแบบขนาน
  • กระบวนการทั้งหมดนี้เริ่มจากการที่ AI หนึ่งตัวช่วยแก้ปัญหาเฉพาะหน้า ก่อนจะขยายไปสู่ โมเดลการวิจัยคณิตศาสตร์แบบใหม่ ที่อาศัย ความร่วมมือระหว่างหลาย AI·มนุษย์·ตัวช่วยพิสูจน์
  • บทความล่าสุดเผยแพร่อยู่บนเว็บไซต์ Stanford CS Faculty (www-cs-faculty.stanford.edu/~knuth/papers/)

บทความที่เกี่ยวข้อง

1 ความคิดเห็น

 
GN⁺ 2026-03-30
ความคิดเห็นจาก Hacker News

  • ฉันพูดมาตลอดว่า AI จะได้เหรียญ Fields ก่อนที่จะไปบริหาร McDonald's
    คณิตศาสตร์สำหรับมนุษย์ให้ความรู้สึกยากเหมือนใช้ค้อนขันสกรู
    LLM เก่งเรื่องการสำรวจแบบตื้นแต่กว้าง จึงค้นพบรูปแบบทางคณิตศาสตร์ใหม่ ๆ ได้มาก
    คาดว่าในอนาคตจะเปลี่ยนจาก LLM ไปเป็น การเสริมแรงแบบ AlphaGo ที่อิงกับต้นไม้ไวยากรณ์ของ Lean
    ถ้าสามารถเข้ารหัส ‘10 ทริก’ ที่นักคณิตศาสตร์ใช้เป็นเวกเตอร์แฝงได้ ก็ถือว่าจบเกม

    • ท้ายที่สุดแล้วทริกก็เป็นแค่ แพตเทิร์น ของนิพจน์เชิงตรรกะ
      เราคิดโดยอาศัยการอุปมาเชิงเรขาคณิต เช่น การนำพีชคณิตเรขาคณิตไปใช้กับปัญหาทฤษฎีจำนวน
      AI ที่เรียนรู้จากต้นไม้ Lean อาจมี ระบบสัญชาตญาณ ที่กว้างกว่ามนุษย์ก็ได้
      เหมือนกรณีที่ StockFish แสดงให้เห็นในหมากรุก แนวทางนี้ก็น่าศึกษาในมุมของ mechanistic interpretability
    • ฉันเป็นนักคณิตศาสตร์มืออาชีพ และสำหรับบทพิสูจน์ที่ดี สิ่งสำคัญคือ วิธีแทนปัญหา
      การหยิบทริกมาใช้นั้น LLM ก็ทำได้ดีอยู่แล้ว
      แต่ส่วนของการแทนปัญหาให้ถูกต้องยังเป็นหน้าที่ของมนุษย์ และมันก็เป็นเรื่องธรรมชาติ
    • ถ้าระบบสามารถฝึกให้ ค้นพบทริกใหม่ ๆ ได้ด้วยตัวเอง นั่นคงน่าทึ่งมาก
    • ฉันชอบประโยคที่ว่า “AI จะได้เหรียญ Fields ก่อนที่จะไปบริหาร McDonald's” มาก
      ฉันอยากเติมเวอร์ชันของตัวเองว่า “อาชีพสุดท้ายที่จะถูกทำให้เป็นอัตโนมัติคือ QA”
      คลื่นเทคโนโลยีรอบนี้ทำให้เราต้องกลับมาคิดใหม่ถึงธรรมชาติของงานใช้ความรู้ และนั่นจะทำให้เราคมขึ้น
    • ฉันเองก็กำลังค่อย ๆ ลองทำ ต้นแบบด้วยตัวเอง สำหรับแนวทางการเสริมแรงบนต้นไม้ Lean

  • ตั้งแต่เคยได้ยินคติ 4chan ที่ว่า “trolls trolling trolls” ฉันก็มองปฏิสัมพันธ์บนอินเทอร์เน็ตด้วยความระแวงมาตลอด
    ก่อนหน้านี้ก็รู้สึกว่า Reddit กลายเป็น ‘อินเทอร์เน็ตที่ตายแล้ว’ ไปแล้ว พอมาเห็นเธรดนี้ยิ่งแยกไม่ออกว่า ใครเป็นบอทหรือเป็นมนุษย์

    • ฉันคิดว่าข้อสังเกตนั้นสำคัญมาก
      เลยสร้างบริการชื่อ RememberBuddy — พื้นที่สำหรับเก็บข้อคิดในชีวิตประจำวันไว้ไม่ให้ลืม

  • วิวัฒนาการของ AI ด้านคณิตศาสตร์ดูเหมือนจะเดินตามเส้นทางที่ Greg Egan เคยคาดไว้ในนิยายยุค 90
    แก่นของคณิตศาสตร์จะไม่เปลี่ยน แต่เหตุผลที่เราทำมันจะเปลี่ยนไป
    ใน 『Diaspora』 ของ Egan การค้นพบทางคณิตศาสตร์ถูกพรรณนาเหมือน การขุดอัญมณีจากเหมืองเกลือ
    บางคนแสวงหาความงามอันบริสุทธิ์ของอัญมณีนั้นเอง ขณะที่บางคนมองหาคุณค่าเชิงปฏิบัติ
    สถานที่อย่างสถาบันวิจัยที่ Terence Tao ตั้งขึ้นในปัจจุบันก็แตะต้องอนาคตแบบนี้อยู่แล้ว
    ในระยะสั้น งานวิจัยแบบนี้จะช่วยยกระดับ ความสามารถของระบบ AI ในการสร้างข้อมูลที่ถูกต้องแม่นยำ อย่างมาก

  • บางคนคิดว่า การค้นพบความรู้เป็นเพียงการเลียนแบบพฤติกรรมในอดีต แต่ฉันไม่เห็นด้วย

  • ถ้ามีผู้เชี่ยวชาญคอยนำทางโมเดลให้ดี ปัญหาส่วนใหญ่ก็แก้ได้
    โมเดลเป็นเครื่องมือที่ยอดเยี่ยมสำหรับ ทำงานน่าเบื่อแทนผู้เชี่ยวชาญ แต่ในปัญหาซับซ้อนก็ยังมี จุดบอด อยู่

  • ฉันเห็นบางส่วนของ system prompt ในบทความ
    มีกฎว่า “ให้อัปเดต plan.md ทันทีหลังรัน exploreXX.py ทุกครั้ง”
    เลยสงสัยว่าทำไมพรอมป์แบบนี้ถึงช่วย เพิ่มประสิทธิภาพการแก้ปัญหาระดับสูง ได้

    • น่าจะเป็นกลไกที่ทำให้ เริ่มใหม่ได้โดยไม่ทำขั้นตอนหาย

  • เรากำลังเข้าใกล้วิสัยทัศน์ของ CEO OpenAI เรื่อง “intelligence as a subscription” มากขึ้นเรื่อย ๆ

  • การลดการสลับแท็บยังถูกประเมินค่าต่ำเกินไป
    ครึ่งหนึ่งของเครื่องมือ AI ไม่ใช่การต่อสู้เรื่อง UX แต่เป็นการต่อสู้เพื่อ ทำให้การเข้าถึงโมเดลมีเสถียรภาพ

  • “ถ้าให้ลิง 100 ตัวมีปืน 100 กระบอกกับวัสดุก่อสร้าง พวกมันจะสร้างบ้านหรือจะปล้นธนาคาร?”
    ถ้าได้ผลลัพธ์ออกมา ฉันก็อยากถามว่านั่นเป็น พฤติกรรมที่มีเจตนา หรือไม่

  • ฉันเห็นทวีตนี้

    • คอมเมนต์ส่วนใหญ่ดูเป็น รูปแบบประโยคที่ AI สร้างขึ้นอย่างชัดเจน — ซ้ำแนว “นั่นไม่ใช่ X แต่มันคือ Y”