AI ที่การแข่งขันคณิตศาสตร์โอลิมปิกระหว่างประเทศ: วิธีที่ AlphaProof และ AlphaGeometry 2 ได้รับมาตรฐานเหรียญเงิน

การให้เหตุผลทางคณิตศาสตร์เป็นลักษณะสำคัญของความสามารถในการรับรู้ของมนุษย์ ซึ่งขับเคลื่อนความก้าวหน้าในการค้นพบทางวิทยาศาสตร์และการพัฒนาทางเทคโนโลยี ในขณะที่เราพยายามพัฒนาความฉลาดเทียมที่มีความสามารถเทียบเท่ากับการรับรู้ของมนุษย์ การให้ความสามารถในการให้เหตุผลทางคณิตศาสตร์ที่ทันสมัยแก่ AI เป็นสิ่งจำเป็น ในขณะที่ระบบ AI ปัจจุบันสามารถจัดการปัญหาคณิตศาสตร์ขั้นพื้นฐานได้ แต่พวกเขาก็ยังคงดิ้นรนในการให้เหตุผลที่ซับซ้อนซึ่งจำเป็นสำหรับสาขาคณิตศาสตร์ที่ซับซ้อน เช่น แคลคูลัสและเรขาคณิต อย่างไรก็ตาม สิ่งนี้อาจเปลี่ยนแปลงไป เนื่องจาก Google DeepMind ได้ทำการก้าวหน้าอย่างมีนัยสำคัญในการพัฒนาความสามารถในการให้เหตุผลทางคณิตศาสตร์ของระบบ AI ซึ่งได้รับการพัฒนาในการแข่งขันคณิตศาสตร์โอลิมปิกระหว่างประเทศ (IMO) 2024 ซึ่งจัดตั้งขึ้นในปี 1959 เป็นการแข่งขันคณิตศาสตร์ที่เก่าแก่ที่สุดและเป็นที่น่าเชื่อถือที่สุด โดยที่นักเรียนมัธยมศึกษาทั่วโลกได้รับการท้าทายด้วยปัญหาในด้านแคลคูลัส คอมบินาโทริกส์ เรขาคณิต และทฤษฎีจำนวน ในแต่ละปี ทีมนักเรียนคณิตศาสตร์แข่งขันกันเพื่อแก้ปัญหา 6 ข้อที่ท้าทายมาก ในปีนี้ Google DeepMind ได้นำระบบ AI สองระบบมาใช้: AlphaProof ซึ่งมุ่งเน้นไปที่การให้เหตุผลทางคณิตศาสตร์อย่างเป็นทางการ และ AlphaGeometry 2 ซึ่งมีความเชี่ยวชาญในการแก้ปัญหาเรขาคณิต ระบบ AI เหล่านี้สามารถแก้ปัญหา 4 ใน 6 ข้อได้ โดยแสดงผลงานที่ระดับเหรียญเงิน ในบทความนี้ เราจะสำรวจว่าระบบเหล่านี้ทำงานอย่างไรในการแก้ปัญหาและวิธีการที่พวกเขาสามารถพัฒนาความสามารถในการให้เหตุผลทางคณิตศาสตร์ได้

AlphaProof: การรวม AI และภาษาแบบฟอร์มอลสำหรับการพิสูจน์ทฤษฎีทางคณิตศาสตร์

AlphaProof เป็นระบบ AI ที่ออกแบบมาเพื่อพิสูจน์ข้อความทางคณิตศาสตร์โดยใช้ภาษาแบบฟอร์มอล Lean มันรวม Gemini ซึ่งเป็นแบบจำลองภาษาที่ได้รับการฝึกอบรมล่วงหน้าเข้ากับ AlphaZero ซึ่งเป็นอัลกอริทึมการเรียนรู้แบบเสริมที่มีชื่อเสียงในการเล่นหมากรุก สโงกิ และโก

แบบจำลอง Gemini แปลข้อความปัญหาจากภาษาธรรมชาติเป็นภาษาแบบฟอร์มอล โดยสร้างห้องสมุดปัญหาในระดับความยากต่างๆ สิ่งนี้มีจุดประสงค์สองประการ: การแปลงภาษาธรรมชาติที่ไม่ชัดเจนเป็นภาษาแบบฟอร์มอลที่แม่นยำสำหรับการยืนยันพิสูจน์ทางคณิตศาสตร์ และการใช้ความสามารถในการคาดเดาของ Gemini เพื่อสร้างรายการคำตอบที่เป็นไปได้ด้วยความแม่นยำของภาษาแบบฟอร์มอล

