DEVX
Мэдээ

OpenAI шийдэгдээгүй 700 гаруй математикийн бодлогыг кодчилов: Теренс Тао болон алгоритмчдыг донсолгосон "Lean" хувьсгал

TOGTOKHTOGTOKH·2026 оны арван нэгдүгээр сарын 1·1 үзсэн·
OpenAI шийдэгдээгүй 700 гаруй математикийн бодлогыг кодчилов: Теренс Тао болон алгоритмчдыг донсолгосон "Lean" хувьсгал

Хиймэл оюун ухаан программ бичих, чатлах, контент бүтээх талбарт хүчтэй нэвтэрсэн ч хүний оюун санааны дээд оргил болсон цэвэр онолын математик, нарийн логик баталгааны салбарт ойрын хугацаанд гарч ирж чадахгүй гэж олон хүн итгэж байв. Гэвч энэ хана нурж уналаа.

Хэдхэн хоногийн өмнө OpenAI өөрсдийн хараахан олон нийтэд цацаагүй "frontier" загвараар боловсруулсан, шийдэгдээгүй олон зуун бодлогын хариуг агуулсан openai/math нэртэй албан ёсны GitHub репозиторыг дэлгэсэн юм. Улмаар өнөөдөр манай гаргийн хамгийн нөлөө бүхий математикчдын нэг, Филдсийн шагналт Теренс Тао (Terence Tao) өөрийн алдарт блогтоо профессор Франк Калегаригийн "Mathematics has changed. Let's act like it" нийтлэлийг онцлон тавьсан нь Hacker News болон дэлхийн технологийн нийгэмлэгийг бүхэлд нь шуугиулж эхэллээ.

Энэ үйл явдал яагаад цэвэр математикчдаас гадна нийт программ хангамжийн инженерүүдэд асар том дохио болж байгааг DEVX тоймлон хүргэж байна.

721 судалгааны ажил, 373 бүлэг: GitHub дээр юу нийтлэгдэв?

OpenAI-ийн танилцуулсан датасет болон репозиторт цэвэр хиймэл оюуны загварын бие даан гаргаж авсан 721 эрдэм шинжилгээний гар бичмэл (manuscript) багтжээ. Эдгээр нь тооны онол, алгебр геометр, хагас бүлгийн онол зэрэг орчин цагийн математикийн хамгийн хүнд 373 бүлэг сэдвийг хамарч байна.

Гайхалтай нь эдгээр ажлуудын дунд хэдэн арван жилийн турш математикчдын толгойн өвчин байсан:

  • $\pi$ тооны иррационал экспонент яг 2-той тэнцүү болохыг баталсан ажил,
  • Риманы алдарт таамаглалын (Riemann Hypothesis) хүрээнд $Re(s) > 7/8$ хагас хавтгайд тэгийн утгагүй байх хил хязгаарыг тодорхойлсон Quasi-Riemann үр дүн,
  • Компьютерын ухааны онолын гол суурь болох Exponential Time Hypothesis-ийг няцаасан хэмээн зарласан шинэ баталгаанууд багтсан явдал байв.

Нэг үр дүнг гаргаж авахад AI систем дунджаар 3 цагийн турш тасралтгүй reasoning тооцоолол хийсэн бөгөөд энэ нь хүний судлаачийн олон сар, жилийн хөдөлмөрийг хэдхэн цагт шахаж буй хэрэг юм.

Lean 4: Хиймэл оюуны худлыг (hallucination) шүүх туйлын шүүгч

Энэхүү нийтлэлийн хамгийн анхаарал татах техникийн хэсэг нь ердийн текст биш, харин Formal Verification (Албан хэлбэржүүлсэн шалгалт) байв.

LLM загваруудын хамгийн сул тал нь өөртөө итгэлтэйгээр худал ярих буюу hallucination үүсгэх явдал байдаг. Хэрвээ OpenAI ердөө 700 ширхэг LaTeX файл нийтэлсэн бол эрдэмтэд болон хөгжүүлэгчид үл итгэсэн харцаар харах байлаа. Гэтэл тэд нийт ажлуудынхаа 42 орчим хувийг Lean 4 интерактив баталгааны хэлээр (Theorem Prover / Proof Assistant) бүрэн кодчилж, хөрвүүлэгч (compiler kernel)-ээр амжилттай шалгагдсаныг зарлав.

