Tencent Hunyuan imetangaza leo kwamba wakala wa utafiti Hyra, kulingana na modeli ya Hy3, amepata muundo muhimu unaotoa jibu kamili kwa tatizo lililo wazi katika kombinatoriki ya jumlisho, ambalo limekuwa halijatatuliwa kwa zaidi ya nusu karne.
Kwa sasa, nakala ya awali ya utafiti, muundo dhahiri na uthibitisho rasmi vyote vimewekwa hadharani:
Utafiti: https://arxiv.org/abs/2607.27199
Uthibitisho rasmi wa Lean: https://github.com/linhaowei1/sum-diff-proof
Tatizo hilo ni kama ifuatavyo:
Chukua kwanza seti yenye kikomo ya nambari kamili iliyo na angalau vipengele viwili, tuiite A. Jumlisha jozi zozote mbili za vipengele vyake na kukusanya matokeo yote tofauti ili kupata “seti ya jumla” (A+A); toa jozi zozote mbili na kukusanya matokeo yote tofauti ili kupata “seti ya tofauti” (A-A).
Kwa kuwa matokeo yanayojirudia huhesabiwa mara moja tu, swali la kawaida ni: baada ya kujumlisha na kutoa, seti hii itapanuka kwa kiasi gani katika kila hali?
Wanahisabati hutumia vipimo viwili kupima upanuzi huu:
Cha kwanza ni uwiano wa upanuzi wa seti ya jumla, na cha pili ni uwiano wa upanuzi wa seti ya tofauti. Ukosefu wa usawa wa kawaida wa seti za jumla na tofauti unatueleza:
Ili kupima kiashiria hiki, tunaweza kufafanua
Kwa hiyo ukosefu wa usawa wa kawaida unatoa 。 Swali halisi ni: Je, 2 ni kikomo cha juu kilicho legea tu, au ni kiashiria bora kinachoweza kukaribiwa kiholela?
Kwa zaidi ya nusu karne, wanahisabati wameendelea kujenga seti mpya wakijaribu kufanya C (A) iwe kubwa iwezekanavyo. Muundo wa awali wa mwaka 1969 ulifikia takriban 1.0290, wa mwaka 1973 ukaifikisha 1.0598, na muundo wa mwaka 2013 ukaifikisha zaidi hadi 1.1259. Katika mwaka uliopita, utafutaji kadhaa uliosaidiwa na AI uliisogeza thamani hii hadi 1.1449. Katika jaribio la ndani lililorekodiwa kwenye utafiti, Codex (GPT-5.5), kwa mwongozo wa binadamu, iliiongeza tena hadi 1.2851.
Hyra na Hy3 wamepiga hatua ya kuamua. Wametoa familia ya seti dhahiri zenye kikomo za nambari kamili, zinazokidhi
Hii inamaanisha kwamba, bila kujali lengo lililo karibu kiasi gani na 2, tunaweza kujenga seti inayolingana ambayo kiashiria chake kinazidi lengo hilo. Kwa hiyo, 2 ni kikomo cha juu kabisa cha tatizo hili.
Hapo awali, watafiti kama Georgiev, Gómez-Serrano, Tao Zhexuan na Wagner walitumia AlphaEvolve kuboresha kanuni za utafutaji na seti teule. Mbinu hizi hutegemea kuorodhesha wazi seti zenye kikomo; kadiri ukubwa unavyoongezeka, gharama za ukokotoaji na kumbukumbu huongezeka haraka, na pia ni vigumu kuzihamishia kwa njia ya asili kwenye miundo ya asymptotiki inayoweza kuthibitishwa.
Kulingana na maelezo, Tencent Hunyuan alitumia kwanza Hyra kuongeza matokeo bora katika utafutaji wenye kikomo kutoka takriban 1.14 hadi 1.21, kisha akageukia kutumia lugha ya kawaida kupendekeza miundo na hoja za kihisabati. LLM judge ilitumika kutoa mrejesho kwa mchakato wa utafutaji.
Baada ya kufanya kazi kwa takriban saa 24, Hyra alipendekeza wazo kuu la utafiti: kutumia muundo wa tarakimu za mfumo wa kumi na mbili na muundo mahiri kudhibiti seti ya tofauti, kisha kuunganisha msingi wa jumlisho wenye ulinganifu kwenye kikundi cha mzunguko na nadharia ya mabaki ya China, ili seti ya jumla ipanuke kwa kasi inayokaribia ya mraba. Maafisa walikagua na kupanga kwa kujitegemea uthibitisho kamili, na pia wakatoa uthibitisho rasmi wa Lean 4.