OpenAI อ้าง AI ไขโจทย์คณิตศาสตร์กว่า 700 ข้อได้ในคำสั่งเดียว

หมัดเด็ดคณิตศาสตร์จาก OpenAI

ลองจินตนาการว่าคุณส่งโจทย์คณิตศาสตร์ให้ AI แค่ข้อเดียว แล้วลุกเดินออกไปสัก 3 ชั่วโมง พอกลับมาก็ได้บทพิสูจน์ทางคณิตศาสตร์ชิ้นใหม่เอี่ยมเรียบร้อยแล้ว นั่นคือสิ่งที่ OpenAI อ้างว่าทำได้สำเร็จครับ

บริษัท AI ยักษ์ใหญ่รายนี้เพิ่งเปิดเผยงานวิจัยคณิตศาสตร์ 722 ฉบับบน GitHub ทาง OpenAI บอกว่าเอกสารเกือบทั้งหมดมาจากโมเดล AI ตัวใหม่ที่ยังไม่เปิดตัว ซึ่งตอบสนองต่อคำสั่งเพียงคำสั่งเดียว แม้จะฟังดูเหมือนการก้าวกระโดดครั้งใหญ่ทางเทคโนโลยี แต่นักคณิตศาสตร์ระดับท็อปหลายคนกลับมองว่า ต้องขอเห็นหลักฐานมัดแน่นก่อนจะปักใจเชื่อครับ

เจาะลึกตัวเลขเบื้องหลัง

การจะเข้าใจเรื่องนี้ ต้องย้อนดูวิธีที่ OpenAI รวบรวมผลลัพธ์ครับ พวกเขาไม่ได้แค่แก้โจทย์เดี่ยวๆ 722 ข้อ แต่จัดกลุ่มงานวิจัยออกเป็น 372 กลุ่มผลลัพธ์

โดยในหนึ่งกลุ่มอาจรวมทฤษฎีบทหลัก ข้อสนับสนุน บทพิสูจน์ทางเลือก หรือข้อสรุปทางตรรกะไว้ด้วยกัน และนี่คือขั้นตอนที่เกิดขึ้นครับ:

• OpenAI ป้อนโจทย์คณิตศาสตร์ที่ยังไม่มีใครแก้ได้ประมาณ 4,000 ข้อ เข้าไปยังโมเดล AI ภายในของตัวเอง
• ทีมงานคัดเลือกและตีพิมพ์เฉพาะผลลัพธ์ที่พวกเขามองว่ามีนัยสำคัญเท่านั้น
• โดยเฉลี่ยแล้ว แต่ละผลลัพธ์ใช้พลังประมวลผลการคิดของ ChatGPT Pro ราวๆ 3 ชั่วโมง

กระบวนการนี้ต่างจากการทดลองก่อนหน้าของ OpenAI ในโจทย์ Navier-Stokes อย่างมาก โครงการนั้นต้องใช้เอเจนต์ AI ร่วมมือกันถึง 10,000 ตัว ทำงานต่อเนื่องนาน 88 ชั่วโมง

ทำไมนักคณิตศาสตร์ถึงขอดูหลักฐาน?

แม้ข่าวจะพาดหัวน่าตื่นเต้น แต่นักวิจัยหลายคนเตือนให้ระวังจนกว่าผู้เชี่ยวชาญอิสระจะได้ทดสอบ AI ด้วยตัวเอง Andrew Sutherland นักคณิตศาสตร์จาก MIT ให้สัมภาษณ์กับ Scientific American ว่า การอ้างว่าแก้โจทย์ได้ด้วยคำสั่งเดียวจะยังไม่ได้รับการยืนยัน จนกว่าจะเปิดปล่อยโมเดลออกมาสู่สาธารณะ

ตราบใดที่ยังไม่มีการปล่อยโมเดลให้คนอื่นลองทำซ้ำเพื่อพิสูจน์ผลลัพธ์ ผมคิดว่าเราควรจัดว่าข้ออ้างเรื่องการแก้โจทย์ในครั้งเดียวด้วยเอเจนต์เดี่ยวยังไม่ผ่านการตรวจสอบ เราจึงควรเรียกร้องขอหลักฐานที่ชัดเจนก่อน

ประเด็นใหญ่อยู่ที่การตรวจสอบครับ เพราะงานวิจัยเพียง 162 จาก 722 ฉบับ หรือประมาณ 22% เท่านั้นที่ผ่านการตรวจสอบด้วย Lean ซึ่งเป็นซอฟต์แวร์เฉพาะทางที่ใช้ตรวจสอบขั้นตอนทางตรรกะแบบอัตโนมัติ

