AlphaGeometry ระบบ AI ด้านเรขาคณิตระดับโอลิมปิก

 (deepmind.google)
1 คะแนน โดย GN⁺ 2024-01-18 | 1 ความคิดเห็น | แชร์ทาง WhatsApp
  • ในช่วงที่ International Mathematical Olympiad กลายเป็นสนามทดสอบของการให้เหตุผลทางคณิตศาสตร์ของ AI นั้น AlphaGeometry สามารถแก้โจทย์เรขาคณิตได้ 25 จาก 30 ข้อภายในเวลาที่กำหนด ใกล้เคียงกับค่าเฉลี่ย 25.9 ข้อของผู้ได้เหรียญทองมนุษย์
  • หัวใจสำคัญคือการผสาน โมเดลภาษาประสาท เข้ากับ เอนจินให้เหตุผลเชิงสัญลักษณ์ แบบอิงกฎ เพื่อจัดการทั้งการเสนอการสร้างเสริมเชิงสัญชาตญาณและการตรวจสอบด้วยตรรกะเชิงรูปนัยภายในลูปเดียว
  • ตัวอย่างสังเคราะห์ที่ไม่ซ้ำกัน 100 ล้านรายการ ซึ่งสร้างขึ้นโดยไม่มีการสาธิตจากมนุษย์ ช่วยลดคอขวดด้านการฝึก และในจำนวนนี้ 9 ล้านรายการมีการสร้างเสริมที่จำเป็นต่อการพิสูจน์
  • คำตอบโอลิมปิกทั้งหมดได้รับการตรวจสอบด้วยคอมพิวเตอร์ และ Evan Chen ประเมินว่าผลลัพธ์นั้นตรวจสอบด้วยเครื่องได้ ขณะเดียวกันมนุษย์ก็อ่านเข้าใจได้ และเป็นไปตามกฎเรขาคณิตคลาสสิกที่นักเรียนใช้
  • โดยปกติ IMO หนึ่งครั้งมี 6 ข้อ และมีเพียง 2 ข้อที่เป็นเรขาคณิต จึงมีขอบเขตการใช้งานจำกัด แต่จากความสามารถด้านเรขาคณิตเพียงอย่างเดียว ก็ทำให้มันเป็นโมเดล AI ตัวแรกที่ทำคะแนนเกินเกณฑ์เหรียญทองแดง IMO ปี 2000 และ 2015 ได้

ผลงานบนเบนช์มาร์กเรขาคณิต IMO

  • AlphaGeometry ที่เผยแพร่ใน Nature สามารถแก้ปัญหาเรขาคณิตที่ซับซ้อนได้ในระดับใกล้เคียงกับผู้ได้เหรียญทองโอลิมปิกมนุษย์
  • เบนช์มาร์กประกอบด้วยโจทย์เรขาคณิต IMO-AG-30 จำนวน 30 ข้อ ที่คัดมาจากการแข่งขันโอลิมปิกช่วงปี 2000 ถึง 2022
    • AlphaGeometry: แก้ได้ 25 ข้อภายในเวลาที่กำหนด
    • Wu’s method ซึ่งเป็นแนวทางที่ดีที่สุดก่อนหน้านี้: แก้ได้ 10 ข้อ
    • ค่าเฉลี่ยผู้ได้เหรียญทองมนุษย์: แก้ได้ 25.9 ข้อ
  • Google DeepMind เปิดซอร์ส โค้ดและโมเดลของ AlphaGeometry

โครงสร้างระบบประสาท-สัญลักษณ์

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

ลูปการแก้โจทย์เพื่อค้นหาองค์ประกอบเสริม

  • โจทย์เรขาคณิตระดับโอลิมปิกบางครั้งไม่สามารถแก้ได้ทันทีจากรูปที่ให้มา และจำเป็นต้องเพิ่มองค์ประกอบเรขาคณิตใหม่ที่จำเป็นต่อวิธีแก้
  • กระบวนการแก้โจทย์ของ AlphaGeometry ทำงานแบบสลับกันระหว่างการให้เหตุผลเชิงสัญลักษณ์และข้อเสนอจากโมเดลภาษา
    • จากรูปที่กำหนดและสมมุติฐานของทฤษฎีบท เอนจินให้เหตุผลเชิงสัญลักษณ์จะอนุมานข้อความใหม่
    • หากยังหาคำตอบไม่พบ หรือไม่สามารถสร้างข้อความใหม่ได้อีก โมเดลภาษาจะเพิ่มองค์ประกอบเสริมหนึ่งรายการที่มีแนวโน้มว่าจะเป็นประโยชน์
    • องค์ประกอบที่เพิ่มเข้ามาจะเปิดเส้นทางใหม่ให้เอนจินให้เหตุผล และกระบวนการนี้จะทำซ้ำไปจนกว่าจะพบคำตอบ
  • ในข้อ 3 ของ International Mathematical Olympiad ปี 2015 คำตอบของ AlphaGeometry ประกอบด้วย 109 ขั้นของตรรกะ

