เจาะลึกโจทย์ปัญหา Navier–Stokes Millennium Prize Problem

เราแชร์วิธีแก้โจทย์ปัญหาการมีอยู่และความราบรื่นของ Navier–Stokes ซึ่งเป็นหนึ่งใน Millennium Prize Problems บทพิสูจน์นี้มาจากระบบภายในของ OpenAI และแสดงให้เห็นว่าพลวัตของสมการ Navier–Stokes สำหรับการเคลื่อนที่ของของไหลสามารถเกิดภาวะเอกฐานในเวลาจำกัด พร้อมกันนี้ เรายังแชร์ทั้งบทความอธิบายบทพิสูจน์และการการเขียนบทพิสูจน์อย่างเป็นทางการ ใน Lean ด้วย

Millennium Prize Problems⁠(เปิดในหน้าต่างใหม่) รวบรวมโจทย์ปัญหาที่ยากที่สุดบางข้อซึ่งยังท้าทายนักคณิตศาสตร์มาจนถึงปัจจุบัน หนึ่งในคำถามสำคัญคือ ของไหลที่เคลื่อนที่อย่างราบเรียบในสามมิติจะเกิดภาวะเอกฐานขึ้นได้หรือไม่ ซึ่งเป็นคำถามที่นักคณิตศาสตร์ยังหาคำตอบไม่ได้มานานเกือบ 90 ปี

หนึ่งในเป้าหมายหลักของเราคือการสนับสนุนนักวิทยาศาสตร์ให้สามารถผลักดันงานวิจัยและเทคโนโลยีที่สร้างประโยชน์ให้กับมนุษยชาติได้มากยิ่งขึ้น สำหรับการแก้ปัญหา Navier–Stokes เราใช้โมเดลภายในที่มีความสามารถสูงกว่า GPT‑6 Astra อย่างมาก และเราเชื่อว่าการทำให้ทุกคนได้รับรู้ว่า AI กำลังก้าวหน้าไปอย่างรวดเร็วเพียงใด รวมถึงสิ่งที่คาดหวังได้จากโมเดลรุ่นต่อๆ ไปนั้นเป็นเรื่องสำคัญ

สมการ Navier–Stokes ใช้กฎการเคลื่อนที่ข้อที่สองของนิวตัน (“F=ma”) เพื่ออธิบายการเคลื่อนที่ของของไหล จุดสำคัญคือ สมการเหล่านี้มองของไหลเป็นตัวกลางที่ต่อเนื่อง แทนที่จะติดตามการเคลื่อนที่ของโมเลกุลแต่ละตัว สมการนี้นำไปใช้ในการออกแบบเครื่องบิน การพยากรณ์อากาศ และการศึกษาการไหลเวียนของเลือด

หนึ่งในคำถามพื้นฐานที่ยังหาคำตอบไม่ได้เกี่ยวกับสมการพลวัตเหล่านี้คือ แบบจำลองที่ถือว่าของไหลเป็นตัวกลางต่อเนื่องจะมีจุดที่ใช้ไม่ได้หรือไม่ หรือพูดให้เจาะจงก็คือ แม้การเคลื่อนที่จะเริ่มต้นอย่างราบเรียบ สมการ Navier–Stokes สำหรับของไหลสามมิติที่อัดตัวไม่ได้และมีความหนาแน่นคงที่ จะเกิด “ภาวะเอกฐาน” ขึ้นได้หรือไม่ ภาวะเอกฐานในที่นี้เกิดขึ้นเมื่อความเร็วของของไหลเพิ่มขึ้นอย่างไม่มีขีดจำกัดภายในเวลาจำกัด ทั้งที่มีความหนืดซึ่งช่วยให้การเคลื่อนที่ราบเรียบขึ้น เนื่องจากในความเป็นจริงของไหลไม่สามารถเคลื่อนที่ด้วยความเร็วที่เพิ่มขึ้นอย่างไม่มีขีดจำกัดได้ หากเกิดภาวะนี้ขึ้น ก็หมายความว่าสมการไม่สามารถจำลองพฤติกรรมของของไหลด้วยแนวคิดแบบตัวกลางต่อเนื่องได้อีกต่อไป และหากต้องการจำลองระบบต่อ ก็จะต้องติดตามพฤติกรรมของอนุภาคแต่ละตัวแทน