Lean 4 бол математикийн логик дүрмүүдийг программчлалын хэлний хатуу Type System (төрлийн систем)-тэй хослуулсан хэрэгсэл юм. Хэрэв код Lean дээр алдаагүй хөрвөж л байвал уг математик баталгаа ямар нэг логик алдаагүй, 100% үнэн гэдгийг компьютерын цөм батална.

Энэ нь программ хангамжийн ертөнцөд unit test-ээр хэзээ ч хүрч чаддаггүй "Mathematical Invariant" буюу системийн логик алдаагүй гэдгийг хөдөлшгүй нотлох зарчим билээ.

Теренс Тао ба математикийн нийгэмлэгийн эргэцүүлэл

Уг явдал шинжлэх ухааны салбарт асар хүчтэй шок авчирлаа. Филдсийн медальт, Францын математикч Хюго Дюминил-Копен (Hugo Duminil-Copin): "Миний карьерынхаа турш илтгэл, лекц, судалгааны тэтгэлэгт дурдаж байсан нэг ч томоохон нээлттэй асуудал энэ мэдэгдлээс хоцорсонгүй. Бүгдийг нь шийдчихлээ гэж зарлаж байна" хэмээн халаглажээ.

Харин өнөөдөр Теренс Таогийн блогт нийтлэгдсэн Чикагогийн Их сургуулийн профессор Франк Калегаригийн өгүүлэлд асуудлыг илүү эрүүл ухаанаар харсан байна:

"Өнгөрсөн үеийнхээ араас гашуудах хэрэггүй. Математик нэгэнт өөрчлөгдсөн, одоо үүнийгээ хүлээн зөвшөөрч түүнтэй ажиллах хэрэгтэй. Зарим математикчид тоглоом дууссан гэж харж байхад, өөдрөг үзэлтнүүд тоглоомын дүрэм өөрчлөгдсөнийг олж харж байна. Бидний хайрладаг соёлын зарим зүйлс ард үлдэх нь үнэн. Гэвч бидэнд математикийг судлах урьд хожид үзэгдээгүй хүчирхэг шинэ багаж ирлээ."

Гэхдээ Калегари нэгэн чухал зүйлийг анхааруулсан нь: Lean-ээр баталгаажаагүй үлдсэн 58% судалгааны ажилд ноцтой алдаанууд илэрч эхэлсэн байна. Хиймэл оюуны гаргасан код, логикийг системчилж цэгцлэх, худал үнэнийг нь шүүн тунгаах ажил өмнөхөөс ч чухал болж хувирав.

Программ хангамжийн инженерүүдэд энэ юуг сануулж байна вэ?

Энэхүү математикийн салбарт өрнөж буй хувьсгал нь хөгжүүлэгч бидэнд дараах 3 том сургамжийг өгч байна:

  1. Deterministic Verification бол хиймэл оюуны туйлын хамгаалалт: LLM агентууд асар их хэмжээний код үйлдвэрлэх тусам түүнийг зөв ажиллаж буйг батлах Static Analysis, Formal Specification, хатуу Type Checker хэрэгслүүдийн үнэ цэн тэнгэрт хадна.
  2. "Хэрэгжүүлэгчээс" "Архитектор" руу: Математикчид өдөржин тооцооны томьёо гараараа сараачдаг цаг дуусч, бодлогын үндсэн концепц, хил хязгаарыг томьёологч болж буй шиг хөгжүүлэгчдийн ажил ч өдөр тутмын CRUD код бичихээс системийн архитектур, логик инвариантуудыг тодорхойлоход шилжиж байна.
  3. Хяналтгүй өгөгдлийн үер: OpenAI 700 ажлыг гэнэт нийтэлсэн нь багийн гишүүн тань нэг дор 500 Pull Request зэрэг оруулж ирээд "Шалгаад өг" гэж тулгасантай ижил нөхцөлийг шинжлэх ухаанд үүсгэв. Автомат үүсгэгдсэн логикийг бодит амьдрал дээр найдвартай ашиглах "Governance" систем хамгийн чухал салбар болох нь тодорхой байна.

Шинжлэх ухаан, технологийн ертөнцөд дүрэм өөрчлөгдлөө. Одоо түүнийг үгүйсгэх бус, шинэ хүчирхэг баталгаажуулалтын системүүдийг өөрсдийн өдөр тутмын хөгжүүлэлтийн паттерндээ хэрхэн нэвтрүүлэх талаар бодох цаг болжээ.

Эх сурвалж:

#AI#OpenAI#FormalVerification#Lean4#SoftwareEngineering#Logic

Сэтгэгдэл

Ачаалж байна...