AlphaProof Nexus: AI ของ DeepMind ไขโจทย์ Erdős 56 ปี
Google DeepMind เปิดตัว AlphaProof Nexus เฟรมเวิร์กจับคู่ Gemini 3.1 Pro กับภาษา Lean แก้โจทย์คณิตศาสตร์ Erdős อายุ 56 ปีสำเร็จด้วยต้นทุนต่ำ
ภาพประกอบจากคลังภาพสต็อก ไม่ใช่ภาพจากเหตุการณ์จริง
- DeepMind เปิดตัว AlphaProof Nexus จับคู่ Gemini 3.1 Pro กับภาษา Lean
- ไขโจทย์คณิตศาสตร์ Erdős อายุ 56 ปีสำเร็จ 2 ข้อจากทั้งหมด 9 ข้อที่แก้ได้
- ทุกบทพิสูจน์ผ่านการตรวจสอบตรรกะด้วยคอมไพเลอร์โดยไม่ต้องพึ่งความเชื่อใจ
- ใช้ต้นทุนประมวลผลเพียงไม่กี่ร้อยดอลลาร์ต่อโจทย์หรือราว 60 ดอลลาร์ต่อ TPU
ปัญหาคณิตศาสตร์ที่นักคณิตศาสตร์ชาวฮังการี Paul Erdős ทิ้งไว้และรอคอยคำตอบมานานถึง 56 ปี ถูกปิดลงได้ด้วยระบบปัญญาประดิษฐ์ที่ใช้ค่าประมวลผลเพียงหลักร้อยดอลลาร์ต่อโจทย์ จุดสำคัญของความสำเร็จนี้ไม่ใช่แค่ตัวคำตอบ แต่ทุกขั้นตอนของบทพิสูจน์ได้รับการตรวจสอบความถูกต้องผ่านเครื่องคอมพิวเตอร์เรียบร้อยแล้ว ตัดความกังวลเรื่องการกุข้อมูลของ AI ออกไปได้อย่างสิ้นเชิง
Google DeepMind เผยแพร่งานวิจัยในหัวข้อ Advancing Mathematics Research with AI-Driven Formal Proof Search บนแพลตฟอร์ม arXiv เพื่อแนะนำ AlphaProof Nexus เฟรมเวิร์กที่ผสานการทำงานระหว่างโมเดลภาษาขนาดใหญ่ Gemini 3.1 Pro และภาษา Lean สำหรับเขียนบทพิสูจน์คณิตศาสตร์ที่คอมพิวเตอร์ตรวจสอบตรรกะได้ ผลลัพธ์คือระบบสามารถแก้โจทย์ Erdős ที่ยังเปิดอยู่ได้ 9 จาก 353 ข้อ พิสูจน์ข้อความคาดการณ์จากฐานข้อมูล Online Encyclopedia of Integer Sequences (OEIS) ได้ 44 จาก 492 ข้อ พร้อมทั้งปิดคำถามสาขาเรขาคณิตเชิงพีชคณิตที่ค้างมานานกว่า 15 ปี
อุปสรรคสำคัญในการใช้โมเดลภาษาทำงานวิจัยคณิตศาสตร์คือความน่าเชื่อถือ เนื่องจากบทพิสูจน์ในภาษาธรรมชาติมักมีจุดผิดพลาดเล็กๆ ซ่อนอยู่ ทีม DeepMind จึงแก้ไขด้วยการบังคับให้ AI เขียนบทพิสูจน์แบบเป็นทางการในภาษา Lean เสมือนการเขียนโค้ดโปรแกรม เพื่อให้คอมไพเลอร์ตรวจตรรกะทีละบรรทัด หากพบข้อผิดพลาด ระบบจะนำข้อความแจ้งเตือนป้อนกลับให้ AI แก้ไขในรอบถัดไปทันที
ภาพประกอบจากคลังภาพสต็อก ไม่ใช่ภาพจากเหตุการณ์จริง
กระบวนการทำงานของ AlphaProof Nexus เริ่มต้นจากการป้อนโครงบทพิสูจน์ในภาษา Lean ที่เว้นว่างไว้ให้นักวิจัย จากนั้นให้ AI Agent เติมช่องว่างเหล่านั้นจนครบ โดยมีการทดลองโครงสร้าง Agent ทั้งหมด 4 รูปแบบ ตั้งแต่แบบพื้นฐานที่รัน Gemini 3.1 Pro หลายตัวแยกอิสระ แบบที่สองที่ผสานระบบ AlphaProof ที่ผ่านการฝึกด้วย Reinforcement Learning แบบที่สามที่เพิ่มกลไกวิวัฒนาการจัดอันดับด้วยระบบ Elo และแบบสุดท้ายคือ Agent ครบเครื่องที่รวมทุกกลไกเข้าไว้ด้วยกันซึ่งถูกนำมาใช้ลุยโจทย์ปลายเปิดจริง
"จากระบบเฉพาะทางที่ต้องฝึกพิเศษ ไปสู่วงจร Agent ที่เรียบง่าย"
ทีมวิจัย Google DeepMind
การนำภาษา Lean มาใช้ร่วมกับ LLM ถือเป็นหมุดหมายสำคัญที่เปลี่ยนผ่านจากการให้ AI แค่คาดเดาคำตอบ มาเป็นการตรวจสอบตรรกะเชิงสัญญะอย่างเข้มงวด การที่คอมไพเลอร์สามารถชี้จุดผิดพลาดและส่งฟีดแบ็กกลับไปยัง AI ได้โดยตรง ช่วยแก้จุดอ่อนเรื่องการกุข้อมูลหรือ Halucination ที่มักพบในโมเดลภาษาทั่วไป ทำให้วงการวิจัยคณิตศาสตร์สามารถเชื่อมั่นในผลลัพธ์ระดับทฤษฎีได้มากขึ้น
ชุดโจทย์ Erdős ที่นำมาทดสอบมาจากคลังข้อความคาดการณ์บนเว็บไซต์ ErdosProblems.com โดยโจทย์หมายเลข 125 ซึ่งเปิดค้างไว้ตั้งแต่ปี 1996 เกี่ยวข้องกับผลบวกของเซตจำนวนฐานสามและฐานสี่ ถูกระบบพิสูจน์ได้ว่าไม่สามารถกินพื้นที่ในเส้นจำนวนมากกว่าศูนย์ได้ ด้านต้นทุนการประมวลผลใช้เวลาบนชิป TPU ประมาณ 27.5 ชั่วโมงต่อโจทย์ หรือคิดเป็นมูลค่าราว 60 ดอลลาร์สหรัฐเท่านั้น
ที่มา: Techsauce
พบข้อมูลผิดพลาดในบทความนี้? แจ้งปัญหาบทความนี้
ความคิดเห็น
แสดงความคิดเห็น