Ushbu tadqiqot tabiiy tilda ifodalangan matematik, ilmiy va texnik bilimlarni nafaqat yakka teoremalar yoki tasdiqlar darajasida, balki butun bir nazariyaning barcha bog‘liqliklari bilan birga mashina tomonidan tekshiriladigan formal shaklga o‘tkazilishi zarurligini asoslaydi. Mualliflar yangi eksperimental tizim ishlab chiqish o‘rniga matematika, fan, dasturiy ta’minot va apparat vositalarini verifikatsiya qilishdagi (tekshirishdagi) mavjud loyihalarni, avtomatik formallashtirish adabiyotini hamda sohaning baholash muammolarini tahlil qiluvchi pozitsion maqolani taqdim etganlar. Asosiy da’vo shundan iboratki, maqsadli teoremani formallashtirish uchun avvalo aksiomalar, ta’riflar, belgilar, yordamchi lemmalar, isbot taktikalari va ular orasidagi bog‘liqliklarni izchil kutubxona sifatida qurish talab etiladi. Shunday bo‘lsa-da, tadqiqot taklif etilgan nazariya darajasidagi yondashuvni to‘liq amalga oshiruvchi yangi tizim, ma’lumotlar to‘plami yoki eksperimental tasdiqni taqdim etmaydi.

Maqolada hozirgi avtomatik formallashtirish ishlarining aksariyati yetuk formal kutubxonalar allaqachon mavjud deb hisoblashi ta’kidlanadi. Masalan, Lean muhitidagi Mathlib ko‘plab ta’riflar va lemmalarni avvaldan ta’minlagani sababli bitta maqsadli tasdiqni o‘girish nisbatan oson ko‘rinadi. Biroq sonli tahlil, muayyan muhandislik sohalari, maxsus xavfsizlik siyosatlari yoki tashkilotga xos soha tillari kabi yetarli formal infratuzilma bo‘lmagan sohalarda asosiy muammo bitta tasdiqni tarjima qilish emas, balki ushbu tasdiqning mazmunini ta’minlovchi butun nazariy kontekstni noldan shakllantirishdir.

Mualliflar nazariya darajasidagi avtomatik formallashtirish oldida to‘rtta asosiy muammoni belgilaydilar: formallashtirishlarning ma’no jihatidan ekvivalentligini ishonchli tekshirish, katta matnlarni ierarxik bog‘liqlik tuzilmalariga ajratish va qayta ishlatiladigan abstraksiyalarni o‘rganish, Lean dan tashqari kam resursli soha tillariga moslashish hamda matn, matematik belgilar, vaqt diagrammalari, sxemalar yoki erkin chizmalar kabi ko‘p modalli (multimodal) kirish ma’lumotlarini birgalikda talqin qilish. Yechim sifatida esa nazariya darajasidagi baholash mezonlari, tor bitta kutubxonaga moslashgan emas, balki umumiy maqsadli modellar hamda turli formal tillar o‘rtasida ko‘prik bo‘la oladigan yagona oraliq ifodalash (intermediate representation) taklif etiladi.

Avtomatik formallashtirish nima?

Avtomatik formallashtirish (autoformalization) — tabiiy tilda yoki yarim formal ko‘rinishda bayon etilgan axborotni isbot assistenti (proof assistant) yoki formal verifikator tomonidan tekshirilishi mumkin bo‘lgan formal tilga o‘tkazishdir. Bu tarjima shunchaki jumlalarni sintaktik qayta yozish emas. Hosil qilingan formal ifoda asl matndagi ma’no, farazlar, kvantorlar, istisnolar va bog‘liqliklarni to‘liq saqlashi shart.

Maqola ikkita asosiy quyi vazifani ajratadi:

• Tasdiqni avtomatik formallashtirish: Tabiiy tildagi teorema, gipoteza yoki da’voni formal e’longa aylantirish.
• Isbotni avtomatik formallashtirish: Muayyan tabiiy til isbotining mantiqiy tuzilishini saqlagan holda uni mashina tekshiradigan isbot skriptiga o‘tkazish.