เมื่อ AlphaProof พบปัญหา มันจะสร้างคำตอบที่เป็นไปได้และค้นหาขั้นตอนพิสูจน์ใน Lean เพื่อยืนยันหรือพิสูจน์คำตอบเหล่านั้น สิ่งนี้เป็นแนวทางแบบ neuro-symbolic โดยที่เครือข่ายประสาทเทียม Gemini แปลคำสั่งภาษาธรรมชาติเป็นภาษาแบบฟอร์มอล Lean เพื่อพิสูจน์หรือพิสูจน์ข้อความนั้น ในทำนองเดียวกับการเล่นแบบ self-play ของ AlphaZero ซึ่งระบบเรียนรู้โดยการเล่นกับตัวเอง AlphaProof ฝึกอบรมตัวเองโดยพยายามพิสูจน์ข้อความทางคณิตศาสตร์ การพิสูจน์ที่สำเร็จจะทำให้ AlphaProof พัฒนารูปแบบภาษาของมัน โดยการพิสูจน์ที่สำเร็จจะเสริมสร้างความสามารถของมันในการแก้ปัญหาที่ท้าทายมากขึ้น

สำหรับการแข่งขันคณิตศาสตร์โอลิมปิกระหว่างประเทศ (IMO) AlphaProof ได้รับการฝึกอบรมโดยการพิสูจน์หรือพิสูจน์ปัญหาหลายล้านข้อในระดับความยากและหัวข้อคณิตศาสตร์ต่างๆ การฝึกอบรมนี้ดำเนินต่อไปในช่วงการแข่งขัน โดยที่ AlphaProof พัฒนาวิธีแก้ปัญหาอย่างต่อเนื่องจนกว่าจะพบคำตอบที่สมบูรณ์สำหรับปัญหา

AlphaGeometry 2: การบูรณาการ LLMs และ AI แบบสัญลักษณ์สำหรับการแก้ปัญหาเรขาคณิต

AlphaGeometry 2 เป็นรุ่นล่าสุดของซีรีส์ AlphaGeometry ซึ่งได้รับการออกแบบมาเพื่อแก้ปัญหาเรขาคณิตด้วยความแม่นยำและประสิทธิภาพที่ดีขึ้น โดยสร้างบนพื้นฐานของตัวก่อนหน้า AlphaGeometry 2 ใช้แนวทางแบบ neuro-symbolic ที่รวม LLMs (แบบจำลองภาษาขนาดใหญ่) เข้ากับ AI แบบสัญลักษณ์ การบูรณาการนี้รวมตรรกะแบบกฎเข้ากับความสามารถในการคาดเดาของเครือข่ายประสาทเทียมเพื่อระบุจุดช่วยเหลือที่จำเป็นสำหรับการแก้ปัญหาเรขาคณิต LLM ใน AlphaGeometry คาดเดาโครงสร้างทางเรขาคณิตใหม่ ในขณะที่ AI แบบสัญลักษณ์ใช้ตรรกะแบบฟอร์มอลเพื่อสร้างพิสูจน์

เมื่อเผชิญกับปัญหาเรขาคณิต AlphaGeometry’s LLM จะประเมินความเป็นไปได้หลายอย่าง โดยคาดเดาโครงสร้างที่สำคัญสำหรับการแก้ปัญหา การคาดเดาเหล่านี้ทำหน้าที่เป็นคำใบ้ที่มีคุณค่า โดยชี้นำเครื่องยนต์แบบสัญลักษณ์ไปสู่การอนุมานที่แม่นยำและก้าวหน้าไปสู่คำตอบ

หนึ่งในคุณสมบัติที่ได้รับการปรับปรุงใน AlphaGeometry 2 คือการบูรณาการของ LLM Gemini ซึ่งได้รับการฝึกอบรมจากข้อมูลสังเคราะห์ที่สำคัญมากกว่ารุ่นก่อนหน้า การฝึกอบรมนี้ทำให้สามารถจัดการปัญหาเรขาคณิตที่ยากขึ้น รวมถึงปัญหาที่เกี่ยวข้องกับการเคลื่อนไหวของวัตถุและสมการของมุม อัตราส่วน หรือระยะทาง นอกจากนี้ AlphaGeometry 2 ยังมีเครื่องยนต์แบบสัญลักษณ์ที่ทำงานเร็วขึ้นสองอันดับ ทำให้สามารถสำรวจวิธีแก้ปัญหาทางเลือกด้วยความเร็วที่ไม่เคยเห็นมาก่อน ความก้าวหน้าเหล่านี้ทำให้ AlphaGeometry 2 เป็นเครื่องมือที่ทรงพลังสำหรับการแก้ปัญหาเรขาคณิตที่ซับซ้อน โดยตั้งมาตรฐานใหม่ในด้านนี้

AlphaProof และ AlphaGeometry 2 ที่ IMO

