Asosiy kontentga o‘tish
Modellar va texnologiya

Tencent Hunyuan: Hy3 modeliga asoslangan Hyra ilmiy agenti additiv kombinatorikadagi 50 yillik ochiq muammoni hal qildi

Tencent Hunyuan bugun e’lon qilgan xabarga ko‘ra, Hyra ilmiy agenti muhim konstruksiyani topib, additiv kombinatorikadagi yarim asrdan ortiq vaqt davomida ochiq qolgan muammoga to‘liq yechim berdi.

Tencent Hunyuan: Hy3 modeliga asoslangan Hyra ilmiy agenti additiv kombinatorikadagi 50 yillik ochiq muammoni hal qildi

Tencent Hunyuan bugun e’lon qilgan xabarga ko‘ra, Hy3 modeliga asoslangan Hyra ilmiy agenti muhim konstruksiyani topib, additiv kombinatorikadagi yarim asrdan ortiq vaqt davomida ochiq qolgan muammoga to‘liq yechim berdi.

Hozirda maqolaning preprinti, aniq konstruksiya va formallashtirilgan isbot ochiq e’lon qilingan:

Maqola: https://arxiv.org/abs/2607.27199

Lean formallashtirilgan isboti: https://github.com/linhaowei1/sum-diff-proof

Muammo quyidagicha:

Avval kamida ikkita elementni o‘z ichiga olgan chekli butun sonlar to‘plami olinadi va A deb belgilanadi. Undagi istalgan ikkita element qo‘shilib, barcha turli natijalar jamlanadi va “yig‘indi to‘plami” (A+A) hosil qilinadi; istalgan ikkita element ayirilib, barcha turli natijalar jamlanadi va “ayirma to‘plami” (A-A) hosil qilinadi.

Takroriy natijalar faqat bir marta hisoblangani sababli, tabiiy savol tug‘iladi: qo‘shish va ayirishdan so‘ng bu to‘plam mos ravishda qanchaga kengayadi?

Matematiklar bunday kengayishni ikki miqdor bilan o‘lchaydilar:

Birinchisi yig‘indi to‘plamining kengayish koeffitsiyenti, ikkinchisi esa ayirma to‘plamining kengayish koeffitsiyentidir. Klassik yig‘indi-ayirma to‘plamlari tengsizligi quyidagilarni bildiradi:

Bu ko‘rsatkichni o‘lchash uchun quyidagini aniqlash mumkin:

Shunday qilib, klassik tengsizlikdan kelib chiqadi. Asl savol shuki: 2 shunchaki bo‘sh yuqori chegara hisoblanadimi yoki unga ixtiyoriy darajada yaqinlashish mumkin bo‘lgan optimal ko‘rsatkichmi?

Yarim asrdan ortiq vaqt davomida matematiklar C (A) ni imkon qadar kattalashtirishga urinib, yangi to‘plamlar konstruksiyalarini yaratib kelishdi. 1969-yildagi dastlabki konstruksiya taxminan 1.0290 natijaga erishgan, 1973-yilda bu ko‘rsatkich 1.0598 ga oshirilgan, 2013-yildagi konstruksiya esa uni 1.1259 ga yetkazgan. So‘nggi bir yil ichida AI yordamidagi bir nechta qidiruvlar bu qiymatni 1.1449 gacha olib bordi. Maqolada qayd etilgan ichki tadqiqot tajribalaridan birida Codex (GPT-5.5) inson yo‘riqnomasi bilan bu ko‘rsatkichni yana 1.2851 gacha oshirdi.

Hyra va Hy3 esa hal qiluvchi qadamni tashladi. Ular quyidagi xususiyatga ega chekli butun sonlar to‘plamlarining aniq konstruksiyalar oilasini taqdim etdi:

Bu shuni anglatadiki, 2 ga qanchalik yaqin bo‘lgan maqsad berilmasin, ko‘rsatkich undan oshadigan mos to‘plamni qurish mumkin. Demak, 2 haqiqatan ham bu masalaning supremumidir.

Tencent Hunyuan: Hy3 modeliga asoslangan Hyra ilmiy agenti additiv kombinatorikadagi 50 yillik ochiq muammoni hal qildi

Bundan avval Georgiev, Gómez-Serrano, Tao Zhexuan va Wagner kabi tadqiqotchilar AlphaEvolve yordamida qidiruv algoritmlari va nomzod to‘plamlarni optimallashtirgan edi. Bunday usullar chekli to‘plamlarni aniq sanab chiqishga tayanadi. Hajm oshgani sari hisoblash va xotira xarajatlari tez ko‘payadi, shuningdek, ularni isbotlanadigan asimptotik konstruksiyaga tabiiy ravishda o‘tkazish qiyin.

Ma’lum qilinishicha, Tencent Hunyuan avval Hyra yordamida chekli qidiruvda eng yaxshi natijani taxminan 1.14 dan 1.21 gacha yaxshilagan, so‘ng matematik konstruksiya va mulohazalarni tabiiy tilda ifodalashga o‘tgan. Qidiruv jarayoniga fikr-mulohaza berish uchun LLM judge’dan foydalanilgan.

Taxminan 24 soatlik ish jarayonidan so‘ng Hyra maqolaning asosiy g‘oyasini taklif qildi: o‘n ikkilik sanoq tizimi raqamlarining tuzilmasi va ayirma to‘plamini nazorat qiluvchi nafis konstruksiyadan foydalanish, keyin esa siklik guruhdagi simmetrik qo‘shish bazasi va Xitoy qoldiqlar teoremasini birlashtirish orqali yig‘indi to‘plamining deyarli kvadratik tezlikda kengayishini ta’minlash. Rasmiy tomon to‘liq isbotni mustaqil tekshirib, tartibga keltirdi hamda Lean 4 da formallashtirilgan isbotni taqdim etdi.