การสร้างข้อมูลสังเคราะห์ 100 ล้านรายการ

  • เรขาคณิตตั้งอยู่บนความเข้าใจเรื่องปริภูมิ ระยะทาง รูปร่าง และตำแหน่งสัมพัทธ์ และเป็นพื้นฐานของหลายสาขา เช่น ศิลปะ สถาปัตยกรรม และวิศวกรรม
  • วิธีสร้างข้อมูลสังเคราะห์ของ AlphaGeometry เป็นการจำลองในวงกว้างถึงกระบวนการที่มนุษย์มองรูปเรขาคณิตแล้วใช้ความรู้เดิมค้นหาสมบัติและความสัมพันธ์ใหม่ทางเรขาคณิต
  • ระบบสร้าง รูปเรขาคณิตสุ่ม 1 พันล้านรูป ด้วยการประมวลผลแบบขนานสูง
    • อนุมานความสัมพันธ์ทั้งหมดระหว่างจุดและเส้นในแต่ละรูปอย่างละเอียดถี่ถ้วน
    • ค้นหาการพิสูจน์ทั้งหมดที่มีอยู่ในแต่ละรูป
    • ย้อนรอยว่าจำเป็นต้องมีองค์ประกอบเสริมใดบ้างจึงจะไปถึงการพิสูจน์นั้นได้
  • กระบวนการนี้เรียกว่า symbolic deduction and traceback
  • พูลข้อมูลขนาดมหึมานี้ถูกกรองเพื่อคัดออกตัวอย่างที่คล้ายกัน ทำให้สุดท้ายได้ ตัวอย่างฝึกที่ไม่ซ้ำกัน 100 ล้านรายการ ที่มีระดับความยากหลากหลาย
    • ในจำนวนนี้ 9 ล้านรายการเป็นกรณีที่มีการเพิ่มองค์ประกอบเสริม
    • โมเดลภาษาฝึกจากตัวอย่างจำนวนมากที่การสร้างเสริมนำไปสู่การพิสูจน์ จึงสามารถเสนอการสร้างใหม่ในโจทย์โอลิมปิกได้

ความสามารถในการตรวจสอบและข้อจำกัดการใช้งาน

  • คำตอบของ AlphaGeometry สำหรับโจทย์โอลิมปิกทั้งหมดได้รับการ ตรวจสอบและยืนยันด้วยคอมพิวเตอร์
  • ผลลัพธ์ถูกนำไปเปรียบเทียบกับวิธี AI ก่อนหน้าและผลงานของมนุษย์ในโอลิมปิก
  • Evan Chen ซึ่งเป็นโค้ชคณิตศาสตร์และอดีตผู้ได้เหรียญทองโอลิมปิก ได้ประเมินคำตอบบางส่วน
    • ผลลัพธ์ของ AlphaGeometry ตรวจสอบได้และเรียบร้อย
    • ในอดีต คำตอบจาก AI สำหรับโจทย์แข่งขันแบบพิสูจน์เคยมีทั้งกรณีที่ถูกและผิด จึงอาจต้องให้มนุษย์ตรวจสอบ
    • คำตอบของ AlphaGeometry มีโครงสร้างที่เครื่องตรวจสอบได้ ขณะเดียวกันมนุษย์ก็อ่านได้เข้าใจ
    • แทนที่จะใช้ระบบพิกัดเพื่อไล่คำนวณพีชคณิตปริมาณมหาศาล มันใช้ กฎเรขาคณิตแบบคลาสสิก เช่น มุมและสามเหลี่ยมคล้าย เหมือนที่นักเรียนใช้
  • IMO หนึ่งครั้งประกอบด้วย 6 ข้อ และโดยทั่วไปมีเพียง 2 ข้อที่เน้นเรขาคณิต
    • ดังนั้น AlphaGeometry จึงใช้ได้กับเพียงประมาณหนึ่งในสามของโจทย์แต่ละครั้ง
    • ถึงอย่างนั้น ด้วยความสามารถด้านเรขาคณิตเพียงอย่างเดียว มันก็เป็นโมเดล AI ตัวแรกที่สามารถผ่านเกณฑ์เหรียญทองแดง IMO ปี 2000 และ 2015 ได้