ในปีนี้ในการแข่งขันคณิตศาสตร์โอลิมปิกระหว่างประเทศ ผู้เข้าแข่งขันได้รับการทดสอบด้วยปัญหา 6 ข้อที่หลากหลาย: 2 ข้อในด้านแคลคูลัส 1 ข้อในด้านทฤษฎีจำนวน 1 ข้อในด้านเรขาคณิต และ 2 ข้อในด้านคณิตศาสตร์ผสม นักวิจัยของ Google ได้แปลปัญหาเหล่านี้เป็นภาษาคณิตศาสตร์แบบฟอร์มอลสำหรับ AlphaProof และ AlphaGeometry 2 AlphaProof ได้แก้ปัญหา 2 ข้อในด้านแคลคูลัสและ 1 ข้อในด้านทฤษฎีจำนวน รวมถึงปัญหาที่ยากที่สุดในการแข่งขันซึ่งได้รับการแก้โดยนักเรียนคณิตศาสตร์ 5 คนในปีนี้ ในขณะที่ AlphaGeometry 2 ได้แก้ปัญหาเรขาคณิตสำเร็จ แต่ไม่สามารถแก้ปัญหา 2 ข้อในด้านคณิตศาสตร์ผสมได้
แต่ละปัญหาในการแข่งขันคณิตศาสตร์โอลิมปิกระหว่างประเทศมีค่า 7 คะแนน โดยมีคะแนนสูงสุด 42 คะแนน AlphaProof และ AlphaGeometry 2 ได้รับคะแนน 28 คะแนน โดยได้คะแนนสมบูรณ์ในการแก้ปัญหาเหล่านั้น สิ่งนี้ทำให้พวกเขาอยู่ในระดับสูงของหมวดเหรียญเงิน คะแนนสำหรับเหรียญทองในปีนี้คือ 29 คะแนน ซึ่งถึงโดยผู้เข้าแข่งขัน 58 คนจากทั้งหมด 609 คน

การก้าวหน้าถัดไป: ภาษาธรรมชาติสำหรับการท้าทายคณิตศาสตร์

AlphaProof และ AlphaGeometry 2 ได้แสดงให้เห็นถึงความก้าวหน้าที่น่าประทับใจในการแก้ปัญหาและให้เหตุผลทางคณิตศาสตร์ของ AI อย่างไรก็ตาม ระบบเหล่านี้ยังคงต้องการผู้เชี่ยวชาญด้านคณิตศาสตร์ในการแปลปัญหาเป็นภาษาแบบฟอร์มอลสำหรับการประมวลผล นอกจากนี้ ยังไม่ชัดเจนว่าความสามารถทางคณิตศาสตร์ที่เฉพาะเจาะจงเหล่านี้จะถูกบูรณาการเข้ากับระบบ AI อื่นๆ เช่น การสำรวจสมมติฐาน การทดสอบวิธีแก้ปัญหาใหม่ๆ สำหรับปัญหาที่ยังไม่ได้รับการแก้ไข และการจัดการด้านเวลาในการพิสูจน์อย่างมีประสิทธิภาพ
เพื่อ 克服ข้อจำกัดเหล่านี้ นักวิจัยของ Google กำลังพัฒนาระบบการให้เหตุผลภาษาธรรมชาติซึ่งพัฒนาต่อจาก Gemini และการวิจัยล่าสุด ระบบใหม่นี้มีเป้าหมายที่จะพัฒนาความสามารถในการแก้ปัญหาโดยไม่ต้องการการแปลภาษาแบบฟอร์มอล และได้รับการออกแบบให้บูรณาการเข้ากับระบบ AI อื่นๆ ได้อย่างราบรื่น

สรุป

การแสดงผลของ AlphaProof และ AlphaGeometry 2 ในการแข่งขันคณิตศาสตร์โอลิมปิกระหว่างประเทศเป็นการก้าวหน้าอย่างมีนัยสำคัญในการแก้ปัญหาและให้เหตุผลทางคณิตศาสตร์ของ AI ทั้งสองระบบแสดงให้เห็นถึงความสามารถในการแก้ปัญหา 4 ใน 6 ข้อที่ท้าทาย โดยแสดงให้เห็นถึงความก้าวหน้าที่สำคัญในการพิสูจน์แบบฟอร์มอลและแก้ปัญหาเรขาคณิต แม้ว่าพวกเขาจะบรรลุความสำเร็จ แต่ระบบ AI เหล่านี้ยังคงต้องการการแปลปัญหาเป็นภาษาแบบฟอร์มอลและเผชิญกับความท้าทายในการบูรณาการเข้ากับระบบ AI อื่นๆ การวิจัยในอนาคตมีเป้าหมายที่จะพัฒนาระบบเหล่านี้เพิ่มเติม โดยอาจรวมถึงการบูรณาการการให้เหตุผลภาษาธรรมชาติเพื่อขยายความสามารถของพวกเขาในการแก้ปัญหาที่ท้าทายทางคณิตศาสตร์อย่างกว้างขวาง