AI ของ DeepMind แก้โจทย์โอลิมปิกคณิตศาสตร์นานาชาติได้ในระดับเหรียญเงิน

(deepmind.google)

3 คะแนน โดย GN⁺ 2024-07-26 | 3 ความคิดเห็น | แชร์ทาง WhatsApp

AlphaProof และ AlphaGeometry 2 ของ Google DeepMind สามารถแก้โจทย์ International Mathematical Olympiad ได้
- AlphaProof: ระบบให้เหตุผลทางคณิตศาสตร์ที่อิงกับการเรียนรู้แบบเสริมกำลัง
- AlphaGeometry 2: ระบบแก้ปัญหาเรขาคณิตที่ได้รับการปรับปรุง
- ทั้งสองระบบแก้ได้ 4 จาก 6 ข้อในการแข่งขัน International Mathematical Olympiad (IMO) ปีนี้ ทำผลงานได้ในระดับเหรียญเงิน

ความก้าวหน้าของ AI ในการแก้ปัญหาคณิตศาสตร์ที่ซับซ้อน

แนะนำ IMO
- การแข่งขันคณิตศาสตร์เยาวชนที่เก่าแก่และทรงเกียรติที่สุด จัดขึ้นทุกปีตั้งแต่ปี 1959
- โจทย์การแข่งขันออกจากพีชคณิต คอมบินาทอริกส์ เรขาคณิต และทฤษฎีจำนวน
- ผู้ได้รับรางวัล Fields Medal จำนวนมากเคยผ่าน IMO มาแล้ว
ความท้าทาย IMO ของระบบ AI
- AlphaProof และ AlphaGeometry 2 แก้โจทย์ IMO ของปีนี้ได้
- โจทย์ถูกให้คะแนนตามกติกาอย่างเป็นทางการของการแข่งขัน
- AlphaProof แก้โจทย์พีชคณิต 2 ข้อและโจทย์ทฤษฎีจำนวน 1 ข้อ
- AlphaGeometry 2 แก้โจทย์เรขาคณิต 1 ข้อ
- โจทย์คอมบินาทอริกส์ 2 ข้อยังแก้ไม่ได้
- ได้คะแนนรวม 28 จาก 42 คะแนน ทำผลงานได้ในระดับเหรียญเงิน

AlphaProof: แนวทางการให้เหตุผลแบบเป็นทางการ

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

AlphaGeometry 2 ที่แข่งขันได้มากขึ้น

จุดปรับปรุงของ AlphaGeometry 2
- ใช้โมเดลภาษาที่อิงกับ Gemini และระบบไฮบริดแบบ neural-symbolic
- ฝึกด้วยข้อมูลสังเคราะห์มากกว่ารุ่นก่อน 10 เท่า
- เพิ่มความเร็วและความแม่นยำในการแก้โจทย์เรขาคณิต
- ใช้กลไกการแบ่งปันความรู้เมื่อแก้โจทย์ใหม่
ผลงานใน IMO 2024
- แก้โจทย์เรขาคณิตของ IMO ในช่วง 25 ปีที่ผ่านมาได้ 83%
- ในการแข่งขันปีนี้ แก้ข้อ 4 ได้ภายใน 19 วินาที

พรมแดนใหม่ของการให้เหตุผลทางคณิตศาสตร์

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

สรุปของ GN⁺

AlphaProof และ AlphaGeometry 2 แสดงให้เห็นถึงศักยภาพของ AI ในการให้เหตุผลทางคณิตศาสตร์
การทำผลงานระดับเหรียญเงินใน International Mathematical Olympiad เป็นหลักฐานถึงความสามารถของ AI ในการแก้ปัญหาคณิตศาสตร์
เปิดความเป็นไปได้ให้นักคณิตศาสตร์ทำงานร่วมกับ AI เพื่อสำรวจแนวทางการแก้ปัญหาแบบใหม่
โครงการที่มีลักษณะคล้ายกันมีโมเดลประมวลผลภาษาธรรมชาติอย่าง GPT-3 ของ OpenAI

3 ความคิดเห็น

chabulhwi 2024-07-26

ยิ่งมีนักคณิตศาสตร์ที่ช่วยพัฒนาไลบรารีคณิตศาสตร์เชิงรูปนัยมากขึ้นเท่าไร ก็จะยิ่งสร้าง AI ด้านคณิตศาสตร์ที่มีประสิทธิภาพสูงได้ง่ายขึ้นเท่านั้น เท่าที่ผมทราบ ตอนนี้มีชาวเกาหลีอยู่ 3 คนที่กำลังย้ายทฤษฎีคณิตศาสตร์ซึ่งตนเองได้ทำให้เป็นเชิงรูปนัยโดยตรงด้วยภาษาของตัวช่วยพิสูจน์ Lean ไปยัง Mathlib ซึ่งเป็นไลบรารีคณิตศาสตร์ของ Lean

