OpenAI-ն $5 մլն է տալիս ԱԲ ապացույցների անկախ ստուգմանը

2026 թվականի հոկտեմբերի 15-ին OpenAI-ն հայտարարեց $5 մլն հատկացնելու մասին Simons Foundation-ի նախաձեռնությանը՝ օգնելու մաթեմատիկոսներին քննել, հասկանալ և զարգացնել ԱԲ-ի ստեղծած արդյունքները. նույն հրապարակման մեջ ընկերությունը նկարագրեց նաև GitHub-ում տեղադրված իր մաթեմատիկական աշխատանքների մի մասի Lean ձևակերպումները, որոնց տրամաբանական քայլերը հնարավոր է ստուգել համակարգչով։ Գումարը վերաբերում է գիտական քննությանը, իսկ դրամաշնորհների կառավարումն ու հատկացումը ստանձնում է հիմնադրամը։

Նույն օրը Simons Foundation-ի հայտարարությունը ներկայացրեց հիմնադրամի, OpenAI-ի և Anthropic-ի $15 մլն ընդհանուր ֆինանսավորումն ու ռեսուրսները, իսկ հիմնադրամի նախագահ Դեյվիդ Սփերգելը նպատակը ձևակերպեց այսպես՝ «The goal of the program is to support the mathematics community»։ Աջակցությունը նախատեսված է բաց մրցույթի, աշխատաժողովների ու այլ ծրագրերի համար, որտեղ հետազոտողները կգնահատեն վերջերս ստացված արդյունքները և կձևավորեն ԱԲ գործիքների կիրառման ընդհանուր չափանիշներ։

Ով է տնօրինելու գումարը և ինչի համար

Գումարի ծագումն ու բաշխման իրավասությունը տարբեր են։ Ընկերությունը ֆինանսավորում է ծրագիրը, սակայն աջակցություն ստացող առաջարկների ընտրությունն ու դրամաշնորհների հատկացումը կատարելու է գիտական հիմնադրամը։ Այդ կառուցվածքը հնարավորություն է տալիս քննության թեմաները ձևավորել մաթեմատիկական համայնքի ներսում, թեև ֆինանսավորողի մասնակցությունն ինքնին չի փոխարինում հետազոտողների անկախ դատողությանը։ Կոնկրետ նախագծերի որակը կախված կլինի նրանից, թե ովքեր կկատարեն քննությունը, ինչպես կներկայացնեն մեթոդները և որքան բաց կլինեն դրանց արդյունքները։

Միջոցները նախատեսված են նաև գիտաժողովների և հատուկ ծրագրերի համար։ Այդ ձևաչափերում հնարավոր է մեկ ոլորտի մասնագետների եզրակացությունը համադրել այլ ոլորտի մաթեմատիկոսների հարցերի հետ, պարզել օգտագործված ենթադրությունները և վերաշարադրել բարդ փաստարկը հասկանալի լեզվով։ Սա աշխատանքի առանձին տեսակ է. մոդելի առաջարկած պնդումից մինչև գիտական շրջանառության մեջ ընդունելի արդյունք դեռ պահանջվում են բացատրություն, քննարկում և համեմատություն արդեն հայտնի գրականության հետ։ Հատկապես մեծ ծավալով հրապարակումների դեպքում այդ աշխատանքը տարածվում է բազմաթիվ մասնագիտացումների վրա։

Ինչպես են տարբերվում ապացույցի ստեղծումը և ստուգումը

Առաջին փուլում ԱԲ համակարգը կարող է առաջարկել թեորեմի ձևակերպում կամ ապացույցի ընթացք։ Այդ տեքստը հետազոտական արդյունքի հավակնություն է, որի մեջ կարող են լինել թաքնված ենթադրություններ, բաց թողնված քայլեր կամ սխալ հղումներ։ Հաջորդ փուլում մասնագետը պարզում է, թե արդյոք յուրաքանչյուր անցում հիմնավորված է և արդյոք վերջնական պնդումը համընկնում է սկզբնական խնդրի հետ։ Առանց այդ տարանջատման «լուծվել է» ձևակերպումը շփոթում է առաջարկված փաստարկն ընդունված մաթեմատիկական արդյունքի հետ։

Ֆորմալ ստուգումը գործ ունի հստակ լեզվով գրված պնդման և ապացույցի հետ։ Ստուգող ծրագիրը կարող է հաստատել, որ ներկայացված քայլերը հետևում են տվյալ համակարգի կանոններին ու օգտագործված նախադրյալներին։ Այդ հաստատումը արժեքավոր է, որովհետև կարող է բացահայտել ձեռքով ընթերցելիս աննկատ մնացող տրամաբանական բացեր։ Սակայն նույնիսկ ճիշտ ստուգված շարադրանքը կարող է ձևակերպել սկզբնական հարցից ավելի նեղ խնդիր. համապատասխանությունը պետք է որոշի այդ թեմային ծանոթ մաթեմատիկոսը։

Հրապարակված հավաքածուում առկա ֆորմալացված տարբերակները քննության համար հստակ մեկնակետ են, բայց ամբողջ հավաքածուի այդպիսի ծածկույթ հայտարարված չէ։ Ավելին, համակարգչային ստուգումն ինքնուրույն չի որոշում՝ արդյունքը նոր է, նախկինում հայտնի փաստի վերաձևակերպում է, թե տալիս է արդյունավետ նոր մեթոդ։ Այդ հարցերի պատասխանը պահանջում է թեմայի պատմության իմացություն և անկախ մասնագիտական վերանայում։ Հենց այստեղ է դրամաշնորհային ծրագրի հնարավոր դերը՝ ժամանակ և մասնագիտական մասնակցություն հատկացնել այն աշխատանքին, որը միայն ապացույցի գեներացմամբ չի ավարտվում։

