AI ของ DeepMind แก้โจทย์โอลิมปิกคณิตศาสตร์นานาชาติได้ในระดับเหรียญเงิน
(deepmind.google)- ใน IMO 2024 ซึ่งเป็นสนามทดสอบสำคัญของการให้เหตุผลทางคณิตศาสตร์ระดับยาก AlphaProof และ AlphaGeometry 2 ของ Google DeepMind สามารถแก้ได้ 4 จาก 6 ข้อ ทำให้ AI ไปถึงผลงานระดับเหรียญเงินได้เป็นครั้งแรก
- ได้คะแนนรวม 28 คะแนน จาก 42 คะแนนเต็ม และทั้ง 4 ข้อที่แก้ได้ถูกให้เต็มทั้งหมด โดยขาดเพียง 1 คะแนนจากเกณฑ์เหรียญทองของปี 2024 ที่ 29 คะแนน
- การประเมินทำโดยนักคณิตศาสตร์ตามกติกาการให้คะแนนของ IMO โดยโจทย์พีชคณิตและทฤษฎีจำนวนเป็นหน้าที่ของ AlphaProof ส่วนเรขาคณิตเป็นหน้าที่ของ AlphaGeometry 2 ซึ่งผสานวิธีให้เหตุผลที่แตกต่างกัน
- โจทย์ทั้งหมดถูกแปลเป็น ภาษาคณิตศาสตร์เชิงรูปแบบ ด้วยมือก่อน ขณะที่เวลาการแข่งขันของนักเรียนคือ 2 ช่วง ช่วงละ 4.5 ชั่วโมง ระบบใช้เวลาตั้งแต่ไม่กี่นาทีสำหรับบางข้อไปจนถึงสูงสุด 3 วันสำหรับข้ออื่น
- ผลลัพธ์ครั้งนี้แสดงให้เห็นว่า AI ด้านคณิตศาสตร์ก้าวข้ามการคำนวณธรรมดาไปสู่การค้นหาและตรวจสอบบทพิสูจน์แล้ว แต่การต้องใช้ข้อมูลนำเข้าแบบเชิงรูปแบบและเวลาทำโจทย์ที่ยาวนานยังคงเป็นข้อจำกัดสำคัญ
ผลงานระดับเหรียญเงินใน IMO 2024
- Google DeepMind เปิดเผยระบบให้เหตุผลทางคณิตศาสตร์ AlphaProof และ AlphaGeometry 2 ซึ่งเป็นรุ่นปรับปรุงของระบบแก้โจทย์เรขาคณิต
- ทั้งสองระบบแก้โจทย์ได้ 4 จาก 6 ข้อของ International Mathematical Olympiad 2024
- AlphaProof: แก้โจทย์พีชคณิต 2 ข้อ และทฤษฎีจำนวน 1 ข้อ
- AlphaGeometry 2: พิสูจน์โจทย์เรขาคณิต 1 ข้อ
- โจทย์คอมบิเนทอริกส์ 2 ข้อยังแก้ไม่ได้
- แต่ละข้อมีคะแนนเต็ม 7 คะแนน รวมทั้งหมด 42 คะแนน
- ระบบได้เต็มทั้ง 4 ข้อที่แก้ได้ จึงได้ 28 คะแนน
- นี่เทียบได้กับช่วงบนของระดับเหรียญเงิน IMO ปี 2024
- เกณฑ์เหรียญทองของ IMO 2024 คือ 29 คะแนน และในการแข่งขันจริงมีผู้เข้าแข่งขัน 58 คนจากทั้งหมด 609 คนที่ทำถึงระดับเหรียญทอง
- นี่เป็นกรณีแรกที่ระบบ AI ทำผลงานใน IMO ได้ในระดับ ผู้ชนะเหรียญเงิน
วิธีประเมินและเงื่อนไขการแก้โจทย์
- ใช้โจทย์การแข่งขันที่ผู้จัด IMO จัดเตรียมไว้
- คำตอบถูกประเมินตามกติกาการให้คะแนนของ IMO
- ผู้ประเมินคือ Prof Sir Timothy Gowers ผู้ได้เหรียญทอง IMO และผู้ได้รับรางวัล Fields Medal และ Dr Joseph Myers ผู้ได้เหรียญทอง IMO 2 สมัยและประธานคณะกรรมการคัดเลือกโจทย์ IMO 2024
- เพื่อให้ระบบเข้าใจโจทย์ได้ โจทย์ทั้งหมดจึงถูกแปลเป็น ภาษาคณิตศาสตร์เชิงรูปแบบ ด้วยมือก่อน
- ในการแข่งขันจริง นักเรียนมีเวลาส่งคำตอบ 2 ช่วง ช่วงละ 4.5 ชั่วโมง
- ระบบ AI ใช้เวลาไม่กี่นาทีในการแก้หนึ่งข้อ และใช้เวลาสูงสุด 3 วันสำหรับข้ออื่น
- ในข้อที่ AlphaProof แก้ได้นั้น มีโจทย์ที่ยากที่สุดของ IMO 2024 รวมอยู่ด้วย ซึ่งมีผู้เข้าแข่งขันเพียง 5 คนที่แก้ได้
AlphaProof: การให้เหตุผลเชิงรูปแบบบน Lean
- AlphaProof เป็นระบบที่ฝึกให้พิสูจน์ข้อความทางคณิตศาสตร์ด้วยภาษารูปแบบของ Lean
- มันผสานโมเดลภาษาที่ผ่านการพรีเทรนกับอัลกอริทึมเสริมการเรียนรู้ของ AlphaZero
- AlphaZero คืออัลกอริทึมที่ใช้ให้ระบบเรียนรู้หมากรุก โชกิ และ Go ได้ด้วยตนเอง
- การใช้ภาษารูปแบบทำให้สามารถ ตรวจสอบความถูกต้อง ของบทพิสูจน์ที่มีการให้เหตุผลทางคณิตศาสตร์ได้
- ก่อนหน้านี้ ข้อมูลบทพิสูจน์เชิงรูปแบบที่มนุษย์เขียนมีน้อยมาก ทำให้การใช้ภาษารูปแบบในแมชชีนเลิร์นนิงมีข้อจำกัด
- แนวทางที่อิงภาษาธรรมชาติสามารถใช้ข้อมูลได้มากกว่ามาก แต่ก็อาจสร้างขั้นตอนการให้เหตุผลระหว่างทางหรือคำตอบที่ดูน่าเชื่อถือแต่ผิดพลาดได้
- DeepMind ปรับจูนโมเดล Gemini ให้แปลโจทย์ภาษาธรรมชาติเป็นข้อความเชิงรูปแบบโดยอัตโนมัติ และสร้างคลังโจทย์เชิงรูปแบบที่มีหลายระดับความยาก
- เมื่อได้รับโจทย์ AlphaProof จะสร้างคำตอบผู้สมัคร จากนั้นสำรวจขั้นตอนบทพิสูจน์ที่เป็นไปได้ใน Lean เพื่อพิสูจน์หรือหักล้างคำตอบเหล่านั้น
- บทพิสูจน์ที่ค้นพบและตรวจสอบแล้วจะถูกนำไปใช้เสริมความสามารถของโมเดลภาษาของ AlphaProof
- กระบวนการวนซ้ำนี้ถูกใช้เพื่อเพิ่มความสามารถในการแก้ปัญหาที่ยากขึ้น
- ระหว่างการเตรียมตัวสำหรับ IMO ระบบฝึกด้วยการพิสูจน์หรือหักล้างโจทย์หลายล้านข้อเป็นเวลาหลายสัปดาห์
- ระหว่างการแข่งขันเอง ก็ใช้ลูปการเรียนรู้ที่เสริมบทพิสูจน์ของโจทย์เวอร์ชันดัดแปลงที่สร้างขึ้นเองไปพร้อมกับค้นหาวิธีทำที่สมบูรณ์
AlphaGeometry 2: ขยายไปสู่โจทย์เรขาคณิตที่ยากขึ้น
- AlphaGeometry 2 เป็นเวอร์ชันที่ปรับปรุงครั้งใหญ่จาก AlphaGeometry
- ระบบนี้ใช้สถาปัตยกรรม นิวโร-ซิมโบลิกแบบไฮบริด ที่ผสานโครงข่ายประสาทกับการให้เหตุผลเชิงสัญลักษณ์
- โมเดลภาษาสร้างบนพื้นฐานของ Gemini
- ถูกฝึกใหม่ตั้งแต่ต้นด้วยข้อมูลสังเคราะห์ที่มากกว่ารุ่นก่อนหนึ่งลำดับขั้น
- ด้วยข้อมูลที่มากขึ้นและโมเดลที่ดีขึ้น จึงสามารถรับมือกับโจทย์เรขาคณิตที่ยากกว่าเดิม รวมถึงการเคลื่อนที่ของวัตถุ สมการมุม อัตราส่วน และระยะทาง
- เอนจินเชิงสัญลักษณ์ของ AlphaGeometry 2 เร็วกว่ารุ่นก่อน หลายสิบเท่า
- เมื่อได้รับโจทย์ใหม่ ระบบจะใช้กลไกแบ่งปันความรู้แบบใหม่เพื่อใช้ชุดผสมขั้นสูงจากต้นไม้การค้นหาที่ต่างกัน จัดการกับโจทย์ที่ซับซ้อนยิ่งขึ้น
- อัตราการแก้โจทย์เรขาคณิต IMO ในช่วง 25 ปีล่าสุด:
- ก่อนการแข่งขันปี 2024 AlphaGeometry 2 สามารถแก้โจทย์เรขาคณิต IMO ในช่วง 25 ปีล่าสุดได้ 83%
- AlphaGeometry รุ่นก่อนมีอัตราการแก้ได้ 53%
- ใน IMO 2024 ระบบแก้ Problem 4 ได้ภายใน 19 วินาทีหลังจากแปลงโจทย์เป็นข้อมูลนำเข้าเชิงรูปแบบ
การให้เหตุผลด้วยภาษาธรรมชาติและการใช้งานในอนาคต
- ในฐานะส่วนหนึ่งของงาน IMO นั้น DeepMind ยังทดลอง ระบบให้เหตุผลด้วยภาษาธรรมชาติ ที่อิงจาก Gemini และงานวิจัยล่าสุด
- ระบบนี้ไม่จำเป็นต้องแปลโจทย์เป็นภาษารูปแบบ และสามารถนำไปรวมกับระบบ AI อื่นได้
- DeepMind ได้ทดสอบแนวทางนี้กับโจทย์ IMO 2024 เช่นกัน และประเมินว่าผลลัพธ์มีแนวโน้มที่ดี
- วิธีวิทยาที่มีลักษณะเชิงเทคนิคมากกว่าของ AlphaProof ถูกเผยแพร่ในรูปของบทความ Nature
- DeepMind ตั้งเป้าไปสู่อนาคตที่นักคณิตศาสตร์จะใช้เครื่องมือ AI ร่วมกันเพื่อสำรวจสมมติฐาน ลองแนวทางใหม่กับปัญหาเก่า และทำส่วนที่ใช้เวลามากของการพิสูจน์ให้เสร็จได้รวดเร็วขึ้น
3 ความคิดเห็น
ยิ่งมีนักคณิตศาสตร์ที่ช่วยพัฒนาไลบรารีคณิตศาสตร์เชิงรูปนัยมากขึ้นเท่าไร ก็จะยิ่งสร้าง AI ด้านคณิตศาสตร์ที่มีประสิทธิภาพสูงได้ง่ายขึ้นเท่านั้น เท่าที่ผมทราบ ตอนนี้มีชาวเกาหลีอยู่ 3 คนที่กำลังย้ายทฤษฎีคณิตศาสตร์ซึ่งตนเองได้ทำให้เป็นเชิงรูปนัยโดยตรงด้วยภาษาของตัวช่วยพิสูจน์ Lean ไปยัง Mathlib ซึ่งเป็นไลบรารีคณิตศาสตร์ของ Lean
เมื่อปีที่แล้ว ผมมีส่วนร่วมอยู่บ้างในการย้าย Mathlib จาก Lean 3 ไปเป็น Lean 4 และในปีนี้ ผมได้พิสูจน์ทฤษฎีบทที่ยังไม่ถูกแก้อยู่อันหนึ่งในไลบรารี Batteries ของ Lean 4
ความคิดเห็นจาก Hacker News
ผมตื่นเต้นกับประกาศนี้มากจริง ๆ แต่ยังไม่ชัดเจนว่าประโยคที่ว่า “ก่อนอื่น มนุษย์แปลโจทย์ด้วยตนเองเป็น ภาษาคณิตศาสตร์เชิงรูปแบบ เพื่อให้ระบบเข้าใจได้” นั้นแบกรับงานไว้มากแค่ไหน
โจทย์ที่ไม่ใช่เรขาคณิตทั้งหมดอยู่ในรูป “จงหา X ทั้งหมดที่...” และข้อความทฤษฎีบทอยู่ในรูป “แสดงว่าเซตของ X ทั้งหมดคือ {foo}”
ดูจากเฉลยที่ดาวน์โหลดได้ที่ https://storage.googleapis.com/deepmind-media/DeepMind.com/B... อย่างเดียว จึงยากจะรู้ว่าในขั้นตอนการแปลนั้นมนุษย์เป็นคนกำหนด {foo} หรือคอมพิวเตอร์เป็นคนหา ผมอยากเชื่อว่าคอมพิวเตอร์หาเอง แต่ยังหาหลักฐานยืนยันไม่ได้
{1,1}, และใน P6 พบ2พร้อมนำเสนอ พิสูจน์ใน Lean ในแต่ละกรณีด้วยแม้แต่มนุษย์เวลาจัดการกับวิธีเชิงรูปแบบโดยตรง เรื่องแบบนี้ก็เกิดขึ้นบ่อย นักวิจัยจึงน่าจะตัดสินว่าไม่ว่าจะเป็น LLM หรือเครื่องมืออื่น สุดท้ายก็ต้องตรวจสอบการแปลทั้งหมดอยู่ดี
อย่างไรก็ตาม ยังไม่ชัดเจนว่าเอเจนต์ได้รับรูปแบบตั้งต้นแบบใด จึงทำขั้นตอนนี้ได้
กล่าวคือ ไม่ว่า AlphaProof จะรับ “โจทย์” ในรูปแบบใด และทำให้ “จงหา X ทั้งหมดที่...” เป็นรูปแบบอย่างไร มันก็น่าจะสร้างทฤษฎีบทตัวเลือกเป็น Lean ตัวอย่างเช่น เซตอาจอยู่ในรูป
{n: P(n)}สำหรับสูตร P บางอย่าง จากนั้นจึงค้นหาพิสูจน์ถ้า AlphaProof ไม่ได้หา {foo} เอง แต่เป็นสิ่งที่ให้มาอยู่แล้ว การอ้างว่ามันแก้โจทย์ได้ก็คงค่อนข้างไร้เหตุผล ถึงอย่างนั้น ผมก็ยังตื่นเต้นกับผลลัพธ์นี้มาก
น่าประทับใจแน่นอน แต่เวลาพูดถึง IMO ควรมีข้อควรระวัง เหรียญจะมอบให้ผู้เข้าแข่งขัน หรือก็คือนักเรียนมัธยม 50% และสัดส่วนทอง·เงิน·ทองแดงคือ 1:2:3 ดังนั้น ผู้ได้เหรียญทองและเงิน จะอยู่ในกลุ่มบนสุด 25% ของผู้เข้าแข่งขันทั้งหมด
ดังนั้นถ้อยคำก็คือ “AI แก้โจทย์ IMO ได้ดีกว่านักเรียน 75%” ซึ่งจริง ๆ แล้วอาจน่าประทับใจกว่าด้วยซ้ำ
แต่เงื่อนไข “หนึ่งข้อใช้เวลาไม่กี่นาที ส่วนข้ออื่น ๆ แต่ละข้อใช้ได้สูงสุด 3 วัน” แตกต่างจาก 9 ชั่วโมงที่นักเรียนได้รับ จึงยากจะถือว่าเป็นการเปรียบเทียบที่แท้จริง หากนักเรียนได้รับเวลาสูงสุด 15 วันแทน 9 ชั่วโมง ก็คงมีคนจำนวนมากขึ้นที่ทำคะแนนได้เท่าหรือเกินนี้
ในความเป็นจริง AI แก้ได้เพียงหนึ่งข้อภายในเวลา 9 ชั่วโมงที่นักเรียนได้รับ จึงมีความเป็นไปได้สูงว่ายังห่างไกลจากระดับได้เหรียญ ทำไมต้องทำให้ผลลัพธ์ที่น่าประทับใจแบบนี้มัวลงด้วยการ เปรียบเทียบแอปเปิลกับส้ม ด้วยก็ไม่รู้
รายงานอย่างเป็นกลางกว่านั้นได้ว่า แม้ใช้เวลามากกว่า แต่แก้ได้ X% ของโจทย์ทั้งหมด หรือได้ X คะแนนจากคะแนนเต็ม N
ในที่นี้ เวลา ไม่ใช่แกนที่น่าสนใจนัก เพราะมนุษย์ไม่ได้ใช้ CPU แบบเดียวกับคลัสเตอร์ GPU ขนาดยักษ์ ประเด็นแบบทวิภาค “เมื่อให้ทรัพยากรเพียงพอ จะไปถึงคำตอบได้หรือไม่” น่าสนใจกว่า และคำตอบของ GPT/Claude คือไม่อย่างชัดเจน
มันใกล้เส้นตัดมาก และโดยปกติแค่มีความคืบหน้าเล็กน้อยก็อาจได้ 1 คะแนนแล้ว อย่างไรก็ตาม ด้วยเหตุผลทางเทคนิค หากมีข่าวออกไปว่าคว้าเหรียญทองได้ก็คงไม่ดีนัก จึงดูเหมือนจะพอใจกับเหรียญเงินที่ไม่มีข้อโต้แย้ง
เรื่องนี้ของจริง AlphaGeometry เคยแก้โจทย์ชุดที่จำกัดมากได้ด้วยการค้นหาแบบ brute-force จำนวนมาก
วิธีครั้งนี้กว้างกว่ามาก และผมคิดว่าจะส่งผลใหญ่ต่อวิธีทำคณิตศาสตร์ มันเชื่อมจากคณิตศาสตร์ภาษาธรรมชาติไปสู่ คณิตศาสตร์ที่ถูกทำให้เป็นรูปแบบทางการ และจากตรงนั้นก็กำลังทำให้ไปป์ไลน์แบบ self-supply ที่ฝึกได้ทั้งการทำให้เป็นรูปแบบทางการและการพิสูจน์เกิดขึ้นจริง
โดยหลักการแล้ว ไปป์ไลน์นี้ยังสามารถเรียนรู้การสร้างทฤษฎีพื้นฐาน เช่น การสร้างนิยามเสริมและบทตั้งเสริมได้ด้วย มันใกล้เคียงจอกศักดิ์สิทธิ์ของ proof assistant และผมคิดว่ามันจะช่วยทำให้คณิตศาสตร์ส่วนใหญ่ที่เราสร้างขึ้นตามธรรมชาติกลายเป็นรูปแบบทางการได้ มนุษย์จะทำงานในแบบทำให้เข้มงวดภายหลัง และเครื่องจะเข้ามาช่วยเติมรายละเอียด
ในทางกลับกัน การทำให้เป็นรูปแบบทางการแบบปลายเปิดเช่นนี้เป็นพื้นที่ที่ความก้าวหน้าช้ามากและค่อยเป็นค่อยไป ผมเคยทำงานในสาขาใกล้เคียงเมื่อ 5 ปีก่อน และผลลัพธ์นี้ถือได้ว่าอยู่ในระดับที่เทคนิค automated reasoning แบบดั้งเดิมไปไม่ถึง
การพิสูจน์ทฤษฎีบทอัตโนมัติของจริงมีประโยชน์กว้างไกลกว่าคณิตศาสตร์บริสุทธิ์มาก เช่น เราอาจเขียน axiomatic semantics ของภาษาโปรแกรมขนาดเล็กใน Lean แล้วถามว่า “จงแสดงว่ามีโปรแกรมที่ทำตามสเปกนี้อยู่จริง”
ถ้าแนวทางนี้ขยายต่อได้ มันจะสำคัญกว่าการ ประยุกต์ใช้แมชชีนเลิร์นนิง ใด ๆ ที่ออกมาในช่วงไม่กี่ปีที่ผ่านมา
วิวัฒนาการที่สร้างเราขึ้นมาก็เป็น การค้นหา ที่ทำงานด้วยการลองแบบ brute-force อย่างมหาศาล และการวิจัยด้วยวิธีวิทยาศาสตร์ก็โดยแก่นแล้วคือการค้นหา
https://leandojo.org/
https://machine-learning-for-theorem-proving.github.io/
https://www.youtube.com/watch?v=P5ew0BrRm_I
https://paperswithcode.com/task/automated-theorem-proving
https://old.reddit.com/r/math/comments/11mb9lx/future_of_aut...
https://github.com/RiccardoBiosas/LeanGPT
เพื่อให้ทำงานที่มีประโยชน์ได้ ไม่จำเป็นต้องพิสูจน์โจทย์ที่ยากมากเสมอไป บ่อยครั้งแค่พิสูจน์เรื่องง่าย ๆ ก็พอแล้ว ถ้าให้โมเดลภาษาทำงานให้เสร็จ จัดระเบียบรายการ ประสานตารางเวลา เขียนโค้ดที่ทำ X ฯลฯ ผลลัพธ์มักเชื่อถือได้ยากทันที แต่ถ้าระบบสามารถ แปลบางส่วนของปัญหาเป็นตรรกะ และหาคำตอบได้ ก็จะเชื่อถือได้มากขึ้นมาก
ประเด็นสำคัญถูกกลบไปหน่อย คือพวกเขาใช้ Lean อยู่
เรื่องนี้สำคัญเกินกว่าโจทย์คณิตศาสตร์ การให้โมเดลแมชชีนเลิร์นนิงไปต่อสู้กับระบบพิสูจน์เป็นวิธีที่ดีในการหลีกเลี่ยงการพูดมั่ว ๆ ทั่วไป
หวังว่าต่อไปจะมีคนจำนวนมากขึ้นเขียน type ใน Lean หรือระบบคล้ายกัน เพื่อใช้เป็นวิธีที่ดีกว่ามากในการเขียนพรอมป์ต์
polyrithแค่พิมพ์แปดตัวอักษรก็พอ ผมยังเห็น AlphaProof ใช้nlinarithด้วยTim Gowers มีภาพรวมสั้น ๆ ที่ดี ซึ่งอธิบายข้อควรระวังหลักและให้บริบท เขาเป็นผู้ได้รับเหรียญ Fields และมีส่วนร่วมในงานครั้งนี้ด้วย: https://x.com/wtgowers/status/1816509803407040909
พูดถูกก็จริง แต่การติดทีมชาติของแต่ละประเทศนั้นเป็นกระบวนการที่โหดมากอยู่แล้ว ทุกขั้นถูกคัดออกอย่างโหด ตั้งแต่โอลิมปิกคณิตศาสตร์ระดับท้องถิ่น โอลิมปิกคณิตศาสตร์ระดับประเทศ ฯลฯ
หลังจากนั้นยังมีการฝึกเพิ่มเติมสำหรับกลุ่มหัวกะทินี้ และในบางกรณีอาจมีการคัดเลือกเพิ่มเติมด้วย
สรุปคือการถูกเลือกเข้า ทีม IMO ของประเทศหนึ่ง ๆ เป็นเรื่องใหญ่อยู่แล้ว และการได้เหรียญทองหรือเหรียญเงินในกลุ่มนั้นก็เป็นความสำเร็จที่มหาศาลจริง ๆ
แหล่งข่าวคือเพื่อนที่ได้เหรียญเงิน IMO
อิจฉาคนที่ได้รับเงินเพื่อทำงานแบบนี้จริง ๆ ดูน่าสนุกมาก และการผลักดัน ระดับแนวหน้าสุด แบบนี้ก็น่าจะให้ความรู้สึกอิ่มเอมใจมาก
ในเรื่องความพึงพอใจในการทำงาน ผมมองว่า สภาพแวดล้อมการทำงาน สำคัญกว่าหัวข้อที่ทำ ต่อให้ทำเรื่องที่จะเปลี่ยนโลก แต่ถ้าทีมเละเทะ คุณก็จะต้องเจอกับช่วงเวลาที่ยากลำบาก บางคนมีพรสวรรค์ในการดูดความสนุกออกไปจนหมด การเมืองในองค์กรมีอยู่ทุกที่ และยิ่งเป็นหัวข้อที่เปลี่ยนโลกก็ยิ่งเป็นแบบนั้น
ในทางกลับกัน แม้จะเป็นหัวข้อที่ดูน่าเบื่อที่สุดอย่างการเอาข้อมูลลูกค้าใส่ลงในฐานข้อมูล ถ้ามีทีมที่เป็นมิตร สถาปัตยกรรมที่ออกแบบมาดี และมีเวลาสำหรับการทดลองกับการแบ่งปันความรู้ คุณก็อาจมีช่วงเวลาที่ยอดเยี่ยมได้ ผมยิ่งให้คุณค่ากับความงามของสิ่งเรียบง่ายที่ทำงานได้ดีมากขึ้นเรื่อย ๆ สิ่งแบบนั้นอาจหายากยิ่งกว่าการค้นพบทางวิทยาศาสตร์เสียอีก
แน่นอนว่าสภาพแวดล้อมการทำงานที่ยอดเยี่ยมอาจมาพร้อมกับหัวข้อที่ยอดเยี่ยมได้ และนั่นก็ใกล้เคียงกับการถูกแจ็กพอต จึงน่าอิจฉาอยู่
ควรจะตื่นเต้นและรู้สึกขอบคุณที่ได้ทำงานแบบนี้ แต่เครื่องมือหยาบ ๆ หลายอย่างก็พรากความสนุกจากงานไปเยอะ
(/s)
เครื่องจักรเล่นหมากรุกเก่งกว่ามนุษย์มาหลายสิบปีแล้ว
แต่ก็ไม่มีใครสนใจ ทุกคนยุ่งอยู่กับการดู Magnus Carlsen
เพราะเราเป็นมนุษย์ เราจึงสนใจสิ่งที่มนุษย์คนอื่นทำ ส่วนเครื่องจักร เราสนใจเท่าที่มันเป็นประโยชน์ต่อเราเท่านั้น
หลักการนี้ขยายไปถึงงานและศิลปะได้อย่างกว้างขวาง ตราบใดที่มนุษย์ยังมีอยู่ พื้นที่ของมนุษย์ ในด้านเหล่านี้ก็จะยังคงมีเสมอ
แต่ผมสงสัยมากว่าในอนาคตอันใกล้ จะยังมีนักคณิตศาสตร์ที่ประกาศ ความก้าวหน้าทางคณิตศาสตร์ใหม่ ๆ ที่ AI ไม่ได้ค้นพบเป็นส่วนใหญ่หรือทั้งหมด เหลืออยู่หรือไม่ มนุษย์อาจได้รับเครดิตในการพิสูจน์เพราะเป็นคนตั้งคำถามแรกก็ได้ แต่แทบไม่มีโลกไหนที่จะยืนกรานให้มนุษย์แก้ปัญหาช้ากว่าและแพงกว่า ทั้งที่คอมพิวเตอร์สามารถแก้ปัญหาคณิตศาสตร์ที่มีความหมายได้อย่างง่ายดาย
หลักการนี้ใช้ได้กับศิลปะอย่างแน่นอน แต่กับงาน ใช้ได้แค่บางส่วนหรือส่วนใหญ่เท่านั้น
ดังนั้นจึงไม่จำเป็นต้องเข้าใจการพิสูจน์ และไม่มีใครสนใจว่านักคณิตศาสตร์ที่ไหนสักแห่งเข้าใจการพิสูจน์นั้นอย่างสมบูรณ์หรือไม่ การที่เครื่องจักรค้นหาและตรวจสอบการพิสูจน์ได้ดีกว่าเรานั้นไม่เป็นไร และกลับเป็นสิ่งที่คาดหมายได้ด้วยซ้ำ
นักคณิตศาสตร์จำนวนมากคงไม่อยากทุ่มเทกับงานแบบนั้น อย่างไรก็ตาม ระหว่าง IMO กับ แนวหน้าของคณิตศาสตร์เชิงวิจัย ก็ยังมีระยะห่างมากอยู่
การพิสูจน์ทฤษฎีบทเป็นเกมผู้เล่นคนเดียวที่มีพื้นที่ค้นหาใหญ่โตอย่างไร้สาระ ผมจึงคิดมาตลอดว่ามันจะถูกแก้ได้ก่อน AGI นานมาก
โดยส่วนตัว ผมมองว่าผู้มีส่วนสำคัญที่สุดของ AlphaProof คือคนที่อยู่เบื้องหลัง Lean และ Mathlib เพราะพวกเขารับภารกิจอันน่าหวั่นใจในการทำให้คณิตศาสตร์ทั้งหมดเป็นรูปแบบเชิงพิธีการ
การขาดการทำให้เป็นรูปแบบเชิงพิธีการ ของบทความคณิตศาสตร์เป็นสิ่งที่ฆ่าความพยายามในการทำอัตโนมัติมาโดยตลอด เพราะนักวิจัย AI ต้องต่อสู้กับองค์ประกอบแบบมนุษย์ เช่น สัญกรณ์เฉพาะของผู้เขียน ความรู้โดยนัย และขั้นตอนการพิสูจน์ที่ถูกละไว้
ผมมองว่าคำว่า AGI เองก็ยังไม่มีนิยาม แต่ไม่เข้าใจว่าทำไมถึงคาดว่า การสร้าง “บางสิ่งที่มีสติปัญญาทั่วไป” หรือสติปัญญาระดับค่ากลางของมนุษย์ จะยากกว่าการ “เก่งคณิตศาสตร์กว่า Terrence Tao” มากมายขนาดนั้น
การอภิปรายที่ดีที่สุดอยู่ที่นี่: https://leanprover.zulipchat.com/#narrow/stream/219941-Machi...
การอภิปรายที่ดีที่สุดนั้นดูได้ที่นี่ https://leanprover.zulipchat.com/#narrow/stream/219941-Machine-Learnin…