OpenAI 10,000 AI агентын хүчээр математикийн "Мянганы бодлого"-ыг бодсоноо зарлалаа: Lean баталгаа ба дата маргаан
Хиймэл оюуны салбарт өнгөрсөн хэдэн жил кодын синтакс үүсгэх, boilerplate код автоматаар бичих хэмжээнд эргэлдэж байсан бол өнөөдөр хүн төрөлхтний шинжлэх ухааны хамгийн хүнд сорилтуудын нэгийг бие даан давсан тухай сенсаци дэгдлээ.
OpenAI компани алдарт Клэйн математикийн хүрээлэнгээс (Clay Mathematics Institute) зарласан 1 сая ам.долларын шагналтай 7 "Мянганы бодлого"-ын нэг болох Навье-Стоксын тэгшитгэлийн оршин байх ба гөлгөр чанарын асуудал (Navier–Stokes existence and smoothness problem)-ыг AI систем ашиглан бүрэн шийдсэнээ албан ёсоор зарлалаа.
Энэхүү шийдэл нь зүгээр нэг LLM-ийн текстийн таамаглал бус, 165 хуудас бүхий математик нотолгоо төдийгүй Lean интерактив теорем батлагч (interactive theorem prover) дээр машин өөрөө алхам бүрийг нь шалгаж баталгаажуулсан төсөл болсноороо түүхэн үйл явдалд тооцогдож байна.
90 жилийн турш толгой гашилгасан "Навье-Стокс" гэж юу вэ?
19-р зуунд томьёологдсон Навье-Стоксын дифференциал тэгшитгэл нь шингэн ба хийн хөдөлгөөнийг (онгоцны далавч тойрсон агаарын урсгалаас эхлээд далайн давалгаа, агаар мандлын хуйлрал хүртэл) загварчилдаг физикийн суурь багана юм.
Гэвч 90 гаруй жилийн турш математикчид нэгэн фундаментал асуултад хариулж чадаагүй байв: Гөлгөр (smooth), тасралтгүй анхны нөхцөлтэй шингэний урсгал цаг хугацааны явцад ямагт гөлгөр хэвээр үлдэх үү, эсвэл тодорхой хугацааны дараа хурд, даралт нь хязгааргүй рүү тэмүүлж, тэгшитгэл "дэлбэрэх" буюу сингуляр чанар (finite-time blowup / singularity) үүсэх үү?
OpenAI-ийн танилцуулсан судалгаагаар, гурван хэмжээст Навье-Стоксын тэгшитгэл нь төгсгөлөг хугацаанд заавал сингуляр чанар үүсгэдэг болохыг тогтоосон байна. Өөрөөр хэлбэл, тодорхой нөхцөлд шингэний урсгалын тэгшитгэл хүчингүй болж, математикийн утгаараа "дэлбэрэлт" явагддаг болохыг баталжээ.
10,000 AI агент ба 88 цагийн тооцоолол
Энэхүү ололт нь дан ганц нэг загварт prompt өгөөд гарч ирсэн үр дүн биш юм. OpenAI-ийн мэдээлснээр уг даалгаврыг гүйцэтгэхийн тулд саяхан танилцуулагдсан GPT-6 Astra-аас ч илүү хүчин чадалтай дараагийн үеийн дотоод суурь загварыг дайчилжээ.
Архитектурын онцлох үзүүлэлтүүд:
- 10,000 бие даасан AI агент: Нэг дор зэрэг ажиллах 10 мянган агентын сүлжээ үүсгэж, тэдэнд бодлогын дэд салбарууд, контр-жишээ (counterexample) хайх, гипотез турших, мухардалд орсон замуудыг шүүх үүрэг хуваарилсан байна.
- 88 цагийн тасралтгүй ажиллагаа: Агентууд нийт 88 цагийн дотор олон мянган математик загварыг туршиж, алдаагаа засварласаар эцсийн 165 хуудас баталгааг нэгтгэжээ.
- Lean кодчилол: AI загварууд хамгийн их шүүмжлүүлдэг зүйл бол "хий үзэгдэл" (hallucination) билээ. Тэгвэл энэ удаад систем өөрийн бүх баталгааг Lean 4 хэл дээр албан ёсны математик код болгон хөрвүүлж, компилятор/шалгагч системээр алхам алхмаар нь математикийн логик алдаагүй болохыг 100% баталгаажуулсан байна.
OpenAI үүнийг баталгаажуулах Lean кодын репозитор болон эрдэм шинжилгээний гар бичмэлийг бүх нийтэд нээлттэй байршуулжээ. Мөн Клэйн хүрээлэнгийн 1 сая ам.долларын шагналыг авах хүсэлт гаргахгүй гэдгээ мэдэгдсэн байна.
Шинжлэх ухааны ёс зүй ба "Codex-ийн өгөгдөл хулгайлсан уу?" гэх маргаан
Хэдийгээр энэ нь шинжлэх ухааны гайхалтай ялалт шиг харагдаж байгаа ч зарлагдсан даруйдаа эрдэмтдийн дунд асар том шуурга дэгдээв.
Нью-Йоркийн Их Сургуулийн (NYU) профессор Тристан Бакмастер (Tristan Buckmaster) болон Anthropic-ийн судлаач Левент Алпоге (Levent Alpoge) нар яг энэ чиглэлээр сүүлийн саруудад судалгаа хийж байсан бөгөөд судалгааны төслөө боловсруулахдаа OpenAI-ийн Codex хэрэгсэл болон Anthropic Claude-ийг өргөнөөр ашиглаж байжээ.
Бакмастер өөрийн цахим хуудсаараа дамжуулан:
"Бид ажлынхаа бүх ноорог, код, Lean формализмыг OpenAI-ийн Codex сесс дээр байршуулж ажиллаж байсан. OpenAI яг манай судалгааны аргын дагуу, маш богино хугацаанд энэхүү баталгааг хийснээ зарлалаа. Би хэнийг ч шууд буруутгахгүй ч, тэд манай хаалттай сессийн өгөгдлийг моделио сургах болон агентдаа чиглүүлэгч болгож ашигласан эсэх талаар тодорхой хариулт авч чадсангүй" гэж мэдэгдсэн нь асуудлыг хурцатгав.
Үүний хариуд OpenAI-ийн тэргүүлэх судлаач Себастьян Бубек (Sébastien Bubeck) компани Бакмастер болон Алпоге нарын нийтлэгдээгүй бүтээлийг ашиглаагүй, өөрсдийн бие даасан баталгааг гаргасан гэж няцаав. Гэвч OpenAI-ийн хэвлэлийн алба хэрэглэгчийн бүтээгдэхүүн ашиглалтын анонимжуулсан телеметр эсвэл дата загварыг сайжруулахад шууд бусаар нөлөөлсөн байхыг "бүрэн үгүйсгэх боломжгүй" гэдгийг хүлээн зөвшөөрсөн байна.
Хөгжүүлэгчид, инженерүүдийн хувьд энэ нь ямар ач холбогдолтой вэ?
Энэхүү үйл явдал нь зөвхөн цэвэр математикийн хүрээний яриа биш бөгөөд программ хангамжийн ирээдүйд хэд хэдэн чухал дохио өгч байна:
-
Formal Verification (Албан баталгаажуулалт) гол тренд болно:
LLM-ийг зүгээр л текст таах биш, Lean эсвэл Coq зэрэг formal хэлнүүдтэй хослуулснаар AI-ийн гаргасан үр дүнг математикийн нарийвчлалтайгаар баталгаажуулж болдгийг энэ жишээ харууллаа. Удахгүй үйлдлийн системүүдийн цөм (kernel), криптографийн протоколууд, критик санхүүгийн системүүдийг 10,000 агентын тусламжтайгаар 100% цоорхойгүй, алдаагүй гэдгийг Lean хэлбэрээр баталгаажуулах үе ирж байна. -
Swarm Intelligence ба Олон агентын архитектур:
Нэг том загварт бүх ачааллыг даатгах бус, нарийн зааглагдсан үүрэгтэй 10,000 жижиг дэд агентуудыг олон хоногоор тасралтгүй оркестрчлох загвар нь нарийн төвөгтэй төслүүдийг шийдэх хамгийн үр дүнтэй арга гэдгээ баталлаа. -
Хувийн кодын нууцлал (IP Leakage) хамгийн том асуудал:
Бакмастерт тохиолдсон шиг хөгжүүлэгчид болон стартапууд өөрсдийн шинэ архитектур, өвөрмөц алгоритмын нооргийг cloud дээрх AI туслахуудад оруулж байгаа бол тухайн компани таны өгөгдлийг ашиглан танаас өрсөж бүтээгдэхүүн гаргах эрсдэл бодитой болсныг харуулж байна. Энэ нь цаашид дотоод сүлжээндээ ажилладаг (self-hosted / local) AI загваруудын эрэлтийг улам бүр өсгөх нь тодорхой.
Математикийн хамгийн том оньсого тайлагдсан эсэхийг дэлхийн математикчид ойрын саруудад нарийвчлан шалгаж эцэслэн зарлах болно. Гэхдээ нэг зүйл тодорхой: хиймэл оюун шинжлэх ухааны шинэ хуудсыг аль хэдийн нээжээ.
Эх сурвалж:
- OpenAI Research: "On the Navier–Stokes Millennium Prize Problem" (September 8, 2026)
- The Verge / Financial Times: "OpenAI claims to have solved maths problem that stumped humans for decades"
- TNW & Axios Tech Analysis on Buckmaster-OpenAI Lean Proof Controversy
Сэтгэгдэл
Ачаалж байна...