Թարմացվել է DeepSeek-ի մաթեմատիկական մոդելը՝ Prover-V2

Չինական AI ստարտափ DeepSeek-ը լռելյայն ներկայացրել է Prover-V2-ը՝ 671 միլիարդ պարամետր ունեցող մասնագիտացված մոդել, որը նախատեսված է մաթեմատիկական պնդումների և տեսութունների ապացույցների լուծման համար։ Սա տեղի ունեցավ ընդամենը մեկ օր անց այն բանից հետո, երբ Alibaba-ն ներկայացրեց իր Qwen3 մոդելների շարքը, և DeepSeek-ի սպասվող R2 մոդելի շուրջ սպասումները աճում են, գրում է IndexBox-ը։

Prover-V2-ի հիմնական առանձնահատկությունները

Prover-V2-ը կառուցված է DeepSeek-ի V3 ճարտարապետության վրա՝ կիրառելով «փորձագետների խառնուրդ» (Mixture-of-Experts, MoE) մոտեցումը, որով բարդ մաթեմատիկական առաջադրանքները բաժանվում են ենթառաջադրանքների, որոնք մշակվում են տարբեր փորձագետ մոդուլների միջոցով։ Միայն համապատասխան մոդուլներն են ակտիվացվում, ինչը բարձրացնում է արդյունավետությունը։ Մոդելը օգտագործում է FP8 քանակականացում՝ հաշվարկային ծախսերը նվազեցնելու և մաթեմատիկական ճշգրտությունը պահպանելու համար, ինչը թույլ է տալիս օգտագործել այն նաև սահմանափակ ռեսուրսներով սարքերում։

Մոդելը հասանելի է բաց կոդով Hugging Face հարթակում։ Օգտագործողներ, այդ թվում՝ մաթեմատիկայի օլիմպիադաների մասնակիցներ, բարձր են գնահատել դրա ունակությունները պաշտոնական ապացույցների ստեղծման մեջ։ Prover-V2-ի առանձնահատկություններից է «սառը մեկնարկի» ուսուցման գործընթացը, որը նրան թույլ է տալիս ստեղծել պաշտոնական ապացույցներ Lean 4 հարթակի միջոցով՝ կապ ստեղծելով ինտուիտիվ և ֆորմալ մաթեմատիկայի միջև։

Մրցակցային միջավայր և համատեքստ

Prover-V2-ի թողարկման ժամանակը ռազմավարական է՝ հաջորդելով Alibaba-ի Qwen3 մոդելների թողարկմանը։ Թեև Qwen3-ի խոշորագույն մոդելը ունի 235 միլիարդ պարամետր, DeepSeek-ի 671 միլիարդ պարամետր ունեցող կառուցվածքը՝ MoE տեխնոլոգիայով, ավելի բարձր արդյունավետություն է ցուցաբերում՝ համեմատաբար ցածր հաշվարկային ծախսերով։

Չինական AI ընկերությունները սկսում են լուրջ մրցակցել արևմտյան գիգանտների հետ։ DeepSeek-ի նախորդ R1 մոդելը արդեն հասել էր OpenAI-ի o1 մակարդակին՝ զգալիորեն ավելի ցածր ծախսերով։ Xiaomi-ն նույնպես միացել է մրցակցությանը՝ թողարկելով իր MiMo-7B մոդելների շարքը։ Մաթեմատիկական AI-ն դառնում է նոր մրցակցային դաշտ, որտեղ մասնագիտացված մոդելները կարող են իրական հեղաշրջում կատարել։

DeepSeek-ի առաջխաղացումները

Ենթադրությունները շատանում են՝ կապված DeepSeek-ի սպասվող R2 մոդելի հետ, որի պարամետրերի թիվը կարող է հասնել մինչև 1.2 տրիլիոնի՝ ներառյալ տեսողական հնարավորություն և բարձրակարգ տրամաբանական ունակություններ։ Թեև այն նախատեսված էր 2025-ի մարտին, պաշտոնական թողարկման ամսաթիվ դեռ չկա։ Prover-V2-ի թողարկումը դիտվում է որպես ցուցադրություն DeepSeek-ի տեխնիկական հզորությունների՝ առաջ ընկած R2 մոդելի գործարկումից։

DeepSeek-ի մասնագիտացված մոտեցումը ակնհայտ է նաև DeepSeekMath 7B մոդելում, որը մրցակցային MATH բենչմարքում ստացել է 51.7% արդյունք՝ առանց արտաքին գործիքների կամ քվեարկության մեթոդների կիրառման։ Ընկերությունն ընտրել է ոլորտի գերազանցության ուղին՝ փոխարենը համընդհանուր մոդելների։

Ապագա հետևանքներ և R2 մոդել

Prover-V2-ի լուռ թողարկումն ունի նշանակալի ազդեցություն՝ AI-ի ներգրավմամբ մաթեմատիկական հետազոտությունների ապագայի վրա։ Այս մոդելը ներկայացնում է նեղ, բայց կենսական կարևորության ոլորտների համար մասնագիտացված AI-ի աճող միտումը։ Գիտնականները այժմ կարող են օգտագործել Prover-V2-ը թե՛ արագ վերլուծությունների, թե՛ պաշտոնական ապացույցների համար՝ միացնելով ինտուիտիվ ըմբռնումը ֆորմալ խստության հետ։

Մինչ այդ, տեխնոլոգիական աշխարհը անհամբեր սպասում է R2 մոդելին։ Ըստ արդյունաբերական կանխատեսումների՝ այն կարող է գերազանցել OpenAI-ի, Anthropic-ի և այլ մրցակիցների մոդելներին՝ պահպանելով DeepSeek-ի ծախսարդյունավետության առավելությունը։ Reuters-ի տվյալներով՝ թողարկումը կարող է տեղի ունենալ ամենամոտ ապագայում՝ 2025-ի մայիսի ընթացքում։