สมการเหล่านี้มีต้นกำเนิดจากผลงานของ Claude-Louis Navier และ George Gabriel Stokes ในช่วงคริสต์ศตวรรษที่ 19 ต่อมาใน พ.ศ. 2477 Jean Leray พิสูจน์ว่าคำตอบของสมการมีอยู่จริงในความหมายแบบทั่วไป แต่คำถามที่ว่าคำตอบเหล่านั้นจะคงความราบเรียบอยู่เสมอหรือไม่ กลายเป็นหนึ่งในคำถามสำคัญที่ยังไม่มีคำตอบ จนกระทั่งใน พ.ศ. 2543 Clay Mathematics Institute ได้กำหนดให้ปัญหาการมีอยู่และความราบเรียบของ Navier–Stokes เป็นหนึ่งในเจ็ดโจทย์ปัญหา Millennium Prize Problems

ระบบของเราสร้างทั้งบทพิสูจน์เชิงวิเคราะห์และบทพิสูจน์ใน Lean ซึ่งแสดงให้เห็นว่า ของไหลที่เริ่มต้นจากสภาวะหยุดนิ่งและมีความราบเรียบ สามารถเกิดภาวะเอกฐานขึ้นได้ภายในเวลาจำกัด โดยมีแรงภายนอกที่เป็นฟังก์ชันราบเรียบกระทำต่อของไหล และพลังงานของระบบยังคงมีค่าจำกัดตลอดกระบวนการ ตั้งแต่สภาวะหยุดนิ่งไปจนถึงการเกิดภาวะเอกฐาน ผลลัพธ์นี้เป็นคำตอบของปัญหา Navier–Stokes ใน Millennium Prize Problems โดยพิสูจน์ว่าข้อความ “C” (รวมถึง “D”) ในข้อกำหนดอย่างเป็นทางการของ Millennium Prize⁠(เปิดในหน้าต่างใหม่) เป็นจริง

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

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

เมื่อวันอังคารที่ 1 กันยายน เราได้ยินข่าวลือว่ามีโจทย์ปัญหา Millennium Prize Problems สองข้อที่ได้รับการแก้แล้ว ข่าวลือนี้ ประกอบกับความสามารถของโมเดลภายในที่ก้าวกระโดดขึ้นอย่างชัดเจน ทำให้เราเริ่มทดสอบโมเดลกับ Millennium Prize Problems ทุกข้อที่ยังไม่มีคำตอบ พร้อมกับปัญหาอื่นๆ อีกบางข้อที่มีความสำคัญและอาจสร้างผลกระทบในวงกว้าง

เราใช้ระบบที่ให้เอเจนต์หลายตัวทำงานร่วมกัน และขับเคลื่อนด้วยโมเดลภายในของเรา โดยเอเจนต์สามารถใช้เครื่องมือต่างๆ ได้ เช่น อ่านข้อมูลจากอินเทอร์เน็ตเวอร์ชันที่จัดเก็บไว้ในแคชและรันโค้ดได้ เราแบ่งเอเจนต์ออกเป็นกลุ่ม โดยเอเจนต์ภายในแต่ละกลุ่มสามารถสื่อสารกันได้ แต่ละกลุ่มมีจำนวนเอเจนต์แตกต่างกัน และกลุ่มที่ได้คำตอบของปัญหา Navier–Stokes มีเอเจนต์ทำงานพร้อมกันประมาณ 10,000 ตัว ตลอดกระบวนการ เราใช้มาตรการป้องกันที่เข้มงวดเช่นเดียวกับการประเมินโมเดลระดับแนวหน้าทั้งหมดของเรา ซึ่งรวมถึงการเฝ้าติดตามและการแยกระบบ