Վերարտադրությունը ևս ունի մի քանի շերտ։ Մեկ հետազոտողը կարող է վերագործարկել ֆորմալ ստուգումը, մյուսը՝ նույն եզրակացությանը հասնել ինքնուրույն շարադրանքով, երրորդը՝ գնահատել, թե փաստարկի առանցքային գաղափարն ինչ կապ ունի հարակից խնդիրների հետ։ Այս գործողությունները փոխարինելի չեն. դրանք ստուգում են համապատասխանաբար մեքենայի համար գրված կառուցվածքը, մարդկային ընկալելիությունը և արդյունքի գիտական արժեքը։ Դրանց հրապարակային համադրությունն է թույլ տալիս համայնքին տեսնել, թե կոնկրետ որ պնդումն է հաստատված և որ մասը դեռ քննարկման ենթակա է։

Ինչու են քննարկումներն ու ընդհանուր չափանիշները կարևոր

Ծրագրի նպատակը միայն առանձին ապացույցների ճշտությունը գնահատելը չէ։ Երբ մեծ թվով արդյունքներ հրապարակվում են միասին, մաթեմատիկոսները պետք է կարողանան հասկանալ՝ որտեղ են գտնվում նախորդ աշխատանքներին հղումները, ինչպես են ուղղվում սխալները և ինչ հիմքով է տվյալ պնդումը համարվում նոր։ Հրապարակված հավաքածուի համար նախատեսված են փոփոխությունների ու մեջբերումների կանոններ, սակայն դրանց գործնական արժեքը երևում է այն ժամանակ, երբ անկախ մասնագետները կարողանում են դրանցով հետևել փաստարկի զարգացմանը։

The Independent-ի անդրադարձը նկարագրում է մաթեմատիկոսների արձագանքը ԱԲ-ով ստեղծված հարյուրավոր աշխատանքների միաժամանակյա հրապարակմանը. առարկություններից մեկը դրանք սովորական գիտական վերանայման ճանապարհով գնահատելու ծանրաբեռնվածությունն է։ Այս համատեքստում աշխատաժողովը միայն արդյունքների ներկայացման վայր չէ. այն կարող է տարբեր փորձագետների մեկտեղել մեկ ապացույցի թույլ ու ուժեղ հատվածները քննելու համար։ Թե որքանով այդ ձևաչափը կթեթևացնի ծանրաբեռնվածությունը, պարզ կդառնա իրականացված ծրագրերի ծավալից և հրապարակած գնահատականներից։

Համայնքային չափանիշները վերաբերում են նաև հրապարակման լեզվին։ Եթե պնդման ձևակերպումը, ապացույցի բնական լեզվով տարբերակը և ֆորմալ տարբերակը իրարից տարբերվում են, պետք է նշվի, թե դրանցից որն է ստուգվել։ Նույնը վերաբերում է վարկածների շրջանակին, նախորդ հետազոտությունների օգտագործմանը և հետագա ուղղումներին։ Մեկ միասնական ձևաչափը պարտադիր չէ բոլոր մաթեմատիկական ոլորտների համար, բայց պարզ նշված տարբերակներն ու ստուգման սահմանները թույլ են տալիս քննարկումը կենտրոնացնել բուն արդյունքի վրա։

Ինչ կտա հետազոտողներին մոդելների հասանելիությունը

Ֆինանսավորմանը կից խոստացված մոդելների ու հաշվողական ռեսուրսների հասանելիությունը աջակցություն ստացող գիտնականներին հնարավորություն կտա ուսումնասիրել, թե ինչպես են ստացվում նման արդյունքները, և փորձարկել գործիքները սեփական հարցերի վրա։ Նախաձեռնության շրջանակը կարող է ընդգրկել նաև հիմնարար գիտության այլ ուղղություններ։ Սա ծրագրի առանձին բաղադրիչ է. գործիքին հասանելիությունը չի հավաստում նրա ստեղծած որևէ կոնկրետ ապացույցի ճշտությունը, իսկ վերջնական գնահատականը պետք է հիմնվի հրապարակված փաստարկի քննության վրա։

Այս պահին հայտնի է առաջարկների բաց մրցույթի և գիտական հանդիպումների մտադրությունը, սակայն առանձին դրամաշնորհների ստացողները, դիմումների ժամկետներն ու ստուգման միասնական ընթացակարգը դեռ հրապարակված չեն։ Ուստի նախաձեռնության ազդեցությունը հնարավոր կլինի գնահատել առաջին ֆինանսավորված նախագծերից՝ հատկապես այն բանից, թե արդյոք դրանք կհրապարակեն քննվող պնդումների ճշգրիտ ձևակերպումները, ստուգման քայլերը և մասնագետների եզրակացությունները։ Այդ հրապարակումները կորոշեն, թե որ ԱԲ արդյունքները կարող են դառնալ հետագա մաթեմատիկական աշխատանքի հուսալի հիմք։

Կարդացեք նաև:

• C2PA պիտակը ցույց է տալիս ծագումը, բայց չի ապացուցում բովանդակության ճշմարտությունը
• Atlassian AMP-ը ԱԲ գործակալին տալիս է ինքնություն և սահմանափակ լիազորություն
• OpenAI Agents SDK թե LangGraph․ արագ մեկնարկը բախվում է վերականգնվող վիճակին