มุมมองของนักคณิตศาสตร์ต่อความสามารถด้านคณิตศาสตร์ของ AI

• โมเดลภาษาใหม่ของ OpenAI อย่าง o3 ทำคะแนนได้ 25% บนเบนช์มาร์กคณิตศาสตร์ยาก FrontierMath ทำให้การประเมินว่า AI ด้านคณิตศาสตร์จะก้าวข้ามระดับปริญญาตรีได้หรือไม่กลับมาสั่นคลอนอีกครั้ง
• FrontierMath เป็นชุดข้อมูลไม่เปิดเผยที่สร้างโดย Epoch AI ประกอบด้วยโจทย์คณิตศาสตร์ยากหลายร้อยข้อที่ต้องการ คำตอบเชิงตัวเลขที่ตรวจสอบอัตโนมัติได้ มากกว่า “การพิสูจน์ทฤษฎีบท”
• ตัวอย่าง 5 ข้อที่เปิดเผยออกมาก็ไม่ง่ายแม้แต่นักคณิตศาสตร์วิจัย Tao ประเมินว่า “ท้าทายอย่างยิ่ง” แต่ Borcherds มองว่าการให้คำตอบเป็นตัวเลขนั้น ไม่เหมือนกับการพิสูจน์อย่างสร้างสรรค์
• เมื่อ Elliot Glazer จาก Epoch AI เปิดเผยว่า 25% ของโจทย์เป็น “โจทย์สไตล์ IMO/ปริญญาตรี” จึงยากจะตรวจสอบได้ว่าคะแนน 25% ของ o3 หมายถึงไปถึงระดับความยากใดจริง ๆ เนื่องจากลักษณะของชุดข้อมูลที่ไม่เปิดเผย
• เป้าหมายที่สำคัญกว่าสำหรับนักคณิตศาสตร์ไม่ใช่ “จงหาตัวเลขนี้” แต่คือ การพิสูจน์ทฤษฎีบทอย่างถูกต้องและอธิบายให้มนุษย์เข้าใจได้ โดยแนวทางที่ใช้โมเดลภาษาและแนวทางที่ใช้ Lean ต่างก็มีข้อจำกัดคนละแบบ

---

เส้นฐานที่ถูก o3 และ FrontierMath สั่นคลอน

• o3 เป็นโมเดลภาษาใหม่ของ OpenAI และทำคะแนนได้ 25% บน FrontierMath
• หลังจาก ChatGPT โมเดลภาษาสาธารณะพัฒนาอย่างรวดเร็ว และความสามารถในการแก้โจทย์คณิตศาสตร์ก็ถูกประเมินอยู่ในกระแสนี้ด้วย
• FrontierMath เป็นชุดข้อมูลโจทย์คณิตศาสตร์แบบไม่เปิดเผยที่สร้างโดย Epoch AI โดยบทคัดย่อของบทความระบุว่ามีโจทย์คณิตศาสตร์ยาก “หลายร้อย” ข้อ
• หากเปิดเผยชุดข้อมูล โมเดลภาษาอาจเรียนรู้โจทย์และคำตอบได้ ดังนั้นแม้แต่ข้อมูลพื้นฐานอย่างจำนวนโจทย์ก็ยังถูกจัดการอย่างระมัดระวัง
  • หากโจทย์และคำตอบถูกเปิดเผย โมเดลอาจเล่นซ้ำคำตอบที่เคยเห็นมาแล้วได้
  • ด้วยเหตุนี้ ความยากจริงและความเป็นตัวแทนของเบนช์มาร์กแบบไม่เปิดเผยจึงตรวจสอบจากภายนอกได้ยาก

รูปแบบและความยากของโจทย์ FrontierMath

