OpenAI моделі ондаған жыл шешілмеген математикалық сұрақтарға жауап тапты

OpenAI көпшілікке әлі ұсынылмаған Astra атты ішкі моделі математика мен теориялық информатикадағы 10 күрделі мәселе бойынша жаңа нәтиже тапқанын хабарлады. Кейбір сұрақтар ондаған жыл бойы шешілмей келген. Компания дәлелдердің толық мәтінін, олардың қалай табылғанын түсіндіретін жазбаларды және компьютер тексере алатын Lean нұсқаларын жариялады. Бұл туралы OpenAI-дың ресми материалында айтылған.

Компанияның мәліметінше, шешімдерді іздеуге жұмсалған токендер Sol API тарифімен есептегенде шамамен 2000 доллар тұрар еді. Бұл тек модельдің жауап іздеу шығыны. Ғылыми жұмысты дайындау, тексеру және жариялау процесі бұл сомаға кірмейді.

Astra нақты не істеді

Мектептегі есепте дұрыс жауапты табу жеткілікті болуы мүмкін. Ғылыми математикада нәтиже ғана емес, оның неге дұрыс екенін қатаң дәлелдеу қажет.

Astra бұрыннан белгілі формулаларды қолданып дайын есептерді шығармаған. OpenAI мәлімдеуінше, модель шешімі болмаған ғылыми мәселелерге жаңа математикалық идеялар мен дәлелдер ұсынған.

Нәтижелер геометрия, кодтау теориясы, топтар теориясы, кванттық есептеулер, графтар, криптография және күрделі есептердің орындалу шектері сияқты салаларды қамтиды.

OpenAI математикалық дәлелдерді модель жасағанын айтады. Адамдар оларды ғылыми мақала түріне келтіруге көмектескен, ал Astra кейін дәлелдерді Lean жүйесінде формализациялаған.

Lean дәлелдің қатесін қалай тексереді

Lean дегеніміз мәтінді жай оқып шығатын бағдарлама емес. Ол математикалық анықтамалар, ережелер және дәлелдің әр қадамы арнайы тілде жазылған кезде олардың бір-біріне логикалық тұрғыдан сәйкес келетінін тексереді.

Мұны өте қатаң редакторға ұқсатуға болады. Егер дәлелдің арасында негізсіз бір қадам болса немесе алдыңғы тұжырымнан келесі қорытынды шықпаса, жүйе оны қабылдамайды.

Lean сертификаты жарияланған дәлелде қарапайым арифметикалық немесе логикалық қате кету қаупін азайтады. Дегенмен ғылыми қауымдастық қолданылған анықтамаларды, нәтиженің жаңалығын және оның математикадағы орнын бөлек бағалауы керек.

1999 жылдан бері жауапсыз тұрған сұрақ

Жарияланған нәтижелердің ең маңыздысының бірі софикалық емес топтың нақты мысалын құрастыруға қатысты.

Математикадағы «топ» адам тобы емес. Бұл белгілі бір амалдар мен қатаң ережелерге бағынатын объектілер жиыны. Мұндай құрылымдар симметрияны, қозғалысты және күрделі жүйелердің ішкі тәртібін зерттеу үшін қолданылады.

Софикалық топты өте үлкен немесе шексіз жүйенің шағын бөліктерін ақырлы модельдер арқылы жуықтап көрсетуге болатын құрылым деп түсіндіруге болады. Математиктер ұзақ уақыт бойы кез келген саналымды топты осылай көрсетуге бола ма деген сұраққа жауап таба алмады.

Бұл жуықтау қасиетін Михаил Громов 1999 жылы енгізген. Кейін Беньямин Вайсс мұндай құрылымдарды софикалық топтар деп атап, софикалық емес топтың бар-жоғын сұрады.

Astra ұсынған жұмыста ақырлы модельдермен қажетті деңгейде жуықтауға келмейтін нақты топ құрастырылған. Егер дәлел тәуелсіз тексерулерден өтсе, бұл барлық саналымды топтар софикалық болуы мүмкін деген болжамға нүкте қояды.

OpenAI жариялаған 10 нәтиже