B ilovada ta’kidlangan muhim farq shundaki, isbotni avtomatik formallashtirish umumiy avtomatik teorema isbotlash (ATP) bilan bir xil emas. Formal teorema isbotlagich maqsadli tasdiqni tasdiqlovchi har qanday to‘g‘ri isbotni topishga intilishi mumkin. Isbotni avtomatik formallashtirish esa asl matndagi muayyan fikrlash oqimiga sodiq qolishi shart. Ayni bir teorema uchun ikkita turli formal isbot to‘g‘ri bo‘lishi mumkin; ammo ulardan faqat bittasi tarjima qilingan asl dalilning mantiqiy strukturasini ifodalaydi.

Nazariya darajasida avtomatik formallashtirish nimani o‘zgartiradi?

Mualliflar ta’rifiga ko‘ra, nazariya darajasida avtomatik formallashtirish — muayyan soha doirasidagi aksiomalar, ta’riflar, belgilar, misollar, lemmalar, teoremalar, isbotlar, taktikalar va ular orasidagi barcha bog‘liqliklarni yaxlit va izchil formal kutubxona ko‘rinishida qurishdir. Bu yondashuv bir-biridan uzilgan maqsadli tasdiqlarni tarjima qilish o‘rniga, o‘sha tasdiqlar tayanadigan bilimlar arxitekturasini yaratishni ko‘zlaydi.

2-rasmdagi «Nazariya darajasidagi avtomatik formallashtirish minorasi» Yevklid geometriyasi misolida to‘rt qatlamli strukturani ko‘rsatadi:

Maqolada keltirilgan natijaga ko‘ra, mavjud eng ilg‘or usullardan biri quyi qatlamlar insonlar tomonidan oldindan formallashtirilgan deb qabul qilinganda 3-qatlamdagi tasdiqlarda 71,4% muvaffaqiyatga erishmoqda. Biroq mualliflar amaldagi usullar 0–2 qatlamlar orasidagi barcha infratuzilmani noldan avtomatik qurishni hali maqsad qilmaganini ta’kidlaydilar. Shu sababli 71,4% ko‘rsatkichi butun nazariyaning to‘liq avtomatik formallashtirilish darajasi sifatida talqin qilinmasligi lozim.

Nima sababdan bitta teoremani tarjima qilish yetarli emas?

Bitta maqsadli teorema formal muhitda ko‘ringanidan ancha kengroq poydevorga tayanadi. Teorema ichida uchraydigan har bir obektning turi, har bir munosabatning ma’nosi, qo‘llaniladigan belgilar, yordamchi natijalar va isbot qadamlari oldindan ta’riflangan bo‘lishi shart. Tabiiy tilda mutaxassislar yashirin (nazarda tutilgan) qoldiradigan ko‘plab ma’lumotlar formal tizimda ochiq ko‘rsatilishi majburiydir.

Masalan, matematik olim «kvadrat» tushunchasining to‘g‘ri to‘rtburchak va romb xususiyatlari bilan bog‘liqligini kontekstdan tushunishi mumkin. Formal tizimda esa bu bog‘liqlikni ta’minlovchi ta’riflar yoki teoremalar kutubxonada mavjud bo‘lishi lozim. Xuddi shuningdek, apparat vositalari muhandisi signalning «keyingi taktidan boshlab barqaror qolishi» kerakligini vaqt diagrammasidan anglaydi; ammo formal spetsifikatsiyada «keyingi takt» operatori ochiq yozilishi shart.

Avtomatik formallashtirish nima uchun muhim?

Neyron teorema isbotlagichlar uchun ma’lumotlar yaratish

Neyron tarmoqli teorema isbotlash tizimlarining rivojlanishi katta va ishonchli formal ma’lumotlar bazalariga bog‘liq. Tabiiy tildagi matematik matnlar va isbotlarning formal muqobillarini yaratish tabiiy til bilan formal til o‘rtasida parallel o‘qitish ma’lumotlarini hosil qiladi. Tasdiqlarni formallashtirish yangi maqsadlarni yaratsa, isbotlarni formallashtirish mashina tekshiradigan isbot qadamlarini beradi.

Nazariy va muhandislik verifikatsiyasini tezlashtirish