เมื่อปีที่แล้ว ผมมีส่วนร่วมอยู่บ้างในการย้าย Mathlib จาก Lean 3 ไปเป็น Lean 4 และในปีนี้ ผมได้พิสูจน์ทฤษฎีบทที่ยังไม่ถูกแก้อยู่อันหนึ่งในไลบรารี Batteries ของ Lean 4

GN⁺ 2024-07-26

ความเห็นจาก Hacker News

ความเห็นที่หนึ่ง
- ตื่นเต้นกับโปรเจ็กต์นี้มาก แต่ยังไม่ชัดเจนว่าคอมพิวเตอร์มีส่วนช่วยมากแค่ไหนในกระบวนการแปลโจทย์คณิตศาสตร์ให้เป็นภาษาทางการ
- จากโซลูชันที่ดาวน์โหลดได้ ยังไม่ชัดเจนว่าส่วนไหนเป็นสิ่งที่มนุษย์ตัดสินใจในกระบวนการแปล และส่วนไหนเป็นสิ่งที่คอมพิวเตอร์ค้นพบ
ความเห็นที่สอง
- ใน IMO เหรียญจะมอบให้ผู้เข้าแข่งขัน 50% โดยมีสัดส่วนเหรียญทอง เงิน และทองแดงเป็น 1:2:3
- การที่ AI ทำได้ดีกว่านักเรียน 75% ถือว่าน่าประทับใจ
- อย่างไรก็ตาม เวลาที่ AI ใช้แก้โจทย์แตกต่างจากเวลาที่นักเรียนได้รับในสนามสอบ จึงไม่เหมาะจะนำมาเปรียบเทียบโดยตรง
ความเห็นที่สาม
- AlphaGeometry แก้ได้เฉพาะโจทย์ที่มีขอบเขตจำกัด แต่แนวทางครั้งนี้จะส่งผลต่อวงการคณิตศาสตร์ได้กว้างขวางกว่า
- กำลังพัฒนา pipeline ที่แปลงคณิตศาสตร์ภาษาธรรมชาติให้เป็นคณิตศาสตร์แบบ formalized และสิ่งนี้อาจเรียนรู้การสร้างทฤษฎีพื้นฐานได้ด้วย
- นี่คือจอกศักดิ์สิทธิ์ของ proof assistant และจะช่วยให้มนุษย์ทำให้คณิตศาสตร์เป็นแบบ formalized ได้อย่างเป็นธรรมชาติมากขึ้น
ความเห็นที่สี่
- ถ้าระบบใช้เวลา 3 วันในการแก้โจทย์ ก็แทบไม่ต่างจากการ brute force แบบตรงไปตรงมา
- นี่ไม่ใช่การให้เหตุผลที่แท้จริง
ความเห็นที่ห้า
- กำลังใช้ Lean
- สิ่งนี้สำคัญไม่ใช่แค่กับปัญหาคณิตศาสตร์ แต่ยังสำคัญต่อการหลีกเลี่ยงผลลัพธ์ไร้ความหมายโดยทั่วไป
- หวังว่าจะมีคนเขียน type ในระบบอย่าง Lean มากขึ้น
ความเห็นที่หก
- อิจฉาคนที่ได้เข้าร่วมโปรเจ็กต์นี้
- การได้พัฒนาเทคโนโลยีล้ำสมัยคงทั้งสนุกและให้ความพึงพอใจมาก
ความเห็นที่เจ็ด
- การถกเถียงที่ดีที่สุดเกิดขึ้นในแชต Zulip ของ LeanProver
ความเห็นที่แปด
- Tim Gowers ผู้ได้รับเหรียญ Fields ได้ให้ภาพรวมที่ดี พร้อมอธิบายข้อควรระวังสำคัญและให้บริบทประกอบ
ความเห็นที่เก้า
- การพิสูจน์ทฤษฎีบทคือเกมผู้เล่นคนเดียวที่มีพื้นที่การค้นหาขนาดใหญ่มาก
- ผู้มีส่วนสำคัญที่สุดต่อ AlphaProof คือผู้พัฒนา Lean และ Mathlib
- การขาด formalization ในงานวิจัยคณิตศาสตร์ได้ขัดขวางความพยายามด้านระบบอัตโนมัติ
ความเห็นที่สิบ
- เครื่องจักรเหนือกว่ามนุษย์ในหมากรุกมาหลายทศวรรษแล้ว
- แต่ผู้คนก็ยังคงติดตาม Magnus Carlsen
- มนุษย์สนใจการกระทำของมนุษย์คนอื่น
- เครื่องจักรจะน่าสนใจก็ต่อเมื่อมันมีประโยชน์ต่อมนุษย์