มุมมองของเทอเรนซ์ เต๋า ต่อ proof checker และ AI copilot สำหรับคณิตศาสตร์
(scientificamerican.com)- เมื่อการพิสูจน์ทางคณิตศาสตร์ถูก ทำให้เป็นรูปแบบทางการ อย่างเข้มงวดมากขึ้น เครื่องมืออย่าง Lean ก็กำลังตรวจสอบการพิสูจน์ของมนุษย์ และเปลี่ยนฐานความไว้วางใจของการทำงานร่วมกันขนาดใหญ่
- เมื่อไลบรารีมาตรฐานอย่าง mathlib สะสมมากขึ้น อุปสรรคในการเริ่มทำ formalization ตั้งแต่ทฤษฎีบทระดับปริญญาตรีไปจนถึงสาขาใหม่ ๆ ก็กำลังลดลง
- ในการทำ formalization ของข้อคาดการณ์ PFR มีผู้เข้าร่วมมากกว่า 20 คนแบ่งกันรับผิดชอบขั้นตอนย่อย ๆ ของการพิสูจน์ ส่วนเทอเรนซ์ เต๋าเน้นจัดการทิศทางโดยรวมมากกว่าตรวจทีละบรรทัด
- ในตอนนี้ AI มีบทบาทใกล้เคียงกับ proof copilot ที่ช่วยงาน formalization, verification และงานซ้ำ ๆ มากกว่าการ “แก้” คณิตศาสตร์โดยตรง
- งานวิจัยคณิตศาสตร์อาจเปลี่ยนไปเป็นงานที่ชัดเจนและแบ่งหน้าที่มากขึ้น เช่น การกำหนดทิศทางโดยมนุษย์ การทำ formalization รายละเอียด การฝึก AI และการตีความการพิสูจน์ของ AI
Formalization กำลังเปลี่ยนการทำงานร่วมกันในคณิตศาสตร์
- งานวิจัยคณิตศาสตร์แบบดั้งเดิมมักใกล้เคียงกับการร่วมมือกันของคนจำนวนน้อย และเต๋ามองว่าโดยทั่วไป ประมาณ 5 คน น่าจะใกล้ขีดจำกัดบนของขนาดทีมร่วมมือ
- หากมี automatic proof checker ก็สามารถร่วมมือกับคนหลายร้อยคนที่ไม่รู้จักกันได้
- ผู้ร่วมงานส่งโค้ดขึ้นไป แล้ว Lean compiler ตรวจสอบให้
- ความไว้วางใจไม่ต้องพึ่งพาแค่ความสัมพันธ์ส่วนตัว แต่ยืนยันได้จากผลของ formal verification
- ตอนทำ formalization ของผลลัพธ์ล่าสุดเกี่ยวกับข้อคาดการณ์ Polynomial Freiman-Ruzsa(PFR) มีผู้เข้าร่วม มากกว่า 20 คน
- แบ่งการพิสูจน์ออกเป็นขั้นตอนเล็ก ๆ จำนวนมาก
- ผู้เข้าร่วมแต่ละคนรับผิดชอบการพิสูจน์หนึ่งขั้นตอน
- เต๋าจัดการทิศทางการดำเนินงานโดยรวม มากกว่าตรวจการมีส่วนร่วมทุกอย่างทีละบรรทัด
นักคณิตศาสตร์ทุกคนไม่จำเป็นต้องเป็นโปรแกรมเมอร์
- ในโปรเจกต์ formalization สามารถแบ่งบทบาทกันได้
- บางคนโฟกัสที่ ทิศทางทางคณิตศาสตร์
- บางคนเชี่ยวชาญในการแปลงชิ้นส่วนคณิตศาสตร์เล็ก ๆ ให้เป็น formal proof
- นักคณิตศาสตร์ที่ไม่คุ้นเคยกับคอมพิวเตอร์อย่าง Peter Scholze ก็สามารถเข้าร่วมโปรเจกต์ Lean ได้
- เมื่อแบ่งโจทย์คณิตศาสตร์ขนาดใหญ่ออกเป็นชิ้นเล็ก ๆ ก็สามารถมีส่วนร่วมกับงานย่อยเฉพาะส่วนได้ แม้ไม่เข้าใจทฤษฎีทั้งหมด
ความใช้งานได้จริงที่ Lean, mathlib และการค้นหาสร้างขึ้น
- หนึ่งในเหตุผลสำคัญที่ทำให้ formal mathematics ใช้งานได้จริง คือความก้าวหน้าของไลบรารีคณิตศาสตร์มาตรฐาน
- Lean มีโปรเจกต์ขนาดใหญ่ชื่อ mathlib
- ทฤษฎีบทพื้นฐานของคณิตศาสตร์ระดับปริญญาตรี เช่น แคลคูลัสและทอพอโลยี ค่อย ๆ ถูกนำเข้าไปในไลบรารีทีละรายการ
- เป้าหมายคือยกระดับไลบรารีให้ถึงระดับบัณฑิตศึกษา
- เมื่อเป็นเช่นนั้น การทำ formalization ให้สาขาคณิตศาสตร์ใหม่ ๆ ก็จะง่ายขึ้น
- การสร้างการพิสูจน์จำเป็นต้องค้นหาทฤษฎีบทที่ได้รับการยืนยันแล้วว่าเป็นจริง ดังนั้น เสิร์ชเอนจิน ที่ฉลาดขึ้นจึงสำคัญมากขึ้นด้วย
- หลังจากทำ formalization ของโปรเจกต์ PFR ทั้งหมดแล้ว การคอมไพล์เพื่อตรวจสอบใช้เวลาเพียงประมาณ 30 นาที
- คอขวดอยู่ที่ความง่ายในการใช้งาน ความเป็นมิตรต่อผู้ใช้ และการที่ผู้คนปรับตัวเข้ากับเครื่องมือ มากกว่าพลังประมวลผล
- Lean ถูกประเมินว่าเป็นภาษา formal ที่มีคอมมูนิตี้คึกคักที่สุดในปัจจุบัน
- สำหรับโปรเจกต์ผู้เขียนคนเดียว ภาษาอื่นอาจเหมาะกว่า
- Lean เรียนรู้ง่าย และมีไลบรารีกับคอมมูนิตี้ที่ดี
- ในอนาคตอาจถูกทางเลือกอื่นแทนที่ได้ แต่ปัจจุบันเป็นภาษา formal ที่ครองตลาด
ต้นทุนของ formalization ยังสูง
- เต๋ามองว่าแม้เขาสามารถทำ formalization ให้บางโปรเจกต์ได้ แต่ในปัจจุบันอาจต้องใช้เวลาของตัวเองถึง หนึ่งเดือน
- ยังไม่ถึงขั้นที่จะทำ formalization ให้ผลลัพธ์ทุกอย่างเป็นกิจวัตร
- กรณีที่ช่วยให้เรียนรู้ Lean ได้
- กรณีที่มีความสนใจสูงต่อความถูกต้องของผลลัพธ์
- ควรเลือกโปรเจกต์ที่ formalization ให้คุณค่าจริง
- เมื่อเทคโนโลยีดีขึ้น ต้นทุนของ formalization อาจลดลงได้
- ตอนนี้อาจใช้เวลานานกว่าวิธีเดิม 10 เท่า
- ต่อไปมีความเป็นไปได้ที่จะลดเหลือราว 2 เท่า และยิ่งกว่านั้นอาจต่ำกว่า 1 เท่า
AI อาจกลายเป็น copilot ของนักคณิตศาสตร์
- เต๋าจินตนาการว่าในอนาคตนักคณิตศาสตร์อาจไม่ต้องพิมพ์การพิสูจน์เอง แต่บอกอธิบายให้ระบบอย่าง GPT ฟัง แล้วให้ AI ลองทำ Lean formalization ระหว่างทาง
- หากผ่านการตรวจสอบ ก็สามารถมอบทั้งบทความ LaTeX และการพิสูจน์ Lean ไปพร้อมกันได้
- หากผู้ใช้ต้องการ ก็อาจเป็นผู้ช่วยที่ช่วยไปจนถึงการส่งวารสาร
- เส้นทาง formalization ที่เร็วที่สุดในปัจจุบันยังคงเป็นการให้มนุษย์สร้างไอเดียและร่างการพิสูจน์ก่อน
- ในระยะยาว อาจมีโปรเจกต์ที่มนุษย์ทำ formalization ของชิ้นส่วนเล็ก ๆ โดยไม่รู้การพิสูจน์ทั้งหมด แล้วให้ AI กับมนุษย์ช่วยกันเชื่อมต่อจนพิสูจน์ทฤษฎีบทใหญ่ได้
- เต๋ามองว่าวิธีแบบนี้ต้องใช้เวลา หลายปี กว่าจะเป็นไปได้
- เทคโนโลยีปัจจุบันยังไม่เพียงพอ และ formalization ก็ยังเป็นงานที่ลำบากอยู่
ระยะห่างจากภาพว่า “คณิตศาสตร์จะถูกแก้ได้หมด”
- Tony Wu และ Christian Szegedy เคยกล่าวว่า ภายใน 2–3 ปี คณิตศาสตร์จะ “ถูกแก้” ในความหมายที่ว่าเครื่องจักรจะค้นหาการพิสูจน์ได้ดีกว่ามนุษย์
- เต๋าเห็นว่าใน 3 ปี AI อาจมีประโยชน์ต่อนักคณิตศาสตร์และเกิดความก้าวหน้าชัดเจนได้ แต่ไม่ได้มองว่าคณิตศาสตร์จะถูกแก้ได้หมด
- AI อาจเป็น copilot ที่ขอความช่วยเหลือได้เมื่อขั้นตอนหนึ่งในการพิสูจน์ดูเหมือนจริง แต่มนุษย์ยังมองไม่ออกทันที
- แม้ AI จะทำคณิตศาสตร์ได้ในระดับเดียวกับที่มนุษย์ทำอยู่ตอนนี้ นักคณิตศาสตร์มนุษย์ก็อาจขยับไปทำคณิตศาสตร์ในระดับที่สูงขึ้น
- AI อาจทำให้เกิดวิธีพิสูจน์ทฤษฎีบททีละหลายร้อยหรือหลายพันบทได้
- นักคณิตศาสตร์มนุษย์รับบทเป็นผู้กำกับว่า AI ควรทำอะไร
- เต๋ามองว่าการคาดการณ์กรอบเวลา 2–3 ปีสำหรับการเปลี่ยนแปลงเช่นนี้ค่อนข้างเร่งรัด
ความเข้าใจการพิสูจน์และการพิสูจน์ที่ AI สร้าง
- การพิสูจน์ทางคณิตศาสตร์ไม่ใช่เพียงขั้นตอนยืนยันว่าจริง แต่ยังเป็นกระบวนการทำความเข้าใจว่าทำไมจึงจริงด้วย
- ในอนาคตอันใกล้ AI น่าจะเริ่มจากการทำงานน่าเบื่อและจุกจิกให้เป็นอัตโนมัติ ส่วนมนุษย์ยังคงกำหนดทิศทาง
- หาก AI สร้างการพิสูจน์ที่เข้าใจยากและดูไม่สวยงาม มนุษย์สามารถนำการพิสูจน์นั้นกลับมาวิเคราะห์ใหม่ได้
- เช่น ในการพิสูจน์ที่ได้ข้อสรุปจากสมมติฐาน 10 ข้อ สามารถตรวจสอบได้ว่าถอดสมมติฐานหนึ่งข้อออกแล้วยังเป็นจริงหรือไม่
- อาจเกิดนักคณิตศาสตร์รูปแบบใหม่ที่ สกัด insight จากการพิสูจน์ที่ AI สร้างขึ้น
- การพิสูจน์ของ AI ในช่วงแรกอาจดูเหมือนไม่มี insight
- ผู้คนสามารถทำให้การพิสูจน์นั้นเข้าใจง่ายขึ้นและค้นหาโครงสร้างได้
ปัญหาที่ยังไม่คลี่คลายและข้อจำกัดของ AI
- การพิสูจน์ข้อคาดการณ์ที่ยังไม่แก้ได้ จำเป็นต้องเริ่มจากการแบ่งออกเป็นชิ้นส่วนที่เล็กลงก่อน
- การเปลี่ยนปัญหาให้ยากขึ้นนั้นง่ายกว่าการเปลี่ยนให้เป็นปัญหาที่ง่ายลงมาก
- เต๋ามองว่า AI ยังไม่ได้แสดงความสามารถที่เหนือกว่ามนุษย์ในงานแยกย่อยปัญหานี้
- การใช้ AI เพื่อเสนอความเป็นไปได้ของการเชื่อมโยงระหว่างหลายสาขาเป็นเรื่องน่าสนใจ
- อัตราความสำเร็จในปัจจุบันยังต่ำ
- จากข้อเสนอ 10 ข้อ อาจมีเพียง 1 ข้อที่น่าสนใจ และอีก 9 ข้อไม่มีประโยชน์
- เต๋ามองว่าในอนาคตส่วนนี้อาจเปลี่ยนไปได้
ปัญหาด้านข้อมูลของความรู้คณิตศาสตร์
- หนึ่งในปัญหาของการฝึก AI คณิตศาสตร์คือข้อมูลมีไม่เพียงพอ
- บทความออนไลน์สามารถใช้ฝึกได้ แต่ สัญชาตญาณทางคณิตศาสตร์ จำนวนมากไม่ได้อยู่ในบทความ
- บทสนทนาระหว่างนักคณิตศาสตร์
- การบรรยาย
- วิธีแนะนำดูแลนักศึกษา
- ความพยายามที่ล้มเหลวและกระบวนการแก้ไข
- การพิสูจน์ที่ตีพิมพ์เป็นผลลัพธ์ที่ถูกบีบอัด และผู้คนมักตีพิมพ์เฉพาะกรณีที่สำเร็จ
- ข้อมูลที่มีคุณค่าจริง ๆ คือกระบวนการที่ลองทำบางอย่างแล้วไม่สำเร็จ และแก้ไขอย่างไร
- ในอนาคต กระบวนการลองทำวิจัยและความล้มเหลวอาจถูกบันทึกไว้ เพื่อใช้ฝึก AI หรือช่วยให้นักวิจัยคนอื่นไม่ล้มเหลวซ้ำ
- เต๋ายกตัวอย่างสถานการณ์ที่ยินยอมให้บันทึกกระบวนการวิจัย เพื่อใช้ระบบอย่าง AI Lean ขั้นสูงในปี 2040
การเปลี่ยนผ่านสู่คณิตศาสตร์ที่ชัดเจนยิ่งขึ้น
- ความรู้คณิตศาสตร์จำนวนมากถูกกักอยู่ในหัวของนักคณิตศาสตร์แต่ละคน และมีเพียงส่วนน้อยมากที่ถูกทิ้งไว้ในรูปแบบชัดเจน
- เมื่อ formalization เพิ่มขึ้น ความรู้โดยนัยก็จะถูกเปลี่ยนเป็น ความรู้ที่ชัดเจน มากขึ้น
- ตำราที่ผ่าน formalization แล้วอาจนำไปสู่ตำราแบบโต้ตอบได้
- เริ่มจากคำอธิบายการพิสูจน์ในระดับสูง
- ขั้นตอนที่ไม่เข้าใจสามารถขยายดูรายละเอียดเพิ่มเติมได้
- หากต้องการ ก็สามารถเจาะลงไปถึงระดับสัจพจน์ได้
- วิธีแบบนี้อาจทำให้นักคณิตศาสตร์ในสาขาหนึ่งมีส่วนร่วมกับอีกสาขาได้ง่ายขึ้น
- สามารถระบุงานย่อยของโจทย์ใหญ่ได้อย่างแม่นยำ
- แม้ไม่เข้าใจทั้งหมด ก็ยังเข้าร่วมในชิ้นส่วนที่จำเป็นได้
1 ความคิดเห็น
ความคิดเห็นจาก Hacker News
https://archive.is/Idouw
วลี project manager mathematicians ทำให้นึกถึงงานเขียนเสียดสีของ Edsger Dijkstra จากปี 1975 เรื่อง “A letter to my old friend Jonathan” [1] และบทความติดตาม [2]
เดิมทีเป็นงานวิจารณ์ให้เห็นว่ามันจะน่าขันแค่ไหนหากเอาวิธีสร้างซอฟต์แวร์ไปใช้กับคณิตศาสตร์ แต่ในบางแง่ก็ดูมีวิสัยทัศน์ล่วงหน้า
ประเด็นหลักคือการวิจารณ์ความไร้สาระของการใช้ทรัพย์สินทางปัญญากับความรู้ โดยเฉพาะ ความจริงทางคณิตศาสตร์ และก็น่าโชคดีที่ในการเคลื่อนไปสู่ระบบอัตโนมัติแบบทุกวันนี้ ประเด็นนั้นดูไม่น่าเป็นห่วงมากนัก
[1]: https://www.cs.utexas.edu/users/EWD/transcriptions/EWD04xx/E...
[2]: https://www.cs.utexas.edu/users/EWD/transcriptions/EWD05xx/E...
เป็นบทความที่มีมุมมองลึกซึ้ง แต่สิ่งที่ขาดไปคือประเด็นที่ว่า LLM กำลัง นามธรรมในแบบเหนือมนุษย์มากขึ้นเรื่อยๆ
Tao บอกว่า “ทำให้ปัญหายากขึ้นนั้นง่าย แต่ทำให้มันง่ายลงนั้นยาก และ AI ยังไม่เคยแสดงให้เห็นว่ามันเก่งกว่ามนุษย์ในเรื่องนี้” แต่ด้วยวิธีการทำงานของ LLM มันอาจทำให้เกิดความเข้าใจเชิงลึกในระดับที่สูงกว่ามากได้
ตอนนี้มันยังใกล้เคียงกับผู้ช่วย ผู้ตรวจสอบข้อเท็จจริง และตัวจัดการงานน่าเบื่อ แต่ในไม่ช้ามันจะกลายเป็นสิ่งที่เสนอ insight ได้ ตอนนี้ LLM ก็ฝังตัวแทนข้อมูลและบีบอัดความรู้อยู่แล้ว และอาจมี insight ที่เราไม่เห็น
ช่วงที่ Hinton ยกตัวอย่างความเกี่ยวข้องกันระหว่างระเบิดนิวเคลียร์กับกองปุ๋ยหมัก: https://www.youtube.com/watch?v=Gg-w_n9NJIE&t=4613s
มันก็แค่เครื่องจักรที่ถูกฝึกให้เลียนแบบวิธีที่มนุษย์เขียน และไม่มีข้อมูลฝึกที่จำเป็นต่อการเลียนแบบบางสิ่งที่ฉลาดกว่ามนุษย์
ผมไม่สงสัยเลยว่า machine learning จะก้าวข้ามสติปัญญามนุษย์ได้ แต่คอขวดคือการหาวิธีให้มันเรียนรู้จากผลลัพธ์ของตัวเองโดยไม่มีมนุษย์คอยแทรกแซง แทนที่จะถดถอยกลับไปหาข้อความทั้งหมดของโลก
Ramanujan แทบไม่ได้รับการศึกษาอย่างเป็นระบบ และเคยเจอเพียงหนังสือคณิตศาสตร์ไม่กี่เล่ม แต่กลับค้นพบสิ่งยิ่งใหญ่ทางคณิตศาสตร์ได้ ซึ่งถ้ามองจากมุมข้อมูลฝึกของโมเดล machine learning แล้ว ก็แทบจะไม่มีข้อมูลอะไรเลย
ผมใช้เวลาราว 10 วินาทีในการเรียบเรียงเป็นคำพูด แต่ถ้ารู้ข้อมูลที่จำเป็น คำตอบก็ชัดเจนอยู่แล้ว
Hinton บอกว่านี่แสดงถึงการคิดแบบอุปมาอุปไมย แต่บนออนไลน์ก็มีทั้งบทความเกี่ยวกับสวนและเรื่องฟิสิกส์ของกองปุ๋ยหมักอยู่มาก และมีโอกาสสูงที่ ChatGPT จะเคยเห็นมันระหว่างการฝึกแล้ว
เพราะงั้นตัวอย่างนี้จึงดูเหมือนกรณีที่ควบคุมไม่ได้ว่า LLM เคยเห็นคำตอบในข้อความฝึกมาแล้วโดยพฤตินัย
ช่วงถัดมาในวิดีโอที่ Ilya พูดว่า “มี proof of existence อยู่ มนุษย์ก็มีสมองที่เป็นโครงข่ายประสาท” (https://youtu.be/Gg-w_n9NJIE?t=4966) ก็น่าสนใจเช่นกัน ผมค่อนข้างเห็นด้วยกับมุมมองที่ว่าสมองมนุษย์ก็เป็นโครงข่ายประสาท แต่ก็มีข้อโต้แย้งมากมายว่าระบบประสาทจริงไม่ได้ทำงานแบบ 8 บิต และยังมีความต่างด้านชนิดของเซลล์ DNA ฮอร์โมน และสภาพแวดล้อมทางเคมีของเซลล์ด้วย จึงมองว่าเป็นทางแยกเชิงปรัชญา
ทำได้ภายในไม่กี่นาทีถึงไม่กี่ชั่วโมง
แต่ถ้าจะได้ผู้เชี่ยวชาญมนุษย์เพิ่มอีกหนึ่งคน ก็ต้องมีคนที่ชอบคณิตศาสตร์ในฐานะอาชีพปรากฏขึ้น ผ่านการศึกษาหลายสิบปีและการเชี่ยวชาญขั้นสูง และก็ยังไม่มีอะไรรับประกันว่าคนนั้นจะไปได้จนสุดทางและมีระดับพอจะผลักดันแนวหน้าของความรู้
ระหว่างที่รอเวลานั้น เราอาจสร้างผู้เชี่ยวชาญ AI ที่ทำงานแบบขนานกันได้เป็นล้านล้านตัว
สมองมนุษย์มีแบนด์วิดท์ต่ำในการดูดซับข้อมูลใหม่ แต่เครื่องจักรสามารถคัดลอกความรู้ทั้งชีวิตได้ภายในไม่กี่วินาที สนทนาเป็นพันบทพร้อมกันแบบขนาน และยัง serialize ส่วนหนึ่งของสมองเพื่อส่งไปให้อีก AI ได้ด้วย หากไปถึงขั้น programmable matter ก็อาจสร้าง computronium แบบทวีคูณ และไปถึงจุดโอเมก้าที่ทำวิจัยหลายพันปีได้ภายในไม่กี่วินาทีก็เป็นไปได้
ไม่รู้อะไรเกี่ยวกับคณิตศาสตร์เลย แต่ทำให้นึกถึงประวัติศาสตร์ซอฟต์แวร์ สมัยก่อนโปรเจ็กต์น่าทึ่งอย่าง RollerCoaster Tycoon แทบจะเป็นผลงานที่คนคนเดียวสร้างขึ้น
หลังจากนั้นวิศวกรรมซอฟต์แวร์ก็ถูกทำให้เป็นโมดูล คล้ายกับที่อธิบายไว้ในการสัมภาษณ์ และตอนนี้มันกลายเป็นสายการประกอบขนาดใหญ่ที่คนอย่างฉันปั๊ม React ออกมาเพื่อหาเลี้ยงชีพ ซึ่งดูเหมือนว่าผลิตภาพต่อคนหรือทักษะที่ต้องใช้จะเข้าใกล้ 0
พอวงการอยู่ในยุคทอง อัจฉริยะคนหนึ่งจะเก็บเรื่องไว้ในหัวได้เป็นร้อยอย่างและสร้างงานที่ดีที่สุดออกมา แต่เมื่อสิ่งนั้นถูกแทนที่ด้วยสายการประกอบ ก็ให้ความรู้สึกว่าวงการนั้นจะไม่สามารถสร้างสิ่งที่มีคุณค่าจริง ๆ ได้อีกต่อไป
วิศวกรรมซอฟต์แวร์ไม่ได้หยุดทำสิ่งเจ๋ง ๆ ตรงกันข้ามเลยด้วยซ้ำ
พักเรื่องตลกไว้ก่อน สักวันหนึ่งเมื่อถึงเวลาต้องแก้บั๊กวิกฤต ฝีมือจริงจะปรากฏออกมา การที่ผลิตภัณฑ์หรือบริการมีเสถียรภาพและเริ่มทำกำไรได้ ไม่ได้แปลว่านักพัฒนาเดิมหายไปแล้ว หรือจะไม่มีใครทำเรื่องใหญ่ ๆ ได้อีก
คำบอกว่าวงการนี้ไม่สร้างสิ่งที่มีคุณค่าจริง ๆ อีกแล้วนั้นผิดมาก
มันให้ความรู้สึกเหมือนเอามหาวิหารที่คน 100 คนสร้างตลอด 100 ปี ไปเทียบกับกระท่อมที่คนคนเดียวสร้างเสร็จในเดือนเดียว กระท่อมก็ยังตั้งอยู่และมีที่ให้อาศัย แต่ไม่ใช่มหาวิหาร
ฝั่งเว็บดีเวลอปเมนต์นี่ แค่จะตามดู Python อย่างเดียวยังยากมาก เพราะมีเฟรมเวิร์กและเทคโนโลยีเยอะเกินไปในทุกเฟืองเล็ก ๆ ของวงล้อ
ทักษะโดยทั่วไปเป็นไปตามการกระจายแบบลอค-นอร์มัล ดังนั้นคนที่โดดเด่นเป็นพิเศษจึงมีน้อยอยู่แล้ว และวงการขนาดเล็กในระยะแรกมักขาดโครงสร้างสนับสนุน ทำให้มีแต่คนที่มีพรสวรรค์สุดโต่งเท่านั้นที่อยู่รอดได้ จนความหนาแน่นของคนระดับท็อปสูงผิดธรรมชาติ
การฝืนจับเฟรมเวิร์กล่าสุด 47 ตัวมามัดรวมกันเพื่อปั๊มแอปบันทึกรายการสิ่งที่ต้องทำ กับการสร้างผลกระทบที่มีความหมาย เป็นงานที่ต่างกันโดยพื้นฐาน
ในมุมมองต้นทุนต่อผลตอบแทน มีจุดเหมาะสมเฉพาะที่แรงมากในทางเลือกที่จะพ่นโค้ดราคาถูกออกมาจำนวนมาก แทนที่จะลงทุนระยะยาวกับงานใหญ่ และยิ่งวงการสุกงอมมากขึ้น ระดับทักษะขั้นต่ำที่พาไปถึงจุดนั้นก็ยิ่งต่ำลง
องค์กรที่มุ่งเน้นการฝึกคนระดับท็อปก็มีไม่มาก ดังนั้นยิ่งวงการใหญ่ขึ้นก็ยิ่งอธิบายได้ง่ายว่าทำไมทักษะเฉลี่ยถึงถูกปล่อยให้ลดลง และถ้าจัดการกับการกระจายนี้ผิดพลาด ค่าใช้จ่ายในการแก้ภายหลังก็อาจสูงมาก
บทพิสูจน์ที่ตรวจสอบด้วยคอมพิวเตอร์ เป็นพื้นที่ที่ AI อาจมีประโยชน์ได้ในเวลาไม่นานนัก แต่สิ่งนั้นอาจใกล้เคียงกับโครงข่ายประสาทของเอนจินหมากรุกมากกว่า LLM เต็มรูปแบบ
การพิสูจน์ทุกอย่างด้วยมือทั้งน่าเบื่อและใช้เวลานาน จึงมีการใช้ solver จำนวนมากอยู่แล้ว แต่แทคติกหรือ solver มักลำบากเมื่อโยนทฤษฎีบทและเลมมาจำนวนมากเกินไปเข้าไป
โครงข่ายประสาทในฐานะเครื่องค้นหาที่ใช้การจับคู่รูปแบบเพื่อหาเลมมาที่เกี่ยวข้องจึงเหมาะมาก
การอุปนัยและการรวมเอกภาพระดับสูงก็เป็นการสังเคราะห์โค้ดในทางปฏิบัติเช่นกัน และการไล่วนต้นไม้ไวยากรณ์ที่เป็นไปได้ทั้งหมดแบบ brute force นั้นไม่มีประสิทธิภาพอย่างยิ่ง
ตัว solver เองก็ทำ backtracking อยู่แล้ว ดังนั้นถึง AI จะเสนอเลมมาที่ไร้ประโยชน์ 95% ก็ยังไม่เป็นไร และอาจดีกว่าการค้นหาด้วยมืออย่างมหาศาล
แต่ก็ยังไม่แน่ใจว่าบทพิสูจน์ที่ตรวจสอบด้วยคอมพิวเตอร์จะดีต่อการสื่อสารเสมอไปหรือไม่ บทพิสูจน์ที่มนุษย์อ่านได้มีระดับนามธรรมสูงและละรายละเอียดไว้ ไม่ใช่แค่เพราะเรื่องความยาวเท่านั้น
ปัญหาหลักคือมันต้องเชื่อมโยงกับ นิยามเชิงรูปนัย ของวัตถุทางคณิตศาสตร์ที่ใช้ในบทพิสูจน์
แต่มนุษย์ไม่ได้คิดแบบนั้นเวลาเขียนหรืออ่านบทพิสูจน์ ปกติจะมีความเข้าใจระดับสูงแบบไม่เป็นทางการก่อนว่าตัวเองกำลังทำอะไรอยู่ในเชิง “ความหมายโดยรวม” แล้วจึงเติมรายละเอียดเชิงรูปนัยเท่าที่จำเป็น
โค้ดคอมพิวเตอร์พอใช้แนวนี้ได้ในระดับหนึ่ง เพราะอรรถศาสตร์เชิงรูปนัยของภาษามันใกล้กับแบบจำลองในหัวเรามากกว่า แต่คณิตศาสตร์โดยทั่วไปมีเป้าหมายต่างออกไป
กลยุทธ์ sledgehammer ของ Isabelle จะรวมตัวพิสูจน์ทฤษฎีบทอัตโนมัติอย่าง E, Z3, SPASS และ Vampire เข้าด้วยกัน เพื่อพยายามพิสูจน์หรือหักล้างเป้าหมาย
ในทางทฤษฎีมันดูดี แต่ในทางปฏิบัติมักได้บทพิสูจน์แบบสร้างกลับที่ใช้เลมมาดูสุ่ม ๆ 12 ข้อ และบทพิสูจน์แบบนี้ทั้งอ่านไม่รู้เรื่องและเปราะบางมาก
ดูไม่น่าเป็นไปได้ที่ AI จะแก้ปัญหานี้ได้อย่างน่าอัศจรรย์
ปัจจุบันโครงข่ายประสาทมี sample efficiency ต่ำมาก และชุดข้อมูลคณิตศาสตร์เชิงรูปนัยก็เล็กกว่าชุดข้อมูลอย่างโค้ด Python มาก
เมื่อไม่กี่เดือนก่อน Terence Tao ได้บรรยายยอดเยี่ยมในหัวข้อนี้ และพูดถึง การใช้ Lean อย่างละเอียดมากขึ้น: https://www.youtube.com/watch?v=AayZuuDDKP0
มีนักคณิตศาสตร์ที่กำลังทำงานวิจัยอยู่คนหนึ่งบอกว่าให้ GPT-4o พิสูจน์บทตั้งเสริมที่น่าจะเป็นของใหม่ได้
“คู่หูของฉันเป็นนักคณิตศาสตร์ และสัปดาห์ก่อนเขาเพิ่งลองใช้ ChatGPT เป็นครั้งแรกเพื่อพิสูจน์บทตั้งเสริมบางข้อสำหรับงานวิจัย เราสงสัยอยู่แล้วว่าทฤษฎีบทเหล่านั้นน่าจะเป็นจริง และก็พอมีแนวทางคร่าว ๆ อยู่บ้าง แต่เขาไม่ได้เป็นผู้เชี่ยวชาญในข้อความประเภทนั้น นี่เป็นครั้งแรกที่เราได้หลักฐานพิสูจน์จากโมเดลที่ทั้งถูกต้องและมีประโยชน์
บทตั้งเสริมข้อแรกเป็นสิ่งที่ผู้ร่วมงานค้นพบจากการคำนวณเมื่อ e มีค่าน้อย ๆ ตอนแรก ChatGPT หาหลักฐานพิสูจน์ไม่เจอ จนกระทั่งมีคนบอกให้ลองใช้ฟังก์ชันเมอบิอุส
https://chatgpt.com/share/9ee33e31-7cec-4847-92e4-eebb48d4ff...
ข้อที่สองดูเป็นมาตรฐานมากกว่า และ Mathematica ก็น่าจะทำได้เช่นกัน แต่ Mathematica ไม่ได้ให้การอนุมานที่เรียบร้อยแบบนี้ จึงยังมีประโยชน์อยู่
https://chatgpt.com/share/7335f11d-f7c0-4093-a761-1090a21579...”
สิ่งพวกนี้กำลังเก่งขึ้นอย่างน่ากลัวในด้านการให้เหตุผลและหัวข้อหนัก ๆ
ถ้าวงการแมชชีนเลิร์นนิงยังคงมุ่งเพิ่ม ความสามารถแบบระบบ 2 เพื่อเสริมการคิดแบบระบบ 1 ที่เป็นค่าเริ่มต้นของ LLM ต่อไป สถานการณ์ก็น่าจะเข้มข้นขึ้นมาก
สิ่งที่นึกออกคือ generatingfunctionology
นี่เป็นความจำที่น่าประทับใจ ไม่ใช่การให้เหตุผลใหม่
เราคิดมันในรูปผลรวมของ การแบ่งแบบมีลำดับ แทนที่จะเป็นผลรวมของการแบ่งที่มีสัมประสิทธิ์ |τ|! แต่แน่นอนว่าสองอย่างนี้เท่ากัน
ถ้าเป็นการแบ่งแบบมีลำดับเชิงวัฏจักร กล่าวคือใช้สัมประสิทธิ์ (|τ|-1)! แทน |τ|! จะได้ 0 แทนที่จะเป็น (-1)^e
หลักฐานเชิงจัดหมู่ของ Beren คือสร้างฟังก์ชันหนึ่งต่อหนึ่งระหว่างการแบ่งเชิงวัฏจักรแบบมีลำดับที่มีความยาวคู่และคี่ โดยเลือกสมาชิกพิเศษหนึ่งตัว แล้วถ้ามันอยู่เดี่ยว ๆ ก็รวมเข้ากับส่วนถัดไป แต่ถ้าไม่ได้อยู่เดี่ยวก็แยกมันออกมาเป็นส่วนของตัวเอง
สำหรับกรณีลำดับเชิงเส้นก็ทำคล้ายกัน โดยเริ่มจากสมาชิกตัวสุดท้าย แต่ถ้าสมาชิกตัวสุดท้ายอยู่เดี่ยวในส่วนสุดท้าย การแบ่งนั้นจะจับคู่ไม่ได้ จึงไปทำแบบเวียนกลับกับสมาชิกตัวก่อนหน้าแทน
สุดท้ายทุกอย่างจะถูกจับคู่หมด เหลือเพียงการแบ่งที่ทุกสมาชิกอยู่แยกกันและอยู่ในลำดับเดิมเท่านั้น จากนั้นผลรวมของเครื่องหมายตามความเป็นคู่คี่ของขนาดเซตเดิมก็นำไปสู่ข้อความตั้งต้นเดิม
ก็ไม่รู้ด้วยซ้ำว่าผลรวมเหนือ “τ ≤ τ” มีทั้งหมดกี่พจน์ และมันเชื่อมกับการตั้งข้างซ้ายหรือข้างขวาในข้อ 3 ครั้งหนึ่ง แล้วสรุปอีกข้างหนึ่งได้อย่างไร ซึ่งก็ไม่ตรงกันอยู่ดี
ความจริงคือ ChatGPT แค่นึกฟังก์ชัน เมอบิอุส ของ lattice การแบ่งออก แล้วท่องมันออกมาโดยไม่มีการพิสูจน์ จากนั้นก็พูดเพ้อที่ดูเผิน ๆ เหมือนจะเข้าท่า
ทั้งที่การตั้งฟังก์ชันเมอบิอุสนั่นแหละคือแก่นสำคัญ และคำถามนี้แทบจะเท่ากับให้พิสูจน์ว่าฟังก์ชันนั้นมีรูปแบบเช่นนั้น
แถมสูตรทั่วไปที่ ChatGPT ให้มายังผิดเล็กน้อยด้วย และถูกเฉพาะกรณี |σ| = 1 ซึ่งเป็นกรณีสำคัญต่อหลักฐานพิสูจน์ปัจจุบัน
เรื่องนี้จริง ๆ เห็นได้ทันทีโดยไม่ต้องใช้กลไกฟังก์ชันเมอบิอุสทั้งชุดอย่างชัดแจ้ง เพียงกำหนดให้ N(t,e) เป็นจำนวนการแบ่งที่แยกเป็นคลาสสมมูล t คลาส แล้วใช้อุปนัยแบบพื้นฐานจากสมการเวียนกลับ N(t,e+1)=N(t-1,e)+tN(t,e)
มีอยู่สามอย่างที่เด่นชัดจากบทสัมภาษณ์นี้
อย่างแรก Tao มองอนาคตที่ความเข้าใจเชิงคณิตศาสตร์ถูก “ผลิต” เหมือนผลผลิตชนิดอื่นในสังคม และพูดถึง project manager mathematicians เขาเห็นว่าสาเหตุที่คณิตศาสตร์ยังไม่ถูกทำให้เป็นอุตสาหกรรมถึงขั้นนั้น มาจากการขาดแคลนเครื่องมือ และมองว่า AI กับ proof assistant อาจปฏิวัติส่วนนี้ได้ แต่การปฏิสัมพันธ์และการชี้นำจากมนุษย์ก็ยังจำเป็นอยู่
อย่างที่สอง มี ความรู้โดยนัย จำนวนมากที่ไม่ถูกใส่ไว้ในงานวิจัย ความรู้ประเภทสัญชาตญาณหรือความรู้จากความล้มเหลวมีความสำคัญมาก จนแม้แต่นักคณิตศาสตร์ระดับสูงก็ยังต้องคุยกันเพื่อไม่ให้ทำพลาดซ้ำแบบเดิม
อย่างที่สาม เราอาจคิดได้ง่ายว่าคณิตศาสตร์ถูกทำให้เป็นแบบรูปนัยมากพออยู่แล้ว แต่ในงานวิจัยจริงมีความรู้ร่วมจำนวนมากที่ถูกสมมติไว้ การทำหลักฐานพิสูจน์ให้อยู่ในรูปที่ proof assistant เข้าใจได้ จะช่วยให้คนจำนวนมากขึ้นเข้าใจได้ว่าจริง ๆ แล้วเกิดอะไรขึ้น
อย่างที่ Tao เคยแสดงให้เห็นในบรรยายของโครงการ Polymath บทสัมภาษณ์นี้ทำให้เห็นว่าเขาเป็นคนที่มองหาวิธีใหม่ ๆ สำหรับการทำวิจัยคณิตศาสตร์อยู่เสมอ
ณ ตอนนี้ มันอาจเป็นโครงการที่ทำได้เฉพาะเมื่อ ผู้ได้เหรียญ Fields อย่าง Tao หรือ Scholze มีเวลามากพอจะใช้กับการพิสูจน์มากขึ้น 10 เท่า
เพิ่งคุยกับนักวิจัยหลังปริญญาเอกคณิตศาสตร์ระดับแนวหน้าคนหนึ่งมา เขาบอกว่าในคนรอบตัวไม่มีใครใช้ lean4 กับงานจริงเลย
ถ้าเป็นนักวิจัยช่วงต้นอาชีพ การเชื่อสัญชาตญาณตัวเองและส่งบทความตีพิมพ์น่าจะยังเป็นทางเลือกที่ดีกว่า
ถ้าจะมองประเด็นนี้ให้ถูกต้อง คงใช้ความประทับใจจากคนไม่กี่คนไม่ได้
ในทางกลับกัน สาขาอย่างทอพอโลยีมิติต่ำที่มีสไตล์แบบ อาศัยสัญชาตญาณมากกว่า ก็น่าจะมีคนใช้ proof checker น้อยกว่า
คำว่าอาศัยสัญชาตญาณในที่นี้ไม่ได้แปลว่าเข้มงวดน้อยกว่า เพียงแต่หลักฐานพิสูจน์แบบรูปภาพของความสมมูลเชิงโฮโมโทปีนั้นย้ายให้ Lean เข้าใจได้ยากกว่าการไล่เรียงอสมการมาก
อนึ่ง ฉันอยู่ฝั่งเรขาคณิต/ทอพอโลยี และยังไม่เคยเห็นหรือได้ยินว่ามีใครใช้เครื่องมือพวกนี้เลย
https://lean-lang.org/
https://github.com/leanprover/lean4
“ถ้า AI ให้บทพิสูจน์ที่เข้าใจไม่ได้และดูไม่สวยงาม เราก็สามารถนำมันมาวิเคราะห์ได้ ถ้าบทพิสูจน์นี้ใช้สมมติฐาน 10 ข้อเพื่อให้ได้ข้อสรุปหนึ่งข้อ แล้วถ้าลบสมมติฐานออกไป 1 ข้อ บทพิสูจน์จะยังใช้ได้อยู่ไหม? วิทยาศาสตร์ลักษณะนี้ยังไม่มีอยู่ เพราะตอนนี้ยังมีบทพิสูจน์ที่ AI สร้างขึ้นไม่มากนัก แต่จะมีนักคณิตศาสตร์รูปแบบใหม่ที่รับคณิตศาสตร์ที่ AI สร้างขึ้นมา แล้วทำให้มันเข้าใจได้มากขึ้น” ตรงกับความคิดของฉันเรื่องการออกแบบ public API ของโค้ดอย่างแม่นยำ
เดิมทีนี่เป็นบทบาทที่มีแต่ผู้พัฒนาที่ชำนาญเท่านั้นที่ทำได้ แต่ตอนนี้มันอาจถูกทำให้ง่ายลงอย่างมากและเข้าถึงได้สำหรับทุกคน