OpenAI-ի Astra մոդելը 2000 դոլարով լուծել է 10 բարդ մաթեմատիկական խնդիր

Շաբաթ օրը OpenAI-ը բացահայտեց, որ իր ներքին Astra մոդելը նոր արդյունքներ է տվել մաթեմատիկայի և տեսական համակարգչային գիտության 10 խնդիրների վերաբերյալ, որոնք առնվազն մեկ տասնամյակ մնացել էին չլուծված՝ հրապարակելով մեքենայական ստուգման ենթակա ապացույցներ յուրաքանչյուր պնդման հետ միասին: Ընկերությունը հայտնել է, որ բոլոր 10 լուծումների համար ընթացիկ API սակագներով տոկենների ծախսը կազմել է մոտ 2000 դոլար:forbes+1

Հաստատված ապացույցներ տարբեր ոլորտներում

Արդյունքները ընդգրկում են բարձր չափողականության ոլորտների փաթեթավորումը, կոդավորման տեսությունը, կրիպտոգրաֆիան, ծայրահեղ կոմբինատորիկան և քվանտային խաղերի տեսությունը: Հիմնական արդյունքը ոչ սոֆիկ խմբի բացահայտ կառուցումն է, որը 1999 թվականից ի վեր բաց հարց էր և հերքում է այն վարկածը, թե բոլոր հաշվելի խմբերը սոֆիկ են: Astra-ն նաև հերքել է Կոննեսի կոշտության վարկածը (1980 թ.) և լուծել Պոլ Էրդյոշի կատալոգից երեք խնդիր, ներառյալ 183-րդ խնդիրը բազմագույն Ռամսեյի թվերի վերաբերյալ:newscientist+1

OpenAI-ը GitHub-ում հրապարակել է 249 էջանոց ձեռագիր և Lean 4 ապացույցների սերտիֆիկատներ Apache 2.0 լիցենզիայի ներքո՝ հայտնելով «sorry»-ների զրոյական քանակի մասին, ինչը նշանակում է, որ ոչ մի քայլ ֆորմալացված ապացույցում անապացույց չի մնացել: Lean միջուկը տալիս է երկուական վճիռ՝ ապացույցը կամ կոմպիլացվում է, կամ ոչ, ինչը վերացնում է մոդելի արդյունքներին հավատալու անհրաժեշտությունը:siliconangle+1

Թոմաս Բլումը, որը վարում է Էրդյոշի խնդիրների կատալոգը, արդյունքները անվանել է «մեծ նորություն» և դրանք ավելի բարձր է գնահատել, քան մայիսին OpenAI-ի նախորդ մոդելի կողմից ստացված Էրդյոշի միավոր հեռավորության հակաօրինակը: Լոնդոնի Քուին Մերի համալսարանի Աբհիշեկ Սահան ասել է, որ 10 լուծումներից յուրաքանչյուրը «կլիներ նշանակալի և տպավորիչ ձեռքբերում»:newscientist+1

Սկեպտիկները զգուշության կոչ են անում

Հայտարարությունը սուր քննադատության արժանացավ: Արհեստական բանականության հայտնի սկեպտիկ Գերի Մարկուսը թողարկումը նկարագրել է որպես «զարմանալի, բայց չափազանցված»՝ պնդելով, որ ֆորմալ ստուգելի մաթեմատիկայում հաջողությունը չի տարածվում այն ոլորտների վրա, որտեղ ստուգումն ավելի դժվար է: Նա նշել է, որ 2000 դոլարի ցուցանիշը ներառում է միայն հաջող փորձերը և բացառում է այն մաթեմատիկոսների և համակարգչային գիտնականների աշխատավարձերը, որոնք օգնել են պատրաստել աշխատանքները:garymarcus.substack

Քեմբրիջի համալսարանից Ֆրանչեսկո Ֆուրնիե-Ֆաչոն կասկածի տակ է դրել աշխատանքի թափանցիկությունը՝ պնդելով, որ սոֆիկության լուծումը մեծապես հիմնված է Անդրեաս Թոմի և Գաբոր Կունի 2016 և 2019 թվականների նախորդ աշխատանքների վրա: OpenAI-ի սկզբնական պնդումը, թե 10 խնդիրներից ոչ մեկում «առնվազն մեկ տասնամյակ հիմնական արդյունքի մասով առաջընթաց չի եղել», ուղղվել է Ֆուրնիե-Ֆաչոյի բողոքից հետո:newscientist

Ավելի լայն հետևանքներ

Astra-ն ինքնին մնում է չթողարկված: OpenAI-ը այն նկարագրում է որպես մոդելների ընտանիք, որը կառուցված է երկարատև առաջադրանքների ընթացքում բազմաթիվ գործակալների համակարգման համար: Գործադիր տնօրեն Սեմ Ալթմանը մոդելը ցուցադրել է Վաշինգտոնի քաղաքական գործիչներին, սակայն ընկերությունը չի հայտարարել թողարկման ամսաթիվը կամ այն, թե արդյոք այն կթողարկվի որպես GPT-6 կամ այլ տարբերակ:siliconangle

Ժամանակագրությունը համընկնում է մաթեմատիկական հանրության կողմից ԱԲ ընկերությունների դեմ ուղղված հակազդեցության հետ: Հունիսին Մաթեմատիկոսների միջազգային միությունը հավանություն տվեց Լեյդենի հռչակագրին՝ զգուշացնելով, որ ԱԲ ընկերությունները «օգտագործում են հրապարակված հետազոտությունները առանց համաձայնության, շրջանցում են գործընկերային վերանայումը և սպառնում են ապացույցների և վերագրման ամբողջականությանը»:siliconangle