• โจทย์ FrontierMath ใกล้เคียงกับรูปแบบ “จงหาตัวเลขนี้” ไม่ใช่ “จงพิสูจน์ทฤษฎีบทนี้”
• โจทย์ต้องมีคำตอบที่ชัดเจนและคำนวณได้ และต้องตรวจสอบอัตโนมัติได้
• คำตอบของโจทย์ตัวอย่างที่เปิดเผย 5 ข้อเป็นจำนวนเต็มบวกทั้งหมด
  • ตัวอย่างคำตอบมี 9811 และ 367707
  • อีกสามคำตอบที่เหลือมีขนาดใหญ่กว่า และถูกออกแบบให้เดาสุ่มให้ถูกได้ยาก
• ตัวอย่างที่เปิดเผยไม่ใช่เรื่องธรรมดาแม้แต่นักคณิตศาสตร์วิจัย
  • ผู้เขียนเข้าใจถ้อยแถลงของโจทย์ทั้ง 5 ข้อทั้งหมด
  • ข้อที่สามแก้ได้ค่อนข้างเร็ว และข้อที่ห้ารู้วิธีแก้ด้วยเทคนิคมาตรฐานที่ใช้ Weil conjectures for curves แต่ไม่ได้คำนวณคำตอบ 13 หลักออกมา
  • ข้อแรกและข้อที่สองตัดสินว่าแก้ไม่ได้ ส่วนข้อที่สี่มองว่าหากพยายามอาจมีความคืบหน้าได้ แต่ไม่ได้ลองและอ่านเฉลยแทน
• นักศึกษาปริญญาตรีคณิตศาสตร์ที่ฉลาดทั่วไปอาจแก้โจทย์เหล่านี้ไม่ได้สักข้อ
  • ผู้เขียนมองว่าโจทย์ข้อแรกน่าจะต้องใช้ระดับปริญญาเอกขึ้นไปในทฤษฎีจำนวนเชิงวิเคราะห์

ข้อดีและข้อจำกัดของเบนช์มาร์กคำตอบตัวเลข

• เหตุผลหลักที่ FrontierMath ใช้โจทย์คำตอบเป็นตัวเลขคือ ต้นทุนการให้คะแนน
• หากจะประเมินคำตอบหลายร้อยชุดของโจทย์ประเภท “จงพิสูจน์ทฤษฎีบท” จำเป็นต้องใช้ผู้เชี่ยวชาญที่เป็นมนุษย์
  • ณ ปี 2024 มองว่ายากที่จะให้เครื่องจักรตรวจงานระดับนี้
• ในทางกลับกัน รายการคำตอบเชิงตัวเลขสามารถให้คอมพิวเตอร์เปรียบเทียบได้อย่างรวดเร็วมาก
• Borcherds มองว่านักคณิตศาสตร์วิจัยใช้เวลาส่วนใหญ่ไปกับการหา การพิสูจน์และไอเดีย ไม่ใช่ตัวเลข
• ถึงอย่างนั้น FrontierMath ก็มีคุณค่าในสาขา AI ด้านคณิตศาสตร์
  • ชุดข้อมูลที่ยากมีอยู่น้อยมาก
  • การสร้างชุดข้อมูลแบบนี้ยากมากหรือมีต้นทุนสูง
  • บทความล่าสุดของ Frieder และคณะพูดถึงข้อจำกัดของชุดข้อมูล AI ด้านคณิตศาสตร์อย่างลึกซึ้งยิ่งขึ้น

เหตุผลที่คะแนน 25% ของ o3 น่าประหลาดใจ

• ในความเข้าใจเดิม AI ด้านคณิตศาสตร์อยู่ใกล้กับ ระดับปริญญาตรีหรือต่ำกว่าปริญญาตรี
• AI กำลังเก่งขึ้นมากกับโจทย์สไตล์โอลิมปิกที่นักเรียนมัธยมปลายอัจฉริยะแก้ได้
• มองว่าเป็นเรื่องแน่นอนว่า AI จะสอบผ่านวิชาคณิตศาสตร์ระดับปริญญาตรีได้ภายใน 1 ปี
  • ข้อสอบปริญญาตรีบางครั้งมีโจทย์มาตรฐานเพื่อให้นักศึกษาที่เข้าใจเนื้อหาวิชาในระดับพื้นฐานสามารถสอบผ่านได้
  • เครื่องจักรสามารถตอบโจทย์แบบนี้ได้ง่าย