แม้แต่ OpenAI เองก็ยอมรับว่าเอกสารที่ยังไม่ถูกแปลงเป็นรูปแบบทางการอาจมีข้อผิดพลาดได้ การผ่านการตรวจสอบจาก Lean ช่วยยืนยันว่าตรรกะทางคณิตศาสตร์ถูกต้องตามโค้ด แต่มันไม่ได้พิสูจน์ว่าข้อความนั้นตรงกับโจทย์เดิม หรือเป็นการค้นพบที่มีประโยชน์จริงๆ

คณิตศาสตร์แปลกประหลาด และคลังข้อมูลที่ถูกล็อค

พอเริ่มมีการตรวจเอกสาร นักวิจัยบางคนก็พบว่าตรรกะของ AI ดูน่าฉงน Dmitry Rybin ได้ดูบทพิสูจน์เรื่อง Chromatic Number of a Plane และอธิบายว่าเป็น คณิตศาสตร์ของเอเลี่ยน ที่คาดไม่ถึง เพราะมีขั้นตอนแปลกๆ ที่ไม่มีใครคาดคิด

คนอื่นๆ ชี้ให้เห็นถึงปัญหาในการใช้งานคลังข้อมูล GitHub ของ OpenAI Keith Adler นักคณิตศาสตร์ พยายามนำบทพิสูจน์ Saxl's Conjecture มาแปลงเป็นภาษา Lean 4 แต่พบว่า OpenAI ปิดช่องทางแจ้งปัญหา (Issues) และการส่งการแก้ไข (Pull Requests) ไว้

หากคุณตีพิมพ์งานวิจัย 722 ฉบับ แล้วขอให้คนอื่นช่วยแปลงเป็น Lean คุณก็ควรมีพื้นที่ให้ผู้คนส่งงานกลับมาด้วย

การค้นพบครั้งใหญ่ และปัจจัยด้านมนุษย์

สถาบัน Institute for Advanced Study (IAS) ในพริ้นสตัน ชี้ให้เห็นถึงความกังวลในวงกว้างเกี่ยวกับการรับรู้ของมนุษย์ในวิทยาศาสตร์ยุคใหม่ โดย IAS ระบุในแถลงการณ์ว่า AI สามารถสร้างงานคณิตศาสตร์ซับซ้อนที่มนุษย์ยากจะตรวจสอบหรืออธิบายได้

อย่างไรก็ตาม ศาสตราจารย์ Abhishek Saha มองเหตุการณ์นี้ในแง่ดีกว่า โดยเรียกมันว่า วันสำคัญยิ่งของวงการคณิตศาสตร์ เขาตั้งสังเกตว่าแม้เอกสารส่วนใหญ่จะเป็นความก้าวหน้าที่มั่นคงของปัญหาเดิม แต่มีงานวิจัยชิ้นหนึ่งที่แตะต้องหมุดหมายสำคัญอย่าง Quasi-Riemann Hypothesis

ความโปร่งใส และแนวทางของคู่แข่ง

ความโปร่งใสยังคงเป็นข้อถกเถียงหลัก โดยก่อนหน้านี้ IAS ได้แนะนำให้เปิดเผยรายละเอียดอย่างครบถ้วน รวมถึง:

• ชื่อโมเดล AI ที่แน่นอน
• คำสั่ง (Prompt) เฉพาะที่ใช้
• สรุปกระบวนการคิดตามลำดับตรรกะ (Chain-of-thought)
• เวลาที่ใช้ประมวลผลและต้นทุนการคำนวณที่แม่นยำ

OpenAI ได้ให้ตัวเลขการประมวลผลเฉลี่ยและสรุปเหตุผลสั้นๆ 10 ข้อ แต่ไม่ได้ใส่คำสั่งมาด้วย ในขณะเดียวกัน Daniel Litt นักคณิตศาสตร์จาก University of Toronto มองว่า การแบ่งปันคำตอบคณิตศาสตร์สู่สาธารณะย่อมเกิดประโยชน์ต่อชุมชนอยู่ดี โดยไม่ต้องคำนึงถึงคำสั่ง

ในทางกลับกัน บริษัทคู่แข่งอย่าง Anthropic ใช้แนวทางที่ต่างออกไป Anthropic ปล่อยโค้ด Lean มากถึง 13 ล้านบรรทัดบน GitHub เพื่อตรวจสอบบทพิสูจน์ Fermat's Last Theorem อันโด่งดังของ Andrew Wiles ในปี 1995 โดยมุ่งเน้นที่การพิสูจน์ความสำเร็จของมนุษย์ที่มีอยู่แล้ว มากกว่าการสร้างข้ออ้างใหม่ๆ ที่ยังไม่ได้รับการตรวจสอบ

OpenAI มีแผนจะเพิ่มการแปลงรูปแบบ Lean มากขึ้นเรื่อยๆ ในตอนนี้ ชุมชนนักคณิตศาสตร์จึงยังคงตรวจสอบเอกสาร 162 ฉบับที่ผ่านการตรวจแล้ว พร้อมกับรอคอยการเข้าถึงโมเดลเบื้องหลังอย่างเต็มรูปแบบต่อไป