Anthropic-ի Claude-ը համակարգչային եղանակով ապացուցել է Ֆերմայի վերջին թեորեմը

Anthropic ընկերությունը հինգշաբթի հայտարարեց, որ իր Claude արհեստական բանականության մոդելը ավարտին է հասցրել Ֆերմայի վերջին թեորեմի առաջին համակարգչային ապացույցը, որը մաթեմատիկայի ամենահայտնի արդյունքներից է։ 11 օրվա ընթացքում հիմնականում ինքնուրույն աշխատելով՝ Claude-ը գրել է ապացույցը Lean ծրագրավորման լեզվով՝ ստեղծելով 13 միլիոն տող կոդ և ապացուցելով 29,500 միջանկյալ թեորեմ:anthropic+1

11-օրյա վազք մաթեմատիկայի դարերի միջով

Ֆերմայի վերջին թեորեմը պնդում է, որ ոչ մի դրական ամբողջ a, b և c թվեր չեն բավարարում aⁿ + bⁿ = cⁿ հավասարմանը 2-ից մեծ ցանկացած n ամբողջ թվի համար։ Պիեռ դը Ֆերմայի կողմից մոտ 1637 թվականին առաջ քաշված այս վարկածը ապացուցվել է միայն 1995 թվականին, երբ Էնդրյու Ուայլսը հրապարակեց 129-էջանոց ապացույցը, որի ստուգումը փորձագետներից ամիսներ պահանջեց:anthropic

Այդ ապացույցի ֆորմալացումը՝ այնպես վերաշարադրելը, որ համակարգիչը կարողանա ստուգել յուրաքանչյուր տրամաբանական քայլ, ակնկալվում էր, որ տարիներ կպահանջի։ Լոնդոնի Իմպերիալ քոլեջի մաթեմատիկոս Քևին Բազարդը, որը ղեկավարում էր Lean-ի միջոցով Ֆերմայի թեորեմը ֆորմալացնելու անկախ նախագիծը, հաստատել է, որ կոդը աշխատում է և ճիշտ է։ Ուրբաթ օրը իր բլոգում Բազարդը այն անվանել է «արտակարգ ավտոֆորմալացման նվաճում» և նշել, որ ապացույցը «բազմաշերտ» է՝ ընդգրկելով հանրահաշիվ, հարմոնիկ անալիզ, երկրաչափություն և թվերի տեսություն:xenaproject.wordpress+1

Claude-ի ապացույցը հետևում է Ուայլս-Թեյլոր-Ուայլսի փաստարկի Darmon-Diamond-Taylor շարադրանքին, որը բնօրինակ ապացույցի պարզեցված տարբերակն է։ Մարդկային միջամտությունը սահմանափակվել է Anthropic-ի հետազոտող Տյանյի Պենգի կողմից տրված բարձր մակարդակի հրահանգներով, որի թիմը Կոլումբիայի համալսարանում ստեղծել է Prove2Me հարթակը, որը հնարավոր դարձրեց այս աշխատանքը:anthropic+1

Ինչպես կառուցվեց ապացույցը

Վաղ փորձերից մի քանիսը ձախողվեցին, քանի որ Claude-ի գործակալները կորցնում էին նախագծի ընթացքի հետքը և դադարում էին արդյունավետ համագործակցել։ Բեկումնային պահը վրա հասավ, երբ թիմը անցավ Prove2Me հարթակին՝ բաց համագործակցային համակարգ, որը պահպանում է թեորեմների պնդումների ուղղորդված գրաֆը՝ թույլ տալով բազմաթիվ գործակալների աշխատել զուգահեռ և որոշել, թե որ ապացույցները փորձել հաջորդիվ։ Օգտագործելով Claude Code-ի վրա հիմնված բազմագործակալային համակարգը՝ տասնյակ գործակալներ սպառեցին մոտ վեց միլիարդ ելքային նշաններ Anthropic-ի ներքին հետազոտական մոդելից, որը, ըստ ընկերության, համեմատելի է Claude Fable 5.1-ի հետ:siliconangle+1

Ավարտված ապացույցը ստուգվել է Lean-ի կողմից՝ օգտագործելով միայն դրա երեք ստանդարտ աքսիոմները, իսկ համեմատիչը հաստատել է, որ թեորեմի ձևակերպումը համապատասխանում է Mathlib-ի Ֆերմայի թեորեմի սեփական ձևակերպմանը։ 13 միլիոն տողով այն հինգ անգամ մեծ է Mathlib-ից՝ ֆորմալացված մաթեմատիկայի հիմնական համայնքային գրադարանից:anthropic+1

Ինչ է սա նշանակում մաթեմատիկայի համար

Բազարդը, որը սկզբում նամակը ստացել էր երաժշտական փառատոնի ժամանակ և կարծել, թե ուղարկողը խաբեբա է, գրել է, որ այս նվաճումը նոր դարաշրջան է ազդարարում. «Եթե Ֆերմայի թեորեմի ավտոմատ ֆորմալացումը հնարավոր է հիմա, ապա մենք մեծ քայլ ենք կատարել դեպի ժամանակակից մաթեմատիկական գրականության ավտոմատ ֆորմալացում»։ Նա նշել է, որ նման տեխնիկաները կարող են բացահայտել գոյություն ունեցող մաթեմատիկական կորպուսի սխալները և թեթևացնել նոր աշխատանքները ստուգող գրախոսների բեռը:anthropic+1

Այս կարևոր իրադարձությունը հաջորդում է մաթեմատիկայում արհեստական բանականության կողմից իրականացված մի շարք առաջընթացների։ Anthropic-ը անցյալ ամիս օգտագործեց Claude-ը Ռիմանի զետա ֆունկցիայի մասին նոր տեղեկություններ բացահայտելու համար, մինչդեռ մրցակից OpenAI-ը իր վերջին մոդելով լուծեց Էրդյոշի մի քանի խնդիրներ։ Anthropic-ը նաև վերջերս օգտագործեց Claude-ը՝ հերքելու Յակոբյանի վարկածը երեք և ավելի չափումներում։ Բազարդը, իր հերթին, բնորոշ չորությամբ նշել է. «Ինձ 1 միլիոն ֆունտ ստերլինգ էին տվել 5 տարվա ընթացքում իմ նախագիծը ղեկավարելու համար. Anthropic-ին պահանջվեց ընդամենը 11 օր, բայց ես կասկածում եմ, թե արդյոք նրանք ավելի շատ գումար չեն ծախսել»:xenaproject.wordpress+2