• แต่การกระโดดจากการนำไอเดียมาตรฐานกลับมาใช้ซ้ำ ไปสู่ไอเดียเชิงนวัตกรรมระดับปริญญาตรีขั้นสูงหรือช่วงต้นปริญญาเอก ยังถือว่าใหญ่
• คำตอบของ ChatGPT ต่อข้อสอบ Putnam ล่าสุดต่ำกว่าความคาดหวัง
  • ดูเหมือนว่าเครื่องตอบได้เหมาะสมเพียงข้อ B4 เท่านั้น
  • คำตอบอื่น ๆ ส่วนใหญ่มองว่าอยู่ระดับ 1–2 คะแนนจาก 10 คะแนน
• ด้วยเหตุผลเหล่านี้ จึงเคยคาดว่า FrontierMath จะเกือบโจมตีไม่ได้อยู่หลายปี

ความไม่แน่นอนที่ชุดข้อมูลไม่เปิดเผยทิ้งไว้

• Elliot Glazer จาก Epoch AI เปิดเผยบน Reddit ว่า 25% ของโจทย์ FrontierMath เป็น โจทย์สไตล์ IMO/ปริญญาตรี
• ข้อความนี้ดูไม่ค่อยสอดคล้องกับโจทย์ 5 ข้อที่เปิดเผย
  • แม้แต่โจทย์ที่ง่ายที่สุดในตัวอย่างที่เปิดเผย ก็มีวิธีที่ใช้ Weil conjectures for curves
  • หรืออาจต้องใช้วิธี brute force ที่เจ็บปวดในการแยกตัวประกอบพหุนามกำลังสามดีกรี 10^12 บนฟิลด์จำกัด
• ข้อมูลนี้ทิ้งคำถามไว้เกี่ยวกับความยากของชุดข้อมูลไม่เปิดเผยจริง ๆ และว่าโจทย์ 5 ข้อที่เปิดเผยเป็นตัวอย่างที่เป็นตัวแทนหรือไม่
• เนื่องจากชุดข้อมูลไม่เปิดเผย คำถามนี้จึงตรวจสอบได้ไม่ง่าย
• หาก 25% เป็นโจทย์ระดับปริญญาตรี คะแนน 25% ของ o3 ก็อาจไม่น่าประหลาดใจเท่าไร
• จุดทะลุทะลวงใหญ่ที่คาดหวังคือช่วงที่ AI แสดงผลงานมีนัยสำคัญบนโจทย์ 50% ถัดไปที่ถูกอธิบายว่าเป็น “qual level”

“จงพิสูจน์ทฤษฎีบท” ยังคงเป็นปัญหาอีกแบบ

• ในงานวิจัยคณิตศาสตร์ คำถามสำคัญโดยทั่วไปคือ “จงพิสูจน์ทฤษฎีบทนี้”
• แม้จะมีเครื่องจักรที่ทำผลงานเหนือมนุษย์ในโจทย์หาตัวเลข ความสามารถในการนำไปใช้ในหลายพื้นที่ของคณิตศาสตร์วิจัยก็อาจจำกัด
• กรณีความสำเร็จที่ใหญ่ที่สุดในปี 2024 ถูกยกให้เป็น AlphaProof ของ DeepMind
  • AlphaProof แก้โจทย์ IMO 2024 ได้ 4 ข้อจาก 6 ข้อ
  • โจทย์เป็นประเภท “จงพิสูจน์ทฤษฎีบท” หรือ “จงหาตัวเลขและพิสูจน์ว่าถูกต้อง”
  • ในจำนวนนี้ 3 ข้อถูกส่งออกมาเป็นการพิสูจน์ Lean ที่ formalize อย่างสมบูรณ์