1. Көпөлшемді кеңістіктегі шарларды орналастыру. Модель бірдей шарларды өлшем саны өте көп кеңістікке қаншалықты тығыз орналастыруға болатынына қатысты жалпы шекті жақсартты. Ғылыми жұмыста бұл 1978 жылдан бергі алғашқы осындай жақсарту деп көрсетілген.
2. Екілік және сфералық кодтар. Ақпаратты қате жібермей сақтауға және жеткізуге көмектесетін кодтардың мүмкін болатын көлеміне қатысты бұрынғы шектер жақсартылды.
3. Софикалық емес топтар. Ақырлы ауыстырулар арқылы жуықтауға келмейтін топтың нақты мысалы ұсынылды. Бұл топтар теориясындағы орталық сұрақтардың біріне жауап береді.
4. Коннның қатаңдық болжамы. Бұрын фон Нейман алгебрасы белгілі бір математикалық топты бірегей анықтайды деп есептелген. Astra бір алгебраға сәйкес келетін, бірақ бір-біріне ұқсамайтын шексіз көп топ құрастырып, бұл болжамды жоққа шығарды.
5. Арифметикалық схемалардың күрделілігі. Матрицаның перманенті деп аталатын күрделі шаманы есептейтін кейбір алгоритмдік схемалардың міндетті түрде қаншалықты үлкен болуы керектігіне жаңа төменгі шектер табылды.
6. Кванттық ойындарды қайталау. Екі ойыншы қатысатын кванттық ойын бірнеше рет қатар өткізілгенде, барлық кезеңде жеңу ықтималдығының экспоненциалды азаятыны жалпы жағдайда дәлелденді.
7. Ең жақын вектор есебі. Көпөлшемді тордан берілген нүктеге ең жақын элементті табуды жуықтап шешудің өзі қаншалықты қиын екеніне жаңа нәтиже алынды. Бұл мәселе посткванттық криптографиямен байланысты.
8. Эрхарттың көлем туралы болжамы. Орталығы ішкі тордағы жалғыз нүкте болатын дөңес дененің ең үлкен көлемі кез келген өлшем үшін анықталды.
9. Көптүсті Рамсей сандары. Бірнеше түспен боялған күрделі желіден міндетті түрде бір түсті үшбұрыш пайда болатын шекке қатысты жаңа нәтиже Эрдештің №183 мәселесін шешті.
10. Экстремалдық графтар теориясы. Astra арнайы графтар құрастырып, ықшамдық пен дегенерацияға қатысты екі ескі болжамды жоққа шығарды. Нәтиже Эрдештің №146 және №180 мәселелеріне жауап береді.

Бұл нәтиже неліктен маңызды

Жасанды интеллект бұған дейін дайын деректерді талдау, есептеулер жүргізу және белгілі дәлелдерді формализациялау үшін қолданылып келген. Бұл жолы OpenAI жүйе ғылыми әдебиетте дайын жауабы жоқ мәселелерге жаңа дәлелдер ұсынғанын мәлімдеп отыр.

Нәтиже расталса, ЖИ математиктің жұмысын тек жылдамдататын құралдан жаңа гипотеза мен дәлел табуға қатысатын зерттеу көмекшісіне айнала бастағанын көрсетеді.

Бұл математиктердің қажеті болмай қалады деген сөз емес. Мәселені дұрыс қою, нәтиженің маңызын бағалау, басқа теориялармен байланысын табу және дәлелді тәуелсіз тексеру ғалымдардың қатысуын талап етеді.

OpenAI де жарияланған жұмыстарды математикалық қауымдастықтың жан-жақты талқылауына ұсынғанын айтады. Компания дәлелдердің дұрыстығына жауапкершілік алатынын мәлімдеді, бірақ жаңа нәтижелердің ғылымдағы орнын тәуелсіз мамандар анықтайды.

Қазақстандық зерттеушілер үшін мұндай жүйелер күрделі есептерге болжам ұсыну, дәлелдерді формализациялау және ықтимал қателерді табу жұмысын жеделдетуі мүмкін. Алайда Astra әзірге OpenAI-дың ішкі моделі болып саналады, оның көпшілікке қашан және қандай түрде ұсынылатыны хабарланған жоқ.