OpenAI-ի Navier-Stokes-ի Lean ապացուցումը չի համընկնում բնական լեզվի տարբերակին, հայտնում են մաթեմատիկոսները

Միջև երկու ապացուցումների անհամապատասխանություն

OpenAI-ն սեպտեմբերի 8-ին հայտարարեց, որ գտել է Navier-Stokes-ի խնդրի լուծումը, որը մաթեմատիկայում ամենահայտնի բաց խնդիրներից մեկն է: Ընկերությունը հրապարակեց ապացուցումը երկու տարբերակով՝ մեկը գրված բնական լեզվով՝ անգլերենի և մաթեմատիկական նշանների համադրությամբ, ինչպես կգրեր մարդ մաթեմատիկոս, իսկ մյուսը՝ գրված համակարգչային լեզվով՝ Lean-ով, որը նախատեսված էր ձևակերպման համար և հնարավորություն է տալիս համակարգչին մեխանիկորեն ստուգել յուրաքանչյուր տրամաբանական պնդում:

Այժմ մաթեմատիկոսների խումբը հայտնում է, որ այս երկու տարբերակները չեն համընկնում միմյանց: Քեմբրիջի համալսարանի Էնդերս Հանսենը և Ֆաբիան Չիրչելը Լոնդոնի King's College-ի Ալեքսանդր Բաստունի հետ միասին հաստատում են, որ OpenAI-ի մոդելը թյուրիմաստորեն թարգմանել է ապացուցումը Lean-ում տեղափոխելիս: Հետազոտները ընդգծում են, որ սա չի նշանակում, թե ապացուցումները սխալ են կամ որ OpenAI-ն չի կարողացել լուծել խնդիրը, սակայն կասկած է առաջացնում՝ կարո՞ղ է միշտ հիմնվել AI-ի կողմից գեներված մաթեմատիկական արդյունքների վրա:

Թուլացված լեմա

Խմբի ապացուցումը վերաբերում է ապացուցման այն մասին, որը կոչվում է լեմա 8.6: Բնական լեզվով գրված ապացուցման մեջ այս մասի համապատասխանեցումը պահանջում է, որ որոշակի արժեք լինի m + 4-ից ցածր, որտեղ m-ն ամբողջ թիվ է: Lean-ի ապացուցման մեջ համարժեք արժեքը պետք է լինի m + 5-ից ցածր, ինչը մաթեմատիկորեն ավելի թուլ է: Երկու պնդումներն էլ կարող են ճիշտ լինել, բայց տարբեր բան են ասում, և Lean-ի տարբերակը ավելի շատ հնարավոր պատասխան է տալիս:

Հետազոտների կարծքածությամբ, շեղումը այդպես է տեղի ունենում, որովհետև AI-ն պետք է ստեծի Lean-ի ապացուցում, որը կոմպիլվում է, այսինքն կոդը ամբողջությամբ ինքնուղղված է և սխալներ չի թույլատրում: Եթե մոդելը գտնի մի մաս, որը չի կոմպիլվում, այն փորձելու է գտնել շրջանցող ճանապարհ, նույնիկս եթե դա նշանակում է շեղվել բնական լեզվով գրված ապացուցումից: OpenAI-ն երկու ապացուցումները ներկայացնում է նույնական ձևով և Github-ում հայտարարում է, որ պահոցը պարունակում է աշխատանքում ներկայացված արդյունքների Lean 4 ձևակերպումները:

AI-ի ապացուցումների ստուգման բեռը

Շեղման հայտնաբերումը դժվար էր: Խումբը խնդրեց ChatGPT-ին գտնել երկու տարբերակների միջև հնարավոր անհամապատասխանություններ, այնուհետև ձեռքով ստուգեց դրանցից յուրաքանչյուրը: Շատ առաջարկված անհամապատասխանություններ ստուգումից հետո համոզմունքի ենթարկվեցին: Ընդհանրապես, խումբը իրական շեղման հաստատման համար ծախսեց մոտ երկու շաբաթ, մինչդեռ OpenAI-ի ագենտները ապացուցումների գեներումը տևեց 88 ժամ:

Խնդիրը հատկապես ակտուալ է, քանի որ OpenAI-ն հրապարակեց 722 մաթեմատիկական աշխատանքի խումբ, որոնցից միայն մի մասը ուղեկցվում է Lean-ի ապացուցումներով, որոնք ձեռքով չեն ստուգվել: Լոնդոնի Imperial College-ի Քևին Բազարդը ասաց, որ համոզմած է, որ Navier-Stokes-ի խնդիրը ճիշտ է լուծվել, բայց գերազանց ավելի քիչ համոզմած է, որ PDF-ում նկարագրված ապացուցումը ճիշտ է: Հանսենն ասաց, որ ավելի շատ աշխատանք է անհրաժեշտ կայուն ինքնաձևակերման տեխնիկայի մշակման համար և որ դրա վերջնական ճանապարհը ամբողջությամբ անհայտ է:

Աղբյուրներ: newscientist.com