- โมเดล Gemini Deep Think ของ Google DeepMind ทำได้ถึง คะแนนเกณฑ์เหรียญทอง (35 คะแนน) ในการแข่งขัน คณิตศาสตร์โอลิมปิกระหว่างประเทศ (IMO) ปี 2025
- โมเดลนี้ แก้โจทย์ได้สมบูรณ์ 5 ข้อจาก 6 ข้อ และได้รับการยอมรับจากการประเมินของคณะกรรมการตัดสินอย่างเป็นทางการของ IMO ว่าเป็น วิธีทำทางคณิตศาสตร์ที่ชัดเจนและแม่นยำ
- นับเป็น การก้าวกระโดดครั้งใหญ่ จากระดับเหรียญเงินของ AlphaProof·AlphaGeometry 2 เมื่อปีที่แล้ว (28 คะแนน) โดยสามารถเข้าใจโจทย์อย่างเป็นทางการในภาษาธรรมชาติ และเขียนบทพิสูจน์จนเสร็จได้เหมือนมนุษย์ภายใน 4.5 ชั่วโมง
- โหมด Deep Think ใช้ parallel thinking และ reinforcement learning ล่าสุด เพื่อสำรวจและสังเคราะห์แนวทางแก้หลายแบบพร้อมกัน ทำให้เหมาะกับการแก้โจทย์สไตล์ IMO เป็นพิเศษ
- Google มีแผนจะ ขยายความร่วมมือกับนักคณิตศาสตร์ ต่อไป และมุ่งสู่การพัฒนา AGI รุ่นถัดไป ที่ผสานการให้เหตุผลทางคณิตศาสตร์เข้ากับความสามารถในการตรวจสอบอย่างเป็นทางการ
Breakthrough Performance at IMO 2025 with Gemini Deep Think
- Gemini Deep Think ของ Google DeepMind ได้ 35 คะแนนรวม (แก้ได้สมบูรณ์ 5 ข้อจาก 6 ข้อ) ในการแข่งขันคณิตศาสตร์โอลิมปิกระหว่างประเทศ (IMO) ปี 2025 ทำให้บรรลุเกณฑ์เหรียญทองอย่างเป็นทางการ
- คณะกรรมการตัดสินอย่างเป็นทางการของ IMO ให้คะแนนสูงในด้าน ความชัดเจน ความแม่นยำ และวิธีอธิบายที่เข้าใจง่าย และประธาน IMO Prof. Dr. Gregor Dolinar ได้ออกแถลงการณ์อย่างเป็นทางการว่า "ขอยืนยันว่า Google DeepMind ทำคะแนนเหรียญทองที่ 35 คะแนนได้สำเร็จ"
- เมื่อปีที่แล้ว AlphaGeometry·AlphaProof ยังต้องอาศัยผู้เชี่ยวชาญแปลโจทย์จากภาษาธรรมชาติไปเป็นภาษาเฉพาะโดเมน (เช่น Lean) และยังใช้เวลาคำนวณมากกว่าสองวัน แต่ในปีนี้ Gemini สามารถ ทำครบทั้งกระบวนการตั้งแต่ทำความเข้าใจโจทย์ไปจนถึงเขียนบทพิสูจน์ในภาษาธรรมชาติ ภายในเวลาการแข่งขัน IMO (4.5 ชั่วโมง)
Making the most of Deep Think mode
- Gemini Deep Think เป็น โหมดการให้เหตุผลที่พัฒนาให้ดีขึ้น โดยนำเทคนิควิจัยล่าสุดอย่าง parallel thinking มาใช้ เพื่อสำรวจเส้นทางการแก้ปัญหาหลายแบบพร้อมกันและหาคำตอบที่เหมาะสมที่สุด
- โมเดลนี้ได้รับการฝึกด้วย เทคนิค reinforcement learning เพื่อแก้ปัญหาคณิตศาสตร์ที่ซับซ้อน รวมถึงข้อมูลบทพิสูจน์สไตล์ IMO ที่หลากหลาย และยังมีการป้อนคำแนะนำและเคล็ดลับทั่วไปเกี่ยวกับการเข้าหาโจทย์ IMO เพิ่มเติมด้วย
- โมเดล Deep Think นี้มีแผนจะ เปิดให้ใช้งานเวอร์ชันทดสอบก่อน สำหรับนักคณิตศาสตร์และผู้เชี่ยวชาญบางส่วนที่เชื่อถือได้ และภายหลังจะเปิดให้ผู้สมัครสมาชิก Google AI Ultra ใช้งาน
The Future of AI and Mathematics
- Google DeepMind ยังคง เดินหน้าความร่วมมือกับชุมชนคณิตศาสตร์ ต่อไป พร้อมกับทำวิจัยบน ระบบทางการแบบ formal เช่น AlphaGeometry·AlphaProof ควบคู่ไปกับการให้เหตุผลบนภาษาธรรมชาติ
- ต่อจากนี้ AI ที่ผสานความสามารถในการเข้าใจภาษาธรรมชาติเข้ากับ ความสามารถในการให้เหตุผลทางคณิตศาสตร์แบบเป็นทางการและตรวจสอบได้ มีแนวโน้มจะกลายเป็น เครื่องมือสำคัญ ในงานคณิตศาสตร์ วิทยาศาสตร์ วิศวกรรม และการวิจัย
- DeepMind ประเมินว่าความสำเร็จครั้งนี้เป็น ความก้าวหน้าสำคัญบนเส้นทางสู่ AGI (ปัญญาประดิษฐ์ทั่วไป) และมีแผนจะท้าทายการแก้ปัญหาคณิตศาสตร์ที่ซับซ้อนและยากยิ่งขึ้นในอนาคต
การตรวจสอบคำตอบและจุดยืนอย่างเป็นทางการของ IMO
- คณะผู้จัด IMO ยืนยันอย่างเป็นทางการว่าคำตอบที่ส่งมานั้นเป็นวิธีเฉลยที่สมบูรณ์และถูกต้อง
- อย่างไรก็ตาม IMO ระบุชัดว่าการตรวจสอบดังกล่าว ไม่ได้ครอบคลุมถึงการตรวจสอบระบบ กระบวนการ หรือโมเดลพื้นฐานเอง
- สามารถดูรายละเอียดและข้อชี้แจงเพิ่มเติมได้ในแถลงการณ์อย่างเป็นทางการของ IMO (ดูเพิ่มเติม)
5 ความคิดเห็น
OpenAI ประกาศว่าทำผลงานได้ถึงระดับเหรียญทองในการแข่งขันคณิตศาสตร์โอลิมปิกนานาชาติ (IMO) ปี 2025
เมื่อ 2 วันก่อน OpenAI ออกมาประกาศก่อน ทำให้ความตื่นเต้นลดลงไปแล้ว แต่ก็มีเสียงวิจารณ์ด้วยว่า Alexander Wei ของ OpenAI พูดเรื่องนี้ออกมาก่อนโดยไม่ได้หารือกับ IMO เลย ซึ่งถือว่าไม่ค่อยมีมารยาท
เพราะ IMO ยังไม่ได้รับรองอย่างเป็นทางการด้วยซ้ำแต่กลับประกาศออกไปก่อน จึงถูกมองว่าเป็นการแย่งคำยินดีและความดีความชอบที่ควรเป็นของผู้เข้าร่วมทั่วไป ไม่ใช่ของ AI
สรุปคือด้วยเหตุนี้ OAI จึงเป็นเพียงการให้คณะกรรมการของตัวเองตรวจสอบ ไม่ได้อยู่ในสถานะที่ได้รับการให้คะแนนอย่างเป็นทางการจาก IMO เลยครับ ยิ่งไปกว่านั้น เมื่อดูจากความเห็นจำนวนมากที่มองว่าคุณภาพคำตอบของ Gemini ดีกว่านิดหน่อยด้วยแล้ว... ก็ยิ่งเป็นสถานการณ์ที่ดูเสียหน้าเข้าไปอีกหรือเปล่า
ดูเหมือนว่าพวกเขาไม่ต้องรับความเสี่ยงด้านชื่อเสียง และถ้าสำเร็จก็ค่อยประกาศผลออกมา (ทั้งที่ก็ไม่ใช่การให้คะแนนอย่างเป็นทางการ) แต่ถ้าผลออกมาไม่ดีก็ถอนตัว แบบนี้ต่อให้ในงาน benchmark จะทำกันได้ ก็ไม่น่าจะเป็นท่าทีที่เหมาะสมในเวทีการแข่งขันที่ผู้เข้าแข่งขันลงแข่งโดยใช้ชื่อของตัวเองเป็นเดิมพันครับ
แม้ว่า Google กับ OpenAI จะมีประสิทธิภาพของ LLM สูสีกัน แต่ความต่างด้านความช่ำชองขององค์กรก็เห็นได้ชัดตรงนี้
ความเห็นจาก Hacker News
AlphaGeometry และ AlphaProof ใช้กระบวนการแปลโจทย์ภาษาธรรมชาติไปเป็นภาษาเฉพาะโดเมนอย่าง Lean ก่อน แล้วจึงแปลงผลการพิสูจน์กลับมาเป็นภาษาธรรมชาติ และใช้เวลาคำนวณ 2~3 วัน ส่วนโมเดล Gemini ของปีนี้ใช้แนวทาง end-to-end ที่สร้างบทพิสูจน์ทางคณิตศาสตร์โดยตรงจากคำอธิบายโจทย์อย่างเป็นทางการด้วยภาษาธรรมชาติล้วน ๆ กล่าวคือไม่ได้แปลเป็น Lean ก่อน แต่ก็ยังไม่ชัดเจนว่าภายในใช้เครื่องมืออย่าง Lean, การค้นหาบนอินเทอร์เน็ต, เครื่องคิดเลข หรือ Python หรือไม่ OpenAI ระบุว่าโมเดลของตนไม่ได้ใช้เครื่องมือเหล่านี้ แต่ไม่แน่ใจว่าข้ออ้างนั้นใช้กับ Gemini ได้ตรง ๆ หรือไม่ อยากทราบระดับโดยคร่าวของปริมาณการคำนวณหรือค่าใช้จ่ายที่ทั้งสองระบบใช้ด้วย ถ้าราคาแพงมหาศาลก็แปลว่ายังใช้งานจริงได้ไม่มาก ตอนนี้ยังไม่มีข้อมูลเปิดเผยจึงเดาว่าน่าจะแพงมาก และได้แชร์ลิงก์ที่ยืนยันว่า "ไม่มีการใช้เครื่องมือ, ไม่มีการเชื่อมต่ออินเทอร์เน็ต" https://x.com/FredZhang0/status/1947364744412758305
โมเดล Gemini ของปีนี้สร้างบทพิสูจน์ทางคณิตศาสตร์จากคำอธิบายโจทย์อย่างเป็นทางการด้วยภาษาธรรมชาติล้วน ๆ และทุกขั้นตอนเกิดขึ้นภายในเวลาการแข่งขัน 4.5 ชั่วโมง โดยไม่ได้ใช้เครื่องมือภายนอก
อย่างเป็นทางการแล้ว เครื่องมือตรวจพิสูจน์เชิงรูปแบบอย่าง Lean ไม่ได้ถูกใช้ตอนแก้โจทย์ IMO จริง ๆ แต่ก็สงสัยว่าในกระบวนการฝึกโมเดลมีการใช้หรือไม่ งานวิจัย IMO ปี 2024 ของ Google มีเทคนิคแปลงบทพิสูจน์ภาษาธรรมชาติให้เป็นภาษาเชิงรูปแบบที่ตรวจสอบได้อย่างเป็นทางการ และคิดว่าการนำสิ่งนี้ไปใช้กับการฝึกแบบ RLVR (verification-reward via reinforcement learning) น่าจะเป็นก้าวถัดไปที่เป็นธรรมชาติ หากสามารถแปลและตรวจสอบเหตุผลทุกขั้นที่คณิตศาสตร์ LLM สร้างขึ้นแล้วใช้เป็นสัญญาณรางวัลได้ สัญญาณรางวัลก็จะหนาแน่นขึ้นมาก แม้การได้บทพิสูจน์เชิงรูปแบบที่สมบูรณ์แบบยังยากอยู่ แต่ก็น่าจะช่วยชี้นำให้หลีกเลี่ยงการให้เหตุผลผิดหรือประโยคที่ตีความไม่ได้ เมื่อรวมกับพลังคำนวณมหาศาลก็อาจแก้โจทย์ระดับ IMO ได้ด้วย AlphaProof เองก็แสดงให้เห็นแล้วว่าการสลับไปมาระหว่างบทพิสูจน์ Lean กับผลลัพธ์ของ LLM ช่วยสำรวจพื้นที่การให้เหตุผลได้อย่างมีประสิทธิภาพจนแก้โจทย์ระดับ IMO ได้ จึงสงสัยว่าถ้าข้ามขั้นกลางแล้วสอน LLM ให้เลียนแบบการให้เหตุผลเชิงรูปแบบด้วย RLVR จะได้ประสิทธิภาพและความสามารถในการแก้ปัญหาใกล้เคียงกันหรือไม่
ก็สงสัยเหมือนกันว่าทำไมถึงไม่ใช้ Lean หมายความว่าถ้าใช้ Lean ทุกวันนี้การแก้โจทย์จะง่ายเกินไปแล้ว หรือจริง ๆ แล้ว Lean กลับเป็นตัวถ่วงกันแน่
สงสัยด้วยว่า "ไม่มีการใช้เครื่องมือ, ไม่มีการเชื่อมต่ออินเทอร์เน็ต" หมายความว่าในทางปฏิบัติระบบนี้สามารถรันแบบออฟไลน์โดยไม่พึ่งโครงสร้างพื้นฐานของ Google ได้หรือไม่ หรือก็คืออาจนำไปติดตั้งใช้งานแบบโลคัลได้ตามต้องการ
ปีนี้บอกว่า Gemini รุ่นที่ปรับปรุงแล้วสร้างบทพิสูจน์ได้ตรงจากคำอธิบายโจทย์อย่างเป็นทางการด้วยภาษาธรรมชาติล้วน ๆ แต่ผมกลับรู้สึกเสียดายที่มันเหมือนถอยห่างจากเทคนิคการทำให้เป็นเชิงรูปแบบ ผมคิดว่าถ้าจะทำให้คณิตศาสตร์เป็นอัตโนมัติจริง ๆ หรือไปถึงระดับที่สร้างบทพิสูจน์ยาวนับพันหน้าแบบเครื่องจักรได้ ก็ไม่มีทางอื่นนอกจากการทำให้เป็นเชิงรูปแบบ ไม่อย่างนั้นก็ยังต้องมีผู้ตรวจมนุษย์ และไม่มีทางเชื่อถือบทพิสูจน์ได้จริง
ถ้า LLM สามารถสร้างบทพิสูจน์ที่เข้มงวดในภาษาธรรมชาติได้ การพิสูจน์ในภาษาเชิงรูปแบบอย่าง Lean ก็คงไม่ใช่เรื่องยากมากนัก การใช้ Lean ใน AlphaProof นั้นค่อนข้างจำกัดและเฉพาะกับโจทย์คณิตศาสตร์บางประเภท แต่ถ้าทำสิ่งเดียวกันได้ด้วยวิธี RL และภาษาธรรมชาติ ก็อาจขยายไปสู่หลายสาขาที่ตรวจสอบยากได้ด้วย
มีการแชร์ด้วยว่า DeepMind กำลังรวบรวมคลังเก็บที่บันทึกปัญหาที่ยังไม่ถูกแก้อย่างเป็นทางการในรูปแบบเชิงรูปแบบ https://github.com/google-deepmind/formal-conjectures
ผมเป็นนักคณิตศาสตร์แต่ไม่ได้ทำวิจัยแล้ว เลยอยากให้บริบทเล็กน้อยว่าทำไมนักคณิตศาสตร์จำนวนมากจึงไม่ค่อยกระตือรือร้นกับวิธีเชิงรูปแบบ ในทางปฏิบัติถ้าจะสร้างบทพิสูจน์ยาวนับพันหน้า แน่นอนว่าคงเป็นไปไม่ได้หากไม่มีการทำให้เป็นเชิงรูปแบบ และผมก็เห็นด้วยว่าถ้าจะ "เชื่อถือ" บางอย่างจริง ๆ ก็ควรต้องตรวจสอบอย่างเป็นทางการ แต่สิ่งที่นักคณิตศาสตร์ต้องการจริง ๆ คือคำอธิบายว่าเหตุใดผลนั้นจึงเป็นจริง สิ่งสำคัญแท้จริงไม่ใช่คำตอบแบบใช่หรือไม่ใช่ แต่คือการตีความและเหตุผล ตัวอย่างเช่นคนส่วนใหญ่คิดว่าสมมติฐานรีมันน์น่าจะเป็นจริง แต่ก็ไม่ได้แค่รอคำตอบอย่างเดียว แม้แต่ผลลัพธ์ประเภท "ถ้าสมมติฐานรีมันน์เป็นจริง ก็จะได้ทฤษฎีบทใหม่แบบนี้" ก็มีอยู่มาก สิ่งที่คาดหวังจากบทพิสูจน์โดยพื้นฐานคือมุมมองใหม่หรือวิธีที่ทำให้เข้าใจทฤษฎีจำนวนได้ลึกขึ้น ถ้าอย่าง Lean แค่ตรวจว่าเป็นจริงเชิงรูปแบบ แต่มนุษย์กลับไม่เข้าใจเลย มันก็แทบไม่มีความหมาย
การทำให้เป็นเชิงรูปแบบอย่างถูกต้องมักง่ายกว่าการแก้ปัญหา ดังนั้นจะแก้ปัญหาก่อนแล้วค่อยทำให้เป็นเชิงรูปแบบเพื่อตรวจสอบภายหลังก็ได้
เดิมทีโจทย์ IMO ถูกออกแบบมาให้มนุษย์แก้ได้โดยไม่ใช้เครื่องมืออยู่แล้ว ถ้าจะให้โมเดลแก้โจทย์ที่ยากกว่านั้น ก็ค่อยให้เครื่องมือที่เพียงพอได้ อย่างน้อยการจำลองความสามารถระดับมนุษย์โดยไม่ใช้เครื่องมือให้ได้ก่อนก็น่าจะเป็นทิศทางที่ดี
เมื่อเทียบคำตอบของ OpenAI กับ Gemini แล้ว ผมรู้สึกว่าสไตล์การเขียนของ Gemini ชัดเจนกว่ามาก วิธีนำเสนออาจยังปรับให้ดีกว่านี้ได้ แต่ตัวบทพิสูจน์ตามได้ง่าย และใช้ประโยคที่สั้นกว่า กระชับกว่า คำตอบของ OpenAI
บทพิสูจน์ของ Google อาจเป็นผลสรุปที่ถูกย่อขึ้นภายหลัง หรือการสรุปอาจเป็นส่วนหนึ่งของกลไกอย่าง Tree of Thoughts ก็ได้ ดูไม่เหมือนผลลัพธ์จากการสั่งแบบตรงไปตรงมาง่าย ๆ ว่า "ส่งคำตอบสุดท้ายมา"
ผลงานพิสูจน์ IMO ของ OpenAI และ Google ที่ถูกพูดถึงสามารถดูได้ที่ PDF บทพิสูจน์ของ Google และ Repository ตัวอย่างบทพิสูจน์ของ OpenAI
ทั้ง OpenAI และ Google ต่างเน้นว่าพวกเขา "ทำทุกอย่างเสร็จภายในเวลาแข่งขัน 4.5 ชั่วโมง" แต่ก็สงสัยว่าข้อจำกัดนี้มีความหมายสำคัญจริงหรือไม่ ในทางปฏิบัติพวกเขาอาจรันกระบวนการให้เหตุผลแบบขนานกันนับล้านชุดเพื่อค้นหาบทพิสูจน์ก็ได้ แน่นอนว่าการทำแบบนี้ต้องใช้พลังคำนวณมากกับโมเดลประเมินผลที่คอยคัดเลือกและตัดสินว่าบทพิสูจน์ใดควรส่งท้ายสุด อาจกินเวลา GPU รวมกันหลายร้อยปีจริง ๆ ก็ได้ ถึงอย่างนั้นการที่วิธีนี้หาคำตอบได้ และการที่มันขนานงานได้ถึงระดับนี้ ก็ยังน่าทึ่งอยู่ดี ไม่ว่า AGI จะสำเร็จได้ด้วยคอมพิวต์ที่มากขึ้นหรือไม่ สมองมนุษย์ก็ไม่สามารถขยายแบบนี้ได้ง่าย ๆ ดังนั้นผลลัพธ์นี้จึงมีความหมายแน่ชัด
น่าสนใจมากที่แนวทางเปลี่ยนจากระบบเฉพาะทาง Lean ของปีก่อน มาเป็น LLM ทั่วไปที่อิงภาษาธรรมชาติ + RL ในปีนี้ คาดว่าแนวทางนี้จะช่วยเพิ่มประสิทธิภาพในพื้นที่อื่นนอกเหนือจากการแข่งขันคณิตศาสตร์ด้วย อยากเห็นว่ามันจะขยายไปได้ไกลแค่ไหน และระบบนี้ก็ดูเหมือนไม่ต่างจากโมเดล/ฟีเจอร์ "DeepThink" ที่มีกำหนดเปิดตัวในช่วงฤดูร้อนมากนัก
ตอนนี้ให้ความรู้สึกเหมือนกำลังอยู่ในช่วงเวลาแบบ Deep Blue ปะทะ Kasparov สำหรับการแข่งขันคณิตศาสตร์ระหว่างมนุษย์กับเครื่องจักร มีความก้าวหน้าอย่างมหาศาลเมื่อเทียบกับไม่กี่ปีก่อน แต่ผมก็ยังคิดว่ามันยังห่างไกลจากการเป็น AI นักคณิตศาสตร์ที่แท้จริงมาก ถึงอย่างนั้นเราก็อยู่ในยุคที่น่าทึ่งจริง ๆ
ในพอดแคสต์ล่าสุด Terrence Tao ก็แสดงความสนใจอย่างมากต่อการทำงานร่วมกับเครื่องมือแบบนี้ เขาบอกว่าในระยะใกล้วิธีใช้ที่ดีที่สุดน่าจะเป็นให้มนุษย์กำหนดไอเดียหรือพารามิเตอร์ แล้วให้ LLM สำรวจ ค้นหา และพิสูจน์แบบขนานกันไป อุปมาเรื่อง chess engine ก็เหมาะดี สมัยก่อนแม้แต่นักหมากรุกระดับสูงสุดก็ยังมีทีมผู้เชี่ยวชาญจำนวนมากช่วยวิเคราะห์ แต่ทุกวันนี้ใช้ซูเปอร์คอมพิวเตอร์และซอฟต์แวร์วิเคราะห์ตำแหน่งจำนวนมหาศาล คัดไอเดียที่ดีที่สุดแล้วส่งให้ผู้เล่น
ผมคิดว่ามันใกล้กับการที่ Deep Blue แข่งกับเด็กอัจฉริยะมากกว่า เพราะผู้เข้าแข่งขัน IMO ไม่ใช่นักคณิตศาสตร์ระดับโลก แต่เป็นนักเรียนมัธยมปลาย
ความต่างตรงนี้คือการ brute force อย่างเดียวไม่พอจะได้คะแนนสูงภายในเวลาที่กำหนด นี่คือหมุดหมายทางเทคนิคที่แท้จริง และไม่เหมือนกรณี Deep Blue ที่เป็นแค่ "โดยหลักการแล้วเป็นไปได้"
ข้อ 6 ดูน่าสงสัย ทั้ง openai และ deepmind ต่างก็ส่งคำตอบไม่ได้ มนุษย์ยังเขียนคำตอบบางส่วนได้ แต่อยู่ ๆ AI กลับไม่มีคำตอบเลยก็ดูแปลก เลยสงสัยว่า LLM อาจรับรู้เองหรือไม่ว่ามันแก้ไม่สำเร็จ ข้อจำกัดอย่างหนึ่งของ LLM คือ "ไม่รู้ว่าตัวเองไม่รู้" และถ้าเป็นเช่นนั้นก็แทบเป็นไปไม่ได้ที่จะตรวจสอบความสอดคล้องทางตรรกะโดยไม่มีตัวแก้ปัญหา
น่าจะเป็นไปได้มากกว่าว่ามันยัง "คิด" ไม่เสร็จภายในเวลาการแข่งขัน จึงไปไม่ถึงขั้นตอน "ส่งออก" คำตอบ
ข้อจำกัดนี้ใช้กับการสร้างข้อความของ LLM แบบ pretrain พื้นฐานที่สุดเท่านั้น ยังสามารถฝึก linear probe (ชั้นโครงข่ายประสาทอย่างง่าย) เพิ่มเติมเพื่อให้ส่งออก confidence score ได้ด้วย แน่นอนว่าเชื่อถือได้ไม่ถึง 100% แต่ถ้าใช้กับโดเมนจำกัดอย่างคณิตศาสตร์ อย่างน้อยก็อาจน่าเชื่อถือพอสมควร
หากไม่มีเครื่องมือตรวจพิสูจน์เชิงรูปแบบ การนำไปใช้งานจริงก็อาจยังเสี่ยงมาก o3 รุ่นก่อนแม้ไม่ใช่รุ่นล่าสุด แต่ก็เด่นเรื่องการหาเอกสารอ้างอิงและเสนออสมการใหม่ ๆ อย่างไรก็ตาม ในขั้นพิสูจน์จริงมันยังอาจให้คำตอบที่ดูน่าเชื่อถือ แต่มีข้อความผิดหรือความผิดพลาดทางพีชคณิตในรายละเอียดได้ ยิ่งโมเดลดีขึ้น ความผิดพลาดละเอียดแบบนี้อาจกลับยิ่งหายากต่อการตรวจพบ
สงสัยว่าทำไมพวกเขาถึงเน้นมากว่าไม่ได้ใช้ตัวพิสูจน์ทฤษฎีบท สุดท้ายแล้วเครื่องมืออะไรก็ตามที่ช่วยเพิ่มประสิทธิภาพโมเดลก็น่าจะใช้ได้ไม่ใช่หรือ แถม Gemini เองก็ถูกปรับให้เฉพาะทางกับ IMO ด้วย ผ่านการฝึก reinforcement learning บนข้อมูลการให้เหตุผลหลายขั้น การแก้ปัญหา และการพิสูจน์ทฤษฎีบท รวมถึงได้รับคำอธิบายโจทย์คณิตศาสตร์คุณภาพสูงและคำใบ้เกี่ยวกับวิธีเข้าหาโจทย์ IMO
คาดว่า "Gemini Deepthink เวอร์ชันขั้นสูง" น่าจะต่างจาก Deepthink ที่จะอยู่ในผลิตภัณฑ์สมัครสมาชิก Gemini Ultra ตอนเปิดตัวจริง หรืออย่างน้อยก็น่าจะใช้ปริมาณการคำนวณช่วงทดสอบ (test-time compute) มากกว่ามาก ถึงอย่างนั้นการได้เห็น OpenAI กับ Google แข่งกันก็สนุกดี
จะแชร์ลิงก์ system prompt สำหรับ context engineering ที่แก้โจทย์ข้อ 1-6 ได้หมดไว้ให้ ใช้กับ o3 หรือ Gemini 2.5 ก็ได้ ใส่ prompt ทั้งหมดแล้วใส่คำถาม จากนั้นให้มันช่วยแก้โจทย์ได้เลย https://github.com/redcrash0721/freederia/blob/main/imo6kr.pdf