สำหรับแต่ละโจทย์ปัญหา เราให้เอเจนต์แต่ละกลุ่มลองแก้โจทย์ในรูปแบบที่แตกต่างกัน เพื่อให้ครอบคลุมโจทย์ทุกรูปแบบ สำหรับปัญหา Navier–Stokes เราให้เอเจนต์คนละกลุ่มลองแก้โจทย์ในรูปแบบ “A” และ “B” ซึ่งหากทำสำเร็จจะเป็นการพิสูจน์ว่าข้อความดังกล่าวเป็นจริง และรูปแบบ “C” และ “D” ซึ่งหากทำสำเร็จจะเป็นการพิสูจน์ว่าข้อความดังกล่าวไม่เป็นจริง

นอกจาก Millennium Prize Problems ฉบับเต็มแล้ว เรายังให้ระบบเอเจนต์หลายตัวของเราลองแก้ปัญหาที่ “ง่ายกว่า” อีกชุดหนึ่ง หนึ่งในนั้นเป็นคำถามเรื่องการเกิด blowup ที่คล้ายกัน แต่เป็นกรณีลิมิตของปัญหา Navier–Stokes เมื่อตัดพจน์ความหนืดออก ปัญหานี้เรียกว่าปัญหาความสม่ำเสมอของสมการ Euler และเอเจนต์ของเราก็สร้างความประหลาดใจด้วยการหาคำตอบของปัญหานี้ได้ โดยกรณีที่เอเจนต์แก้ได้คือแบบ ไม่มีแรงภายนอก ซึ่งไม่มีแรงจากภายนอกมากระทำต่อของไหล เอเจนต์เกือบ 100 ตัวทำงานร่วมกันเป็นเวลาประมาณ 50 ชั่วโมง จนได้บทพิสูจน์หักล้างความสม่ำเสมอของ Euler¹

หลังจากเห็นว่าเอเจนต์สามารถแก้ปัญหา Euler ได้ เราคิดว่า Navier–Stokes น่าจะเป็นปัญหาที่มีโอกาสแก้สำเร็จมากที่สุด เราจึงตัดสินใจทุ่มทรัพยากรไปที่ Navier–Stokes โดยย้ายเอเจนต์ที่กำลังทำงานกับ Millennium Prize Problems ข้ออื่นๆ มาช่วยแก้ปัญหานี้ และให้ข้อมูลคำตอบของ Euler แก่เอเจนต์เหล่านั้นเพื่อใช้เป็นแนวทาง ระหว่างที่ดำเนินงาน โมเดลภายในของเราได้รับการฝึกเพิ่มเติมและมีเวอร์ชันใหม่พร้อมใช้งาน เราจึงอัปเดตเอเจนต์ให้ใช้โมเดลเวอร์ชันดังกล่าว

เราสนับสนุนให้เอเจนต์แต่ละกลุ่มลองใช้แนวทางที่หลากหลาย หลังจากทำงานไปได้ระยะหนึ่ง เราใช้ Codex รวบรวมแนวคิดและข้อค้นพบที่เป็นประโยชน์ที่สุดจากแต่ละกลุ่ม แล้วนำมาแบ่งปันให้กลุ่มอื่นๆ เพื่อต่อยอดการทำงาน พรอมต์ในขั้นต่อมาจึงอาศัยผลลัพธ์ระหว่างทางที่เอเจนต์ค้นพบขึ้นมาเอง กลุ่มที่หาคำตอบของปัญหา Navier–Stokes ได้ก็ได้รับแนวทางในลักษณะนี้

เอเจนต์สามารถหาคำตอบได้ในวันเสาร์ที่ 5 กันยายน หลังจากเริ่มให้เอเจนต์ชุดแรกทำงานไปประมาณ 88 ชั่วโมง ส่วนการเขียนบทพิสูจน์อย่างเป็นทางการใน Lean และการตรวจสอบความถูกต้องด้วย GPT‑6 Astra ใช้เวลาเพิ่มอีก 17 ชั่วโมง