Formal verifikatsiya loyihalari nafaqat yakuniy teorema yoki tizimni tekshiradi, balki ta’riflar, oraliq natijalar va texnik vositalardan iborat keng kutubxonani shakllantiradi. 1-jadvalda matematika, fan, dasturiy ta’minot va apparat vositalaridan tanlangan loyihalar juda katta vaqt va inson mehnatini talab qilgani ko‘rsatilgan:

Jadvalning asosiy g‘oyasi shundaki, formal tekshirishdagi asosiy mehnat sarfi bitta isbotni topishda emas, balki o‘sha maqsad qurilishi mumkin bo‘lgan butun ta’riflar va yordamchi teoremalar tarmog‘ini yaratishdadir. Maqolada inson mehnati bilan tub sonlar teoremasining formallashtirilishi 1,5 yil davom etgani; sun’iy intellekt ko‘magidagi miqdoriy takomillashtirish esa uch haftada bajarilgani misol qilinadi. Ammo bu ikki loyihaning ko‘lami bir xil emas va muddatlarni to‘g‘ridan-to‘g‘ri teng taqqoslab bo‘lmaydi.

Tabiiy tildagi mulohazalarni asoslash va yo‘naltirish

Katta til modellarining tabiiy tildagi mulohazalari ziddiyatli asoslar, mavjud bo‘lmagan farazlar yoki tushirib qoldirilgan qadamlarni o‘z ichiga olishi mumkin. Formal tekshirgich noto‘g‘ri turdagi ta’riflarni, ziddiyatlarni yoki isbotlanmaydigan qadamlarni aniqlay oladi. Maqola ta’rificha, «asoslash» — yaroqsiz qadamlarni chetlatish; «yo‘naltirish» esa tekshirgichning xatolik bildirishnomalaridan modelning o‘z javobini to‘g‘rilashi uchun foydalanishdir.

Shu bilan birga, maqola formal verifikatsiya tabiiy til tafakkurining o‘rnini to‘liq egallashini emas, uni to‘ldirishini yoqlaydi.

Umumiy fikrlash qobiliyatlariga hissasi

Mualliflar formal tekshirgichdan olinadigan tekshiriluvchan qayta aloqa matematikadan tashqaridagi fikrlash vazifalariga ham ko‘chirilishi mumkin bo‘lgan foydali xatti-harakatlarni shakllantirishini muhokama qiladilar. Bu matematik ta’lim avtomatik ravishda umumiy sun’iy intellekt yaratishini isbotlamaydi, ammo tekshiriluvchan mukofotlar bilan o‘qitish istiqbolli yo‘nalish sifatida ko‘riladi.

Haqiqiy formallashtirish loyihalari nima uchun nazariya darajasidadir?

Kepler gipotezasi yakka matematik da’vo bo‘lsa-da, uni formal isbotlash yuzlab ta’riflar va yordamchi lemmalarni yaratishni talab qildi. Liquid Tensor Experiment kabi loyihalarda ham maqsadli teoremani ifodalash uchun kondensatsiyalangan matematikaning katta qismlari avval Lean muhitida qurildi. Bu misollar haqiqiy loyihalar oddiy «bitta jumlani boshqa tilga tarjima qilish» emasligini ko‘rsatadi.

Ikkinchi sabab — tasdiqlar darajasidagi usullarning yetuk kutubxonalarga qattiq bog‘liqligidir. Agar biror soha Mathlib da yetarlicha ifodalanmagan bo‘lsa, tasdiqni tarjima qilishdan oldin yetishmayotgan ta’riflar va yordamchi teoremalarni yaratish zarur bo‘ladi.

Uchinchi sabab — nazariy kashfiyotlarning yangi abstraksiyalarga tayanishidir. Guruh, halqa va maydon kabi algebraik tuzilmalar yoki kategoriyalar nazariyasidagi morfizmga asoslangan yondashuv avval ayro ko‘ringan bilimlarni yagona tuzilma ostida birlashtirgan. Mualliflar kelajakda yirik formal bilimlar bazalarini qayta tashkil etish orqali yangi abstraksiyalar kashf etilishi mumkinligini ta’kidlaydilar (bu amaliy natija emas, uzoq muddatli ilmiy g‘oyadir).