ขยายสู่ AI สำหรับการให้เหตุผลทางคณิตศาสตร์

  • AlphaGeometry แสดงให้เห็นว่า AI กำลังมีความสามารถมากขึ้นในการ ให้เหตุผลเชิงตรรกะ และค้นพบรวมถึงตรวจสอบความรู้ใหม่
  • การแก้โจทย์เรขาคณิตระดับโอลิมปิกเป็นหมุดหมายสำคัญสู่การให้เหตุผลทางคณิตศาสตร์ที่ลึกยิ่งขึ้นและระบบ AI ทั่วไปที่ก้าวหน้ากว่าเดิม
  • แนวทางการฝึก AI ตั้งแต่ต้นด้วยข้อมูลสังเคราะห์ขนาดใหญ่ อาจส่งผลต่อวิธีการค้นพบความรู้ใหม่ในวิทยาศาสตร์และ AI ที่กว้างไกลกว่าคณิตศาสตร์
  • AlphaGeometry ตั้งอยู่บนสายงาน AI ด้านการให้เหตุผลทางคณิตศาสตร์ของ Google DeepMind และ Google Research
  • เป้าหมายระยะยาวคือการทำให้สามารถทั่วไปได้ครอบคลุมหลายสาขาของคณิตศาสตร์ พัฒนาการแก้ปัญหาและการให้เหตุผลที่ซับซ้อนซึ่งจำเป็นต่อระบบ AI ทั่วไป และสร้างระบบ AI ที่ขยายขอบเขตความรู้ของมนุษย์