ในการลองแก้ปัญหาทั้งหมด เอเจนต์ส่งข้อความรวม 4.9 ล้านข้อความ และใช้โทเค็นเอาต์พุตประมาณ 3 แสนล้านโทเค็น ส่วนการแก้ปัญหา Navier–Stokes เพียงปัญหาเดียว เอเจนต์ส่งข้อความ 2.7 ล้านข้อความ และใช้โทเค็นเอาต์พุตประมาณ 1.3 แสนล้านโทเค็น

เราเริ่มโครงการนี้เมื่อวันที่ 1 กันยายน หลังจากได้ยินข่าวลือซึ่งต่อมาเราจึงทราบว่าเกี่ยวข้องกับ Levent Alpöge พนักงานของ Anthropic และ Tristan Buckmaster ศาสตราจารย์ด้านคณิตศาสตร์ที่ NYU² หลังจากโครงการของเราเสร็จสมบูรณ์และตรวจสอบบทพิสูจน์ด้วย Lean เรียบร้อยแล้วเมื่อวันที่ 6 กันยายน เราเข้าใจจากข่าวลือว่าทั้งสองคนก็มีคำตอบของโจทย์ปัญหา Navier–Stokes เช่นกัน จึงติดต่อไปเพื่อเสนอให้เผยแพร่ผลลัพธ์พร้อมกัน และระบุในประกาศร่วมว่าพวกเขาค้นพบผลงานก่อนเรา แต่เมื่อได้พูดคุยกัน เราจึงทราบว่าพวกเขาใช้โมเดลภายในของ Anthropic และได้คำตอบของปัญหา Euler แบบมีแรงภายนอก ในระหว่างการพูดคุย เราเสนอให้พวกเขาดูพรอมต์ทั้งหมดที่เราใช้ และต่อมาก็เสนอให้ดูบทพิสูจน์ของเราด้วย เราขอยอมรับว่าผลงานของพวกเขาเกี่ยวกับปัญหา Euler แบบมีแรงภายนอกเกิดขึ้นก่อน และขอแสดงความยินดีกับความสำเร็จทางคณิตศาสตร์ที่น่าประทับใจของพวกเขา

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

จากการตรวจสอบ เรายืนยันว่าพรอมต์ที่ Buckmaster ส่งให้ Codex ตลอดช่วงสองเดือนก่อนการประกาศและบทความที่เผยแพร่เมื่อวันที่ 8 กันยายน 2569 ไม่มีทางส่งผลต่อระบบได้ รวมถึงไม่สามารถมีอิทธิพลผ่านกระบวนการฝึกโมเดล โมเดลภายในของ OpenAI ที่ใช้สำหรับผลลัพธ์นี้ได้รับการพัฒนาด้วยการเรียนรู้แบบเสริมกำลังขนาดใหญ่ โดยต่อยอดจากโมเดลที่ผ่านการฝึกล่วงหน้าแล้ว บทพิสูจน์ของทั้งสองฝ่ายก็แตกต่างกันอย่างชัดเจน สำหรับ Euler นั้น Alpöge และ Buckmaster พิสูจน์กรณีที่มีแรงภายนอก ส่วนระบบของ OpenAI พิสูจน์กรณีที่ไม่มีแรงภายนอก

เป้าหมายของการเผยแพร่ผลลัพธ์นี้คือเพื่อให้ทุกคนได้รับรู้ถึงความก้าวหน้าครั้งสำคัญของโมเดล AI ของเรา โดยเราไม่มีความตั้งใจที่จะยื่นขอรับรางวัล Millennium Prize สำหรับผลงานนี้

ความสำเร็จครั้งสำคัญนี้เกิดจากการทุ่มเททำงานอย่างมากของทั้งนักคณิตศาสตร์และนักวิจัย AI อย่างไรก็ตาม นี่ไม่ใช่จุดสิ้นสุด แต่เป็นเพียงภาพสะท้อนว่า ณ เวลานี้ การพัฒนา AI ก้าวหน้าไปถึงไหนแล้ว

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