• Lean เป็น interactive theorem prover และ mathlib เป็นไลบรารีคณิตศาสตร์ที่รวมเทคนิคหลายอย่างที่จำเป็นต่อการแก้โจทย์ IMO และมากกว่านั้น
• คำตอบของระบบ DeepMind ได้รับการตรวจสอบโดยมนุษย์ และยืนยันว่าเป็นคำตอบ “เต็มคะแนน”
• อย่างไรก็ตาม แม้โจทย์ IMO จะยากมาก แต่วิธีแก้ใช้เพียงเทคนิคระดับโรงเรียน ดังนั้นจึงเท่ากับกลับมาที่โจทย์ระดับมัธยมปลายอีกครั้ง
• คาดว่าในปี 2025 เครื่องจักรจะแสดงสมรรถนะระดับเหรียญทอง IMO

ใครจะให้คะแนนคำตอบของเครื่องจักร

• เราสามารถจินตนาการสถานการณ์ใน IMO เดือนกรกฎาคม 2025 ที่ไม่ใช่แค่นักเรียนมนุษย์ แต่มีเครื่องจักรเข้าร่วมด้วย
• ระบบเครื่องจักรอาจแบ่งได้เป็นสองประเภท
  • ระบบที่ส่งคำตอบด้วยภาษาของ computer proof checker เช่น Lean, Rocq, Isabelle
  • โมเดลภาษาที่ส่งคำตอบเป็นภาษามนุษย์
• สำหรับคำตอบที่ส่งด้วยภาษาของ proof checker ต้องตรวจสอบเพียงว่าถ้อยแถลงของโจทย์ถูกแปลอย่างถูกต้องหรือไม่
  • หลังจากนั้น หากการพิสูจน์คอมไพล์ผ่าน ก็แทบจะรู้ได้ว่าเป็นคำตอบ “เต็มคะแนน”
• โมเดลภาษาที่ส่งคำตอบเป็นภาษาธรรมชาตินั้นต่างออกไป
  • แม้คำตอบจะดูน่าเชื่อถือ ผู้ตรวจที่เป็นมนุษย์ก็ต้องอ่านอย่างละเอียดและประเมิน
  • ไม่มีการรับประกันว่าเป็นคำตอบเต็มคะแนน
• มองว่าโมเดลภาษามีความแม่นยำในการให้เหตุผลเชิงตรรกะน้อยกว่าผู้เชี่ยวชาญมนุษย์อย่างน้อยราวหนึ่งลำดับขั้น
• มีความกังวลว่า “การพิสูจน์” สมมติฐานรีมันน์โดยโมเดลภาษาอาจแทรกข้ออ้างที่คลุมเครือหรือไม่ถูกต้องไว้กลางคณิตศาสตร์ที่ถูกต้องยาว 10 หน้า
• ในทางกลับกัน theorem prover ถูกมองว่าแม่นยำกว่าอย่างน้อยราวหนึ่งลำดับขั้น
  • ในกรณีที่ผู้เขียนเคยเห็น เมื่อ Lean ไม่ยอมรับข้อโต้แย้งในวรรณกรรมคณิตศาสตร์ของมนุษย์ ฝั่งมนุษย์เป็นฝ่ายผิด

เป้าหมายที่เหลือ: การพิสูจน์ที่ถูกต้องและความเข้าใจของมนุษย์

• สิ่งที่นักคณิตศาสตร์ต้องการไม่ใช่แค่ “จงพิสูจน์ทฤษฎีบท” แต่คือ การพิสูจน์ที่ถูกต้อง และคำอธิบายที่มนุษย์เข้าใจได้
• ในแนวทางที่ใช้โมเดลภาษา “ความถูกต้อง” ยังเป็นความกังวลใหญ่
• ในแนวทางที่ใช้ theorem prover “วิธีที่มนุษย์เข้าใจได้” คือความกังวล
• ยังมีงานต้องทำอีกมาก
• ความเร็วในการพัฒนานั้นสูง แต่ไม่มีใครรู้ว่าจะข้าม กำแพงระดับปริญญาตรี ได้เมื่อใด