บทความที่เกี่ยวข้อง

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

 
GN⁺ 2024-01-18
ความคิดเห็นจาก Hacker News

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

    • ในฐานะคนที่เป็นฝ่ายแก้โจทย์พวกนั้น ต้องขอขอบคุณก่อนเลย ถึงจะเรียนจบมัธยมมาหลายสิบปีแล้ว ฉันก็ยังหยิบมาทำเล่นอย่างเพลิดเพลินเป็นครั้งคราว
      เห็นด้วยว่าเรขาคณิตน่าจะมาก่อน จากที่เห็นที่นี่ มันไม่ใช่ “การไล่ลองแบบเดาสุ่ม” ในความหมายที่พึ่งวิธีแก้ด้วยเรขาคณิตเชิงพีชคณิต เวกเตอร์ หรือจำนวนเชิงซ้อน แต่ใกล้เคียงกับการค้นหาแบบครอบจักรวาลในความหมายที่ว่ามันกวาดหาการสร้างเสริมที่ “น่าสนใจ” อย่างละเอียด
      เรขาคณิตเป็นวิชาที่ฉันแย่ที่สุดมาตลอด แต่ก็รู้สึกว่าเมื่อได้การสร้างที่ถูกต้องแล้ว โจทย์จะง่ายขึ้นมาก เพียงแต่ฉันไม่เคยฝึกสัญชาตญาณในการนึกการสร้างแบบนั้นได้อย่างรวดเร็ว AI ตัวนี้ก็ดูเหมือนจะไม่ได้มีสัญชาตญาณแบบนั้นเหมือนกัน แต่สามารถพ่นตัวเลือกออกมาได้เร็วกว่ามาก ท้ายที่สุดแล้วตัวเลือกที่สร้างได้ เช่น เส้นตั้งฉาก เส้นขนาน เส้นแบ่งครึ่ง ก็มีจำนวนจำกัด และยังประเมินได้ค่อนข้างเป็นกลไกด้วยการคลี่มุมและอัตราส่วนทั้งหมดออกมาดู หรือทดลองใช้ทฤษฎีกำลังของจุด
      มันน่าประทับใจมาก แต่ในความหมายของ “เอนจินปะทะ AI” มันดูเหมือน DeepMind:Kasparov::AlphaGeo:Terry Tao มากกว่า
      เห็นด้วยว่าพีชคณิตมีโอกาสเป็นรายต่อไปสูง เพราะเหมือนเรขาคณิตตรงที่โดยมากแค่หาการแทนค่าที่ฉลาดสักหนึ่ง สอง หรือสามตัวก็พอ และตัวเลือกก็มีไม่มาก
      ปัญหาคอมบินาทอริกส์บางส่วนอาจเข้ากับกลยุทธ์การค้นหาแบบนี้ได้เช่นกัน เช่น โจทย์ที่นับวัตถุเดียวกันด้วยสองวิธี เพียงแต่นั่นยังเป็นสะพานที่ไกลกว่า และน่าจะครอบคลุมได้แค่บางส่วนของปัญหาทั้งหมด
      ทฤษฎีจำนวนน่าจะเป็นปราการสุดท้ายก่อนจะไปถึงคะแนนเต็ม 42 คะแนน
    • ชอบท่าทีที่มองความก้าวหน้าแบบนี้ในแง่บวกนะ สงสัยว่าคุณรู้สึกสูญเสียบ้างไหมกับความเป็นไปได้ที่ความสามารถด้านคณิตศาสตร์ระดับสูงมากอาจถูกเครื่องจักรไล่ทันได้ หรือมองว่าสิ่งนั้นยังไม่น่าจะเกิดขึ้นไปอีกพักใหญ่?
    • สงสัยว่าคุณเข้าไปอยู่ในบทบาทผู้ออกข้อสอบแบบนั้นได้อย่างไร มีขั้นตอนสมัครอะไรทำนองนั้นไหม?
      แล้วหลังจากตรวจสอบแล้วว่าโจทย์แก้ได้จริง เขาเลือกอย่างไรว่าโจทย์ไหนจะเข้าไปอยู่ในชุดข้อสอบสุดท้าย เป็นการโหวตหรือใช้วิธีประเมินแบบอื่น?
    • ตอนแรกฉันคิดว่า อสมการสามตัวแปรจะเป็นอย่างแรกที่ถูกโค่น เพราะมีความกำกวมเกี่ยวกับสิ่งที่จะนับว่าเป็นบทพิสูจน์น้อยกว่า แต่ฉันไม่รู้มาก่อนเลยว่าปัญหาชุดหลังนั้นถูกแก้ไปแล้วตั้งแต่ปี 2000 (http://www.mmrc.iss.ac.cn/~xgao/paper/jar-gdbase.pdf)
      ใครสักคนควรทำเรขาคณิตสังเคราะห์ให้เป็นเกมผจญภัยได้แล้ว น่าจะใช้ภาษาสำหรับเขียนบทพิสูจน์ที่ง่ายกว่า Lean และยังทำให้ดูสวยงามในเชิงภาพได้ด้วย

  • ถ้าผมอ่านงานวิจัยนี้ถูกต้อง นี่ดูเหมือนเป็นผลงานจริง มากกว่างานวิจัย AI ด้านคณิตศาสตร์ของ DeepMind ที่เมื่อเดือนก่อนโปรโมตผิด ๆ ว่าแก้ปัญหาวิจัยคณิตศาสตร์แบบเปิดได้เสียอีก ถึงอย่างนั้นก็ยังเห็นได้ชัดว่าโครงสร้างของมันต่างจากสิ่งที่คนทั่วไปนึกถึงเมื่อพูดถึง การให้เหตุผลอัตโนมัติ/ปัญญา มากพอสมควร
    เท่าที่ผมเข้าใจคือเอา Transformer ไปฝึกด้วยทฤษฎีบทเรขาคณิตระดับพื้นฐานนับล้านข้อ แล้วใช้มันกับการค้นหาพิสูจน์แบบ brute force เพราะบริบทเป็นเรขาคณิตพื้นฐาน โครงสร้างจึงจำเป็นต้องเป็นระดับพื้นฐาน และตัดสินจริง/เท็จเชิงสัญลักษณ์ได้ค่อนข้างง่าย ถ้าการค้นหาแบบ brute force ล้มเหลว ก็จะเพิ่มการสร้างเรขาคณิตเสริมอย่างการเพิ่มจุดกึ่งกลางแบบสุ่ม แล้วดูว่าค้นหาต่อได้ไหมด้วยวัสดุที่เพิ่มเข้ามานั้น
    แก้ไข: ตามที่ Imnimo แก้ไว้ ผมเข้าใจกลับด้าน การค้นหาแบบ brute force เป็น brute force ล้วน ๆ ส่วน Transformer ใช้ทำนายว่าจะเพิ่มการสร้างเสริมแบบใด
    อีกอย่างหนึ่งที่ไม่มีในโพสต์บล็อกคือโจทย์จริงก็ต้องถูกแก้ไข/ดัดแปลงด้วย เช่น ประโยคต้นฉบับอย่าง “ให้ความสูงของสามเหลี่ยม ABC เป็น AH1, BH2, CH3…” ถูกเปลี่ยนเป็นการไล่นิยามที่ชัดเจนกว่ามาก เช่น “ให้ ABC เป็นสามเหลี่ยม ให้ AI เป็นเส้นแบ่งครึ่งมุม BAC และให้ CI เป็นเส้นแบ่งครึ่งมุม ACB โดยนิยามจุด I...” และลงท้ายเป็นรูปแบบ “จงพิสูจน์ว่า T1I=IZ”

    • คำอธิบายนี้ดูไม่ค่อยถูกนัก การค้นหาแบบ brute force ไม่ได้ทำโดย Transformer แต่ทำโดยตัวแก้เชิงสัญลักษณ์ เมื่อไม่มีข้ออนุมานใหม่ออกมาอีก ก็ให้ Transformer เสนอการสร้างเรขาคณิตเสริมที่เป็นไปได้ ไม่ได้เพิ่มแบบสุ่ม
    • ผมไม่เข้าใจว่าทำไมถึงมองว่านี่ห่างไกลจากภาพทั่วไปของการให้เหตุผลอัตโนมัติ/ปัญญา การให้เหตุผลโดยพื้นฐานคือปัญหาการค้นหา
      กระบวนการที่อธิบายมานั้นตรงกับสิ่งที่มนุษย์ทำเป๊ะ ๆ คือเดาสิ่งที่ดูน่าจะมีประโยชน์ แล้วลองคลี่รายละเอียดเชิงกลดู ถ้าตันก็เดาใหม่ สุดท้ายมันก็คล้ายการค้นหาบนต้นไม้
      คนเรารู้กระบวนการนี้มาตั้งแต่ปี 1955 แล้ว และยังสร้างต้นแบบที่ใช้งานได้ซึ่งพิสูจน์ทฤษฎีบทได้ด้วย: https://en.wikipedia.org/wiki/Logic_Theorist หัวใจสำคัญอยู่ที่การใช้ heuristic ที่ดี โครงข่ายประสาทสามารถดึง heuristic จากข้อมูลได้ จึงมีความหมายในจุดนี้
      ผมเลยสงสัยว่าภาพทั่วไปของ “การให้เหตุผลอัตโนมัติ” ที่คุณนึกถึงคืออะไร เป็นอุปกรณ์วิเศษที่แก้ปัญหาอะไรก็ได้ใน linear pass เดียวหรือ?
    • วิธีแบบ “ถ้าการค้นหาแบบ brute force ล้มเหลว ก็เพิ่มการสร้างเรขาคณิตเสริมอย่างการเพิ่มจุดกึ่งกลาง แล้วดูว่าค้นหาต่อได้ไหมด้วยวัสดุที่เพิ่มมา” นี่เหมือนเรขาคณิตที่ผมเรียนในโรงเรียนเป๊ะ และผมเกลียดมันมาก
      กว่าจะเข้าเรียนภาควิชาคณิตศาสตร์ในมหาวิทยาลัย ผมถึงได้เรียนวิธีที่ถูกต้องและเริ่มสนุกกับมัน
    • การใช้ LLM มารับบทวาดเส้นช่วยนั้นไม่มีประสิทธิภาพเอามาก ๆ ยากจะนึกภาพว่าต้องทุ่มเครื่องจำนวนมากเพื่อแก้โจทย์ IMO ง่าย ๆ
      สาขานี้ยังอยู่ช่วงเริ่มต้นมาก และดูเหมือนยังมีงานที่ทำไม่เสร็จอีกเยอะ ส่วนการค้นหาควรถูกแทนที่ด้วยโครงข่ายประสาทขนาดเล็ก และส่วนการให้เหตุผลก็ไม่ยากนักและดูไม่จำเป็นต้องปรับปรุงมาก
      ตอนนี้ถึงเวลายกระดับประสิทธิภาพด้วย self-play แล้ว โดยในโจทย์เรขาคณิตระนาบ เราอาจมองข้อสรุปที่ต้องพิสูจน์เป็นจุดหนึ่งบนรูป และมองเงื่อนไขเป็นอีกจุดหนึ่ง แล้วให้ผู้เล่นสองฝ่ายเคลื่อนเข้าหากันให้มากที่สุดพร้อมแบ่งปันข้อมูลกัน ระหว่างทางก็ใช้ส่วนร่วมของผู้เล่นแต่ละฝ่ายไปปรับปรุงประสิทธิภาพ โดยเทียบกับการคิดแพ้ชนะในเกมโกะ

  • แม้โมเดลเฉพาะตัวนี้จะยังดูไม่ค่อย generalize ได้ แต่ แนวทางประสาน neural-symbolic ดูมีอนาคตมาก
    มันคือการเชื่อมเครื่องมือ “System 1” ที่ทรงพลังขึ้นเรื่อย ๆ ซึ่งตอนนี้กินพื้นที่ส่วนใหญ่ของแมชชีนเลิร์นนิง เข้ากับเครื่องมือ “System 2” ที่มีโครงสร้าง เช่น การสร้างบทพิสูจน์เชิงตรรกะ โดย System 2 สามารถวางแผนและตรวจสอบความจริงหรือคุณค่าของผลลัพธ์ได้
    ให้ System 2 เดินหน้าต่อไปจนติดขัด แล้วเมื่อมันตัน System 1 ก็เสนอการเดาแบบสัญชาตญาณว่าควรตรวจส่วนใดของ state space ต่อ
    ในที่นี้พวกเขาใช้ข้อเท็จจริงที่ว่าคอมพิวเตอร์สามารถสร้างบทพิสูจน์ได้ มาสร้างชุดข้อมูลบทพิสูจน์ 100 ล้านรายการ และทำให้การเรียนรู้แบบ self-supervised ที่ขยายขนาดได้เป็นไปได้ โดเมนเชิงสัญลักษณ์ดูเหมือนจะเอื้อต่อการสร้างข้อมูลแบบนี้ แม้มูลค่าของแต่ละอินสแตนซ์จะต่ำ แต่เมื่อรวมกันอาจทำให้ pretraining ที่มีประโยชน์เป็นไปได้
    เมื่อนำองค์ประกอบเหล่านี้มารวมกัน นี่จึงเป็นแนวทางที่อาจไปได้ไกลทีเดียว
    หลักไมล์สำคัญคือการหลุดพ้นจากความจำเป็นที่ต้องพึ่งพาโดเมนเชิงรูปแบบ/เชิงสัญลักษณ์เฉพาะ และสร้างระบบ pretraining ที่ทำให้เทคนิคที่เรียนรู้ในโดเมนนั้น generalize ได้

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

  • ขอบคุณที่ปล่อย โค้ดและน้ำหนักโมเดล มาพร้อมกับงานวิจัย เท่าที่ผมจำได้ นี่เป็นครั้งแรกที่มีงานวิจัย DeepMind ชื่อดังที่ปล่อยโค้ดสำหรับอนุมานที่รันได้จริงพร้อม checkpoint ถ้ามีกรณีก่อนหน้านี้ก็ยินดีให้ช่วยแก้ไข
    ถึงตอนนี้ผมยังไม่เห็นชุดข้อมูลฝึกหรือโค้ดฝึกตัวอย่างที่ปล่อยออกมา แต่ก็ยังถือเป็นพัฒนาการที่ดีตรงที่อย่างน้อยพวกเขาให้บางสิ่งที่นักวิจัยคนอื่นเอาไปต่อยอดได้ ซึ่งสุดท้ายแล้วนั่นก็คือจุดประสงค์ของบทความวิชาการ

    • น่าเสียดายที่ยังไม่มีชุดข้อมูลด้วย พวกเขาบอกว่าสร้างตัวอย่างสังเคราะห์ 100 ล้านรายการ แล้วตัวอย่างเหล่านี้สร้างด้วย AlphaGeometry เองหรือเปล่า? แล้วโค้ดคัดกรองกับอินพุตตั้งต้นที่ใช้สร้างข้อมูลสังเคราะห์นี้อยู่ที่ไหน?
      ถ้าผมไม่ได้เข้าใจผิด พวกเขาใช้โมเดล t5 ใช่ไหม? อย่างน้อยก็ดูเหมือนใช้คลังคำ SentencePiece ของ t5
      ผมก็อยากรู้เหมือนกันว่าใช้เวลา GPU ไปเท่าไรในการฝึกโมเดลนี้ และใช้พารามิเตอร์การฝึกอะไรบ้าง
      ไม่อยากให้เข้าใจผิดนะ ระบบนี้น่าหลงใหลมาก และแสดงให้เห็นว่าวิศวกรรมเชิงประยุกต์ควรมีหน้าตาแบบไหน ผมแค่อยากรู้รายละเอียดการฝึก ข้อมูลตั้งต้น และวิธีสร้างข้อมูลสังเคราะห์ให้มากกว่านี้

  • สงสัยมากว่าโมเดลภาษาสร้าง construction ที่มีประโยชน์ได้บ่อยแค่ไหน แน่นอนว่าน่าจะดีกว่าสุ่มอยู่แล้ว แต่ไม่รู้ว่ามันต้องโยน construction เป็นพัน ๆ อันกว่าจะเจออันดี หรือว่ามันเสนอสิ่งที่ใช้ได้ในสัดส่วนใกล้เคียงกับผู้เชี่ยวชาญมนุษย์
    ในงานวิจัยบอกว่า “กระบวนการถอดรหัสของโมเดลภาษาจะคืนลำดับที่แตกต่างกัน k ลำดับ ซึ่งอธิบาย auxiliary construction ทางเลือกจำนวน k แบบ ดังนั้นเราจึงใช้คะแนนของแต่ละบีมเป็นฟังก์ชันมูลค่า แล้วทำ beam search บนตัวเลือก k แบบนี้ การตั้งค่านี้ทำให้ parallelize ระหว่างบีมได้ง่ายมาก จึงเร็วขึ้นมากเมื่อมีทรัพยากรคำนวณแบบขนาน ในการทดลองเราใช้ beam size k=512, จำนวนรอบสูงสุด 16, และ branching factor ของแต่ละโหนด หรือก็คือ decoding batch size เท่ากับ 32”
    แต่ก็ยังไม่เข้าใจทั้งหมดว่า 512 กับ 16 แปลงเป็นจำนวน construction ที่เสนอทั้งหมดอย่างไร เขายังบอกด้วยว่าถึงจะตัด beam size และจำนวนรอบสูงสุดลง ประสิทธิภาพก็ลดลงไม่มากนัก นี่หมายความว่าโมเดลจัดอันดับ construction ที่มีประโยชน์ได้ค่อนข้างดีจริง ๆ และต้องใช้เป็นพัน ๆ แบบเฉพาะในโจทย์ที่ยากที่สุดหรือเปล่า?

    • เดาส่วนตัวคือ จุดนี้ชนเข้ากับข้อจำกัดของภาษาและอุปมาแบบมนุษย์-เครื่องอย่างจัง
      ถึงอย่างนั้น ถ้าจะลองสรุปแบบย่อก็เป็น 262,144 แต่ไม่ควรตีความแบบตรงตัว
      เอาต์พุตของฟังก์ชันถอดรหัสคือโทเค็น ซึ่งคร่าว ๆ ก็ประมาณ 3/4 ของหนึ่งคำ แต่สมมติว่าเป็น 1 คำไปเลยก็ได้
      ต่อโทเค็นเอาต์พุตหนึ่งตัว จำนวนโทเค็นที่ถูกพิจารณาคือ beam_size * branching_factor * max_iterations = 512 * 32 * 16 = 262,144
      ลองนับจำนวนคำในวิธีแก้ตัวอย่างได้ที่: https://storage.googleapis.com/deepmind-media/DeepMind.com/B...
      วิธีแก้มีโทเค็นรวม 2289 ตัว และจำนวนโทเค็นที่พิจารณาทั้งหมดคือ 262,144 * 2289 = 600,047,616 ตัว
      ถ้าคิดแบบฝืน ๆ ว่า “จำนวนวิธีแก้ที่พิจารณา” = จำนวนโทเค็นทั้งหมดที่พิจารณา / จำนวนโทเค็นทั้งหมดของวิธีแก้ ก็จะได้ 262,144 ซึ่งก็พอฟังขึ้น เพราะเท่ากับจำนวนโทเค็นที่ดูในแต่ละรอบวนซ้ำ

  • น่าสนใจที่ Transformer ที่ใช้มีขนาดเล็ก ตามงานวิจัยบอกว่าเทรนด้วยค่าตั้งต้นของไลบรารี Meliad และมี 12 ชั้น, embedding dimension 1,024, attention head 8 หัว, และชั้น dense ระหว่าง attention ที่มีมิติ 4,096 ใช้ ReLU activation
    ไม่นับชั้น embedding ของ input และ output head แล้ว Transformer ทั้งหมดมีพารามิเตอร์ 151 ล้านตัว tokenizer แบบกำหนดเองถูกฝึกด้วยโหมด ‘word’ ของ SentencePiece และมีขนาด vocabulary 757 จำกัดความยาวบริบทสูงสุดไว้ที่ 1,024 โทเค็น และใช้ relative positional embedding แบบ T5 อีกทั้งยังใช้ sequence packing เพราะมากกว่า 90% ของลำดับมีความยาวต่ำกว่า 200

    • จะว่าเล็กก็คงไม่ค่อยได้ นอกวงการ LLM ถือว่าเป็นขนาดค่อนข้างปกติ เช่น พอ ๆ กับโมเดลภาษาขนาดทั่วไป โมเดลแปลภาษา หรือโมเดลเสียง บางคนก็คงเรียกขนาดนี้ว่าใหญ่ด้วยซ้ำ
    • ผลลัพธ์นี้ชี้ว่าถ้าจัด formalize ได้ดีพอ Transformer อาจยังมี low-hanging fruit ให้เก็บอีกในวิทยาศาสตร์แบบ hard science ดูเหมือนครั้งนี้ไม่ใช่ปัญหาเรื่องสเกล

  • สิ่งที่ใหม่จริง ๆ สำหรับผมคือ ระบบที่ดีที่สุดก่อนหน้านี้ก็แก้โจทย์แบบนี้ได้ตั้ง 10 ข้อ แล้ว ผมเคยได้ยินว่ามี decision algorithm สำหรับปัญหาเรขาคณิตระนาบ แต่ไม่รู้ว่ามันเป็นอัลกอริทึมที่ใช้งานได้จริง พอลองค้นดูก็เจอเอกสารอ้างอิงนี้: http://www.mmrc.iss.ac.cn/~xgao/paper/book-area.pdf

    • ใช่ และส่วนที่ไม่ใช่ neural network ของ AlphaGeometry หรือก็คือองค์ประกอบด้านsymbolic processing และ linear algebra เพียงอย่างเดียว ก็อาจแซงผลงานเดิมที่ดีที่สุดได้ งานหนักส่วนหนึ่งอยู่ในองค์ประกอบที่ไม่ใช่ neural network เหมือนกัน
    • ก็น่าสนใจ แต่ผมคิดว่าถ้าไล่คำนวณแบบ brute force ด้วยสูตรพิกัดแบรีเซนตริกจากหนังสือของ Evan Chen ก็น่าจะแก้โจทย์ IMO ได้ราว 30% บนโน้ตบุ๊กสมัยใหม่ เพราะส่วนใหญ่เป็นโจทย์สามเหลี่ยม

  • ปกติผมพร้อมจะสงสัยกับผลงานประเภทนี้ เพราะมักออกแนว “ไม่เหมือนบทพิสูจน์ของมนุษย์” แต่พอเห็น Evan Chen บอกว่ามันเป็นบทพิสูจน์ที่สะอาดและมนุษย์อ่านรู้เรื่อง ก็เปลี่ยนความคิด
    Evan Chen เป็นบุคคลที่มีชื่อเสียงในชุมชนคณิตโอลิมปิก และยังเป็นผู้เขียนหนังสือเรขาคณิตโอลิมปิกที่มีชื่อเสียงด้วย[1] ดังนั้นครั้งนี้คงต้องยอมรับว่าเครื่องจักรได้พิชิตโจทย์ IMO บางส่วนจริง ๆ
    [1]: https://web.evanchen.cc/geombook.html

    • แต่ในภาคผนวก[1] บทพิสูจน์ทั้งหมดของ IMO P3 ตรง Fig1.f และ Step 26 ดูเหมือนจะมีข้อผิดพลาด เขาบอกว่า ∠GMD = ∠GO2D ซึ่งไม่ถูก ต้องเป็น ∠GMD + ∠GO2D = π มากกว่า ผมพยายามตามตรรกะต่อแต่ตีความ Step 25 ไม่ได้ เลยสงสัยว่าขั้นนี้หลอนขึ้นมาหรือเปล่า
      ถึงอย่างนั้น ไอเดียที่ว่า O2 อยู่บนวงกลมเก้าจุดนั้นถูกต้อง
      แก้ไข: ขอย้อนคำพูด ดูเหมือนเขาจะใช้มุมแบบมีทิศทาง[2] ซึ่งถ้าเป็นแบบนั้นประโยคนั้นก็ถูก
      [1]: https://storage.googleapis.com/deepmind-media/DeepMind.com/B...
      [2]: https://web.evanchen.cc/handouts/Directed-Angles/Directed-An...

  • ที่เกี่ยวข้องกัน https://www.nytimes.com/2024/01/17/science/ai-computers-math... ก็น่าอ่านเช่นกัน
    มาจาก https://news.ycombinator.com/item?id=39030186 และเธรดนั้นมีกำหนดจะถูกรวมเข้ามาที่นี่

  • ที่เกี่ยวข้อง: https://aimoprize.com/
    เป็นเงินรางวัล 10 ล้านดอลลาร์สำหรับโมเดลที่ทำผลงานได้ดีใน IMO