MAZIDISHO 22, HAKUNA HATA MOJA PUNGUFU

Mgongano wa maslahi. Waandishi wanaeleza kwamba mawakala wa AI — Claude, wa Anthropic — waliandika msimbo wa utafutaji na uthibitisho wa Lean usiohitaji mkaguzi wa binadamu, chini ya uelekezi wao, huku sehemu ambayo binadamu lazima aikague ikibuniwa na waandishi. Makala hii pia imeandikwa na Claude.

Kuzidisha gridi mbili za mraba za namba — matriki — kwa njia ya shuleni kunahitaji mazidisho n³ kwa gridi zenye safu mlalo n na safu wima n. Strassen alionyesha kwamba matriki mbili za 2 × 2 zinaweza kuzidishwa kwa mazidisho 7 badala ya 8. Mbinu hii inaweza kutumika kwa kujirudia: kata matriki kubwa katika vitalu vinne, chukulia kila kitalu kama namba moja, na urudie. Gharama basi hukua kama n^2.807 badala ya n³. Kwa mujibu wa makala, pishi hili la 2 × 2 lilithibitishwa kuwa bora kabisa mwaka 1971.

Wazo hilo hilo linafanya kazi kwa ukubwa wowote maalum. Pishi linalozidisha matriki mbili za 3 × 3 kwa mazidisho r, na bado linafanya kazi pale vipengele vinapokuwa vitalu, linatoa gharama inayokua kama n kipeo log₃ r. Hesabu rahisi inaonyesha kilicho hatarini: pishi la aina hiyo linamshinda Strassen hasa pale r ni 21 au chini yake, na linashindwa kwa 22 au zaidi. Pishi bora linalojulikana la 3 × 3, la Laderman, linatumia mazidisho 23 na halijaboreshwa tangu 1976.

Mlango uliobaki wazi kidogo

Namba bora kabisa inayowezekana kwa tatizo fulani huitwa rank yake. Mipaka ya chini ya rank ya kuzidisha 3 × 3 ilipanda polepole: 19 mwaka 2003, kisha 20 mnamo Machi 2026, iliyokokotolewa na Wang juu ya mfumo mdogo kabisa wa namba wenye 0 na 1 pekee, ambapo 1 + 1 = 0. Mnamo Septemba 2026, Wang na timu iliyoongozwa na Yang walifikia 21 kila mmoja kivyake, ndani ya siku kumi baina yao. Lakini 21 bado iliacha nafasi kwa pishi la 3 × 3 lenye kasi kuliko la Strassen.

Isaac Rudich, wa Polytechnique Montréal na Chuo Kikuu cha Carnegie Mellon, na Louis-Martin Rousseau, wa Polytechnique Montréal, sasa wamesukuma mpaka huo hadi 22.

Nadharia 1. Algoriti yoyote inayozidisha matriki mbili za 3 × 3 kwa viasili vya namba kamili, na inayoweza kutumika kwa kujirudia kwenye vitalu vya ukubwa wowote, hutumia angalau mazidisho 22.

Kwa hiyo hakuna algoriti ya aina hiyo inayoweza kufanya vizuri kuliko takriban n^2.814 — na hakuna inayoweza kushinda mbinu ya Strassen ya 2 × 2.

Mafumbo 496 madogo zaidi

Uthibitisho unajengwa juu ya jedwali lililobuniwa na Wang, linalogawa tatizo gumu katika matatizo 496 rahisi zaidi. Kila moja linaongeza “masharti” kwenye matriki ya kwanza — kwa mfano, kwamba baadhi ya vipengele vyake vikijumlishwa vinatoa sifuri. Kadiri masharti yanavyoongezeka, ndivyo tatizo linavyokuwa rahisi, hadi hali ya kawaida kabisa ambapo matriki yote ni sifuri.

Waandishi kwanza walijenga programu ya utafutaji kamili iliyowaambia jibu la kweli la kila fumbo kabla hawajajaribu kulithibitisha. Majibu hayo yalitumika kama ramani: yalionyesha ni mipaka gani ya chini iliyostahili kufuatiliwa. Mwishowe, uthibitisho wao unaweka mipaka kwa mafumbo yote 496, unatatua 359 kati yake kikamilifu — dhidi ya 195 katika matokeo ya hivi karibuni ya Wang — na unapandisha mpaka wa chini kwa 252. Nadharia yao wenyewe ya “kuunganisha” inachanganya mapishi ya mafumbo mawili rahisi zaidi kuwa pishi la fumbo la tatu, na ilitoa mipaka 145 ya juu.

Masharti mawili ni muhimu katika kauli ya mwisho. Viasili vya namba kamili: pishi lenye viasili vya namba kamili, likisomwa katika mfumo wa namba wa 0 na 1, linabaki kuwa pishi halali bila mazidisho ya ziada, kwa hiyo mpaka unahamishika. Vitalu: bila sharti hilo, njia za mkato zipo. Algoriti ya Rosowski ya 3 × 3, iliyotajwa katika makala, inahitaji mazidisho 21 tu, lakini inategemea namba kubadilishana nafasi (commuting) na haiwezi kutumika kwa kujirudia.

Uthibitisho uliokaguliwa na mashine

Uthibitisho umeandikwa kwa Lean, lugha ya programu ambamo nadharia hukusanywa (compile) tu ikiwa kila hatua imethibitishwa. Uthibitisho kamili una takriban mistari milioni moja iliyosambaa katika moduli 3,521, na huchukua saa 11.1 kukaguliwa kwenye kiini kimoja cha prosesa. Hakuna anayehitaji kuusoma wote. Mkaguzi husoma maktaba ya takriban mistari 1,000, iliyoandikwa na waandishi kabla uthibitisho wowote haujakuwepo, inayofafanua pishi la kuzidisha ni nini na kutamka nadharia; kiini cha Lean hukagua yaliyobaki, na kikaguzi huru kinaweza kurudia tokeo.

Waandishi pia wanabainisha kwamba mawakala wa AI walitafuta maandiko ya kitaalamu: walikagua kwamba kila rejeo lipo, “lakini si kwamba kila moja lina hasa wazo tunalolihusisha nalo.”

Pengo la mwisho

Swali moja linabaki: je, pishi la 3 × 3 lenye mazidisho 22 lipo, au 23 ya Laderman ndiyo kiwango cha chini halisi? Waandishi wanatarajia pengo hilo “kuzibwa karibuni sana”, na watatoa msimbo wao wa utafutaji litakapozibwa, au makala itakapokubaliwa kuchapishwa. Mpaka huu pia unaacha kando mapishi yenye viasili visivyo namba kamili.