Muqobil qarashlar va mualliflarning javoblari

«Tabiiy til mulohazalarining o‘zi yetarli» degan qarash

Tabiiy til maxsus sintaksis talab qilmagani va ulkan o‘quv bazasiga egaligi tufayli juda moslashuvchandir. Kuchli modellar qiyin matematik masalalarni tabiiy tilda yecha oladi. Mualliflar bunga javoban formal usullarning uchta ustunligini ko‘rsatadilar: mashina tomonidan qat’iy tekshiriluvchanlik, katta jamoalarda har bir detalni qayta o‘qimasdan modulli ishonch hosil qilish hamda nafaqat o‘rganish, balki qidiruv orqali ham masshtablanish.

«Asosiy e’tibor teorema isbotlashga qaratilishi kerak» degan qarash

Teorema isbotlash berilgan formal maqsad uchun to‘g‘ri isbotni qidiradi. Ammo maqsadli tasdiq va tizim spetsifikatsiyalari avval formal tilda yozilishi shart. Apparat vositalarini tekshirishda model tekshirgichlar yetuk bo‘lsa-da, aynan qaysi xususiyatni tekshirish kerakligini to‘g‘ri yozish asosiy to‘siq bo‘lishi mumkin. Avtomatik formallashtirish isbotlagich ishlaydigan mazmunli maqsadlarni yaratadi.

«Tasdiqlar darajasidagi usullarni rivojlantirish realroq» degan qarash

Tasdiqlar darajasidagi usullarning o‘lchanadigan ma’lumotlar bazalari mavjud. Ba’zi inson–AI hamkorliklarida mutaxassislar avval batafsil chizma yoki bog‘liqlik grafigini tayyorlaydi, model esa lemmalarni ketma-ket formallashtiradi. Mualliflar bu yondashuvni «yarim nazariya darajasidagi» deb ataydilar, chunki bog‘liqlik grafigini tuzish baribir inson zimmasida qoladi va asosiy ta’riflar Mathlib dan olinadi.

Birinchi ochiq muammo: Ekvivalentlik qanday tekshiriladi?

Avtomatik formallashtirishda faqat hosil qilingan kodning kompilyatsiya bo‘lishi (xatosiz yig‘ilishi) yetarli emas. Formal ifoda to‘g‘ri yozilgan, ammo tabiiy tildagi asl ma’nodan boshqa narsani anglatayotgan bo‘lishi mumkin. Shu sababli asosiy savol — ikki ifoda ayni bir ma’noni ifodalayaptimi yoki yo‘qmi?

Ishonchli etalon ma’lumotlarning yetishmasligi

ProofNet ma’lumotlar bazasidagi 371 ta masalaning 118 tasida (31,8%) inson tomonidan kiritilgan formallashtirish xatolari topilgan va tuzatilgan. PutnamBench da esa e’lon qilingandan so‘ng 672 ta Lean formallashtirishidan kamida 58 tasida (8,6%) xatolar to‘g‘rilangan. Ta’riflarni formallashtirishga mo‘ljallangan bazalar esa 56 ta Wikipedia va 30 ta arXiv ta’riflari bilan cheklangan. Hozirda butun bir nazariyani baholaydigan umumiy benchmark mavjud emas.

Sintaktik tenglik, mantiqiy ekvivalentlik va kontekst muammosi

Quyidagi ikki ifoda ayni bir matematik mazmunga ega:

\[ \forall n \in \mathbb{N},\; P(n) \]

\[ \neg \exists n \in \mathbb{N},\; \neg P(n) \]

Bu yerda n — natural son, P — natural sonlardagi xususiyat. Birinchisi «barcha natural sonlar P xususiyatiga ega», ikkinchisi «P xususiyatiga ega bo‘lmagan hech qanday natural son yo‘q» deganidir. Sintaksisi turlicha bo‘lgani uchun oddiy matnli solishtirish ularni bir xil deb topmaydi, biroq ular mantiqan ekvivalentdir.

Quyidagi ekvivalentlik esa faqat mantiqdan emas, balki Yevklid geometriyasidagi ta’riflar va teoremalardan kelib chiqadi:

\[ \mathrm{rectangle}(a) \land \mathrm{rhombus}(a) \]

\[ \mathrm{square}(a) \]

Bu yerda a — geometrik obekt. Obektning bir vaqtda to‘g‘ri to‘rtburchak va romb bo‘lishi uning kvadrat ekanini bildiradi. Ammo bu so‘zlar shunchaki ma’nosiz predikatlar deb olinsa, bu xulosa chiqmaydi. Ekvivalentlikni baholash uchun qaysi fon nazariyasiga tayanish kerakligi aniq bo‘lishi lozim.

Ta’rifiy ekvivalentlik nega yetarli emas?

Lean kabi ispat assistentlari ta’riflarni ochish orqali ayrim ifodalarni soddalashtiradi. Biroq natural sonlar qo‘shilishining rekursiv ta’rifi sababli quyidagi ifodalar bir xil qisqarmasligi mumkin:

[ m + 0 ]

[ 0 + m ]

Birinchi ifoda ta’rif bo‘yicha to‘g‘ridan-to‘g‘ri m ga soddalashsa, ikkinchi ifoda o‘zgaruvchi ustida qotib qolishi mumkin. Uni tenglashtirish uchun qo‘shishning o‘rin almashtirish qonuni kabi isbotlangan teoremalarga murojaat qilish zarur bo‘ladi.

Cheklovlarsiz mulohaza ekvivalentligining xavfi

Fon nazariyasida to‘g‘ri bo‘lgan har qanday ikki tasdiqni ekvivalent deb qabul qilish ham xatodir. Bu yondashuv «1 + 1 = 2» bilan Ferma teoremasi kabi butunlay boshqa mazmundagi ikki to‘g‘ri tasdiqni teng deb yuborishi mumkin. BEq+ tekshirgichi global kontekst va isbot qidiruvini cheklab, 98,0% aniqlik (precision) va 48,3% to‘liqlik (recall) ko‘rsatgan. Sof ta’rifiy ekvivalentlik esa 100% aniqlik va 30,9% to‘liqlik bergan.

Shuningdek, quyidagi ikki xil to‘g‘ri xususiyatning ekvivalentligi avtomatlashtirilgan taktikalar har ikkala tomonni mustaqil isbotlagani tufayli soxta ekvivalentlik xatosini keltirib chiqarishi mumkin:

\[ (n \cdot 1 = n) \leftrightarrow (n + 0 = n) \]

Ikkalasi ham to‘g‘ri bo‘lsa-da, biri ko‘paytirishning, biri qo‘shishning neytral elementi haqidadir; asl ma’no jihatidan ular ayni bir narsa emas.

Ekvivalentlikning subyektiv chegarasi

Maqoladagi yaqqol misol quyidagi integraldir:

\[ \int_{0}^{1} 2x^3 \ln(x^2+1)\,dx > 0 \]

\[ \int_{0}^{1} 2x^3 \ln(1+x^2)\,dx > 0 \]

Integral hisoblanganda u quyidagi ifodaga ham soddalashadi:

\[ \frac{1}{4} > 0 \]

Dastlabki ikki ifoda tashqi ko‘rinishdan bir xil bo‘lsa, uchinchisi faqat integrallash bajarilgandagina ayni natijani beradi. Baholovchi tizim qancha hisoblashni amalga oshirishi kerak? Ekvivalentlik darajasi baholovchining hisoblash resursi va bilimiga qarab o‘zgaradi. Shu bois har bir ekvivalentlik tekshirgichi ruxsat etiladigan hisoblash chuqurligi uchun chegara belgilashi shart.

Ikkinchi ochiq muammo: Ierarxik dekompozitsiya va abstraksiyalarni o‘rganish

Katta darslikni formallashtirish matnni shunchaki alohida jumlalarga ajratishdan iborat emas. Tizim qaysi ta’rif oldin kelishi kerakligini, qaysi teorema qaysi lemmalarga tayanishini va qaysi tushunchalarni qayta ishlatiladigan umumiy abstraksiya ostida birlashtirish mumkinligini aniqlashi lozim.

MiniF2F da DeepSeek-Prover-V2 88,9%, BFS-Prover-V2 esa 95,1% natija ko‘rsatgan. Ammo bu tizimlar yakka maqsadli isbotni quyi maqsadlarga ajratadi. Nazariya darajasidagi vazifa esa o‘nlab asosiy teoremalar va murakkab ichki bog‘liqliklarga ega butun kitoblarni strukturalashni talab etadi.

Abstraksiyalarni o‘rganishning ikki yo‘nalishi bor:

1. Ta’riflarni formallashtirish: Matndagi takrorlanuvchi tushunchalarni topib, ularni qayta ishlatiladigan formal ta’riflarga aylantirish.
2. Bilimlarni siqish (kompaktlashtirish): Mavjud yirik formal kutubxonalardan umumiy strukturalarni ajratib olib, qisqaroq va modulli abstraksiyalar yaratish.

Mualliflar tabiiy tildan tushunchalarni ajratishda umumiy maqsadli til modellari agentlarini, formal kutubxona tuzilgach esa semantik kod tahlili usullarini qo‘llashni tavsiya etadilar.

Uchinchi ochiq muammo: Lean dan tashqari kam resursli soha tillari

Haqiqiy dunyodagi formal verifikatsiya faqat Lean bilan cheklanmaydi. Cheklovlarni yechish, protokollarni tekshirish, apparat vositalari spetsifikatsiyalari, xavfsizlik tahlili va kirish huquqlari siyosati uchun maxsus soha tillari (DSL) qo‘llaniladi. Bu tillarda tabiiy til–formal til juftliklaridan iborat katta ma’lumotlar bazalari mavjud emas.

Avtomatik teorema isbotlagichlar tillari (SMT-LIB, TPTP)

Ro‘yxatdagi elementlarni o‘chirish amali uchun quyidagi xususiyat misol qilinadi:

\[ \forall x,w,L,\; \mathrm{drop}(w,\mathrm{drop}(x,L)) = \mathrm{drop}(x+w,L) \]

Tons of Inductive Problems bazasida formal ifodalar bo‘lsa-da, ularning tabiiy tildagi tavsiflari yo‘qligi parallel korpus yaratishni qiyinlashtiradi.

Taqsimlangan protokollarni tekshirish tillari (Ivy, PVerifier)

IvyBench bor-yo‘g‘i 54 ta formallashtirilgan protokol isbotini o‘z ichiga oladi, bu esa ma’lumotlar o‘ta taqchilligini ko‘rsatadi.

Apparat vositalarini tekshirish tillari (SystemVerilog Assertions)

Apparat spetsifikatsiyalarida vaqt diagrammasi va matn birga o‘qilishi shart. Masalan, 5-rasmdagi vaqt munosabati quyidagi formal kodda aks etadi:

(VALID && !READY) |-> ##1 $stable(INFO)

##1 operatori barqarorlik keyingi taktda boshlanishini bildiradi va bu ma’lumot faqat vaqt diagrammasida mavjud. Bu holat to‘g‘ri formallashtirish matndan tashqari ko‘p modalli tahlilni talab qilishini isbotlaydi.

Deklarativ dasturlash tillari

SQL, Cypher, CodeQL va Cedar kabi deklarativ tillar «qanday hisoblashni» emas, «qanday shart bajarilishini» bildiradi. Tabiiy tildagi talabni Cedar siyosatiga o‘tkazish axborotni yo‘qotmasdan formal chegaralarga ko‘chirishdir. Python yoki C++ kabi imperativ tillarga tarjima qilish esa yangi algoritmlar va ma’lumotlar strukturalarini kiritishni talab etuvchi generativ jarayondir.

To‘rtinchi ochiq muammo: Matndan tashqari ko‘p modalli kirishlar

Haqiqiy formallashtirish to‘rt xil axborot manbasini o‘z ichiga oladi:

• Tabiiy til tavsiflari va texnik hujjatlar,
• Matematik belgilar yoki mavjud formal tillar,
• Vaqt diagrammalari, sxemalar, holat mashinalari va blok-sxemalar,
• Geometrik chizmalar yoki interfeys namunalari.

Tizim ushbu manbalar orasidagi ziddiyatlarni aniqlashi, yashirin farazlarni ochishi va barchasini yagona formal modelda birlashtirishi lozim.

1-tavsiya: Ishonchli nazariya darajasidagi baholash mezonlari

Ideal baholash tizimi uch shartni bajarishi kerak:

1. Faqat maqsadli teoremalarni emas, fon nazariyasining barcha ta’rif va lemmalarini qamrab olishi,
2. Ekvivalentlik tekshirgichining aniqlik (precision) va to‘liqlik (recall) ko‘rsatkichlarini hisobot qilishi,
3. Sinovdagi fon nazariyasining o‘quv bazasiga sizib o‘tmaganligini qat’iy tekshirishi.

2-tavsiya: Tor ixtisoslashgan modellar o‘rniga umumiy maqsadli modellar

Goedel-Formalizer-V2-32B modeli Mathlib dan tashqaridagi LeanEuclidPlus bazasida 0,0% natija bergan bo‘lsa, umumiy Qwen3-32B modeli 20,6% ko‘rsatgan. Bu tor kutybxonaga qattiq moslangan (overfitted) modellar boshqa sohalarga moslasha olmasligini bildiradi. Tavsiya — umumiy modellarni tekshirgich qayta aloqasi va qidiruv algoritmlari bilan kuchaytirishdir.

3-tavsiya: Yagona oraliq ifodalash (Common IR)

7-rasm barcha kirish turlari (matn, diagramma, chizma) dastlab yagona oraliq ifodalashga (IR) o‘tkaziladigan va undan keyin turli maqsadli tillarga (Lean, SMT, SystemVerilog, Cedar) avtomatik o‘giriladigan arxitekturani taklif etadi. Lean tili o‘zining boy tip nazariyasi bilan bu oraliq ifodalash uchun asosiy nomzod sifatida ko‘rsatilgan.

Tadqiqot nimani tasdiqlaydi?

• Haqiqiy formal loyihalar bitta tasdiqni tarjima qilishdan ko‘ra ulkan ta’riflar va yordamchi natijalar infratuzilmasini talab qiladi.
• Mavjud tasdiq darajasidagi usullar asosan inson tayyorlagan kutubxonalarga tayanadi.
• Ekvivalentlikni baholash sintaktik moslik bilan yechilmaydigan murakkab muammodir.
• Kam resursli soha tillari va ko‘p modalli hujjatlar Lean-matematika bazalaridan tubdan farq qiladi.
• Nazariya darajasidagi benchmarklar va yagona oraliq ifodalash istiqbolli tadqiqot yo‘nalishlaridir.

Tadqiqot nimani isbotlamaydi?

• Ishlaydigan to‘liq nazariya darajasidagi avtomatik tizim yaratilganini ko‘rsatmaydi.
• Yagona oraliq ifodalash to‘g‘ridan-to‘g‘ri tarjimadan ustun ekanini eksperimental isbotlamaydi.
• Lean barcha sohalar uchun universal oraliq til bo‘la olishini to‘liq tasdiqlamaydi.
• Yangi matematik kashfiyotlar avtomatik tarzda yaratilganini da’vo qilmaydi.

Tadqiqot usuli va natijalari

Asosiy ko‘rsatkichlar

Manba va metodologiya eslatmasi

Tadqiqotning to‘liq asl nomi: Theory-Level Autoformalization: From Isolated Statements to Unified Formal Knowledge Bases

Mualliflar: Marcus J. Min; Mike He; Zhaoyu Li; Zixuan Yi; Sharad Malik; Aarti Gupta; Xujie Si; Osbert Bastani.

Muassasalar: Pensilvaniya universiteti; Prinston universiteti; Toronto universiteti.

Konferensiya: ICML 2026 (43rd International Conference on Machine Learning), Position Paper Track, Spotlight.

Nashr seriyasi: PMLR 306 (Proceedings of Machine Learning Research).

arXiv:arXiv:2607.13292

OpenReview:OpenReview yozuvi

Ushbu sharh 16 sahifalik rasmiy maqola matni va ilovalari asosida tayyorlandi. Maqolada bo‘lmagan yangi eksperimental natija qo‘shilmadi.