Ин таҳқиқот бар он аст, ки донишҳои математикӣ, илмӣ ва техникӣ, ки бо забони табиӣ ифода мешаванд, бояд на танҳо дар сатҳи теоремаҳо ё пешниҳодҳои ҷудогона, балки ҳамроҳ бо вобастагиҳои тамоми як назария ба шакле табдил дода шаванд, ки аз ҷониби мошин санҷида шавад. Муаллифон ба ҷойи таҳияи низоми нави таҷрибавӣ мақолаи мавқеъгирӣ пешниҳод мекунанд, ки лоиҳаҳои мавҷуда дар математика, илм, тасдиқи нармафзор ва сахтафзор, адабиёти автоматии формализатсия ва мушкилоти арзёбии соҳаро баррасӣ мекунад. Далели асосӣ ин аст, ки барои формализатсияи як теоремаи ҳадаф аввал аксиомаҳо, таърифҳо, ишораҳо, пешниҳодҳои ёрирасон, тактикаҳои исбот ва вобастагиҳои байни онҳо бояд ҳамчун китобхонаи мутобиқ сохта шаванд. Бо вуҷуди ин, таҳқиқот низоми нави пурраи аз аввал то охир, маҷмӯи додаҳо ё санҷиши таҷрибавие пешниҳод намекунад, ки равиши дар сатҳи назария пешниҳодшударо татбиқ кунад.

Мақола таъкид мекунад, ки аксари корҳои мавҷудаи автоматии формализатсия мавҷудияти китобхонаҳои пухтаи формалиро аллакай фарз мекунанд. Масалан, Mathlib дар муҳити Lean бисёр таърифҳо ва теоремаҳои ёрирасонро пешакӣ таъмин мекунад, бинобар ин тарҷумаи як пешниҳоди ҳадаф нисбатан идорашаванда менамояд. Аммо дар соҳаҳое чун таҳлили ададӣ, баъзе соҳаҳои муҳандисӣ, сиёсати махсуси амниятӣ ё забонҳои соҳавии махсуси муассиса, ки зерсохтори кофии формалӣ надоранд, мушкили асосӣ тарҷумаи як пешниҳод нест, балки сохтани тамоми заминаи назариявист, ки ба он пешниҳод маъно медиҳад.

Муаллифон чор мушкили асосиро дар роҳи автоматии формализатсия дар сатҳи назария муайян мекунанд: боэътимод санҷидани он ки формализатсияҳо аз ҷиҳати маъно баробар ҳастанд ё не; тақсим кардани матнҳои калон ба сохторҳои иерархии вобастагӣ ва омӯхтани абстраксияҳои аз нав истифодашаванда; мутобиқ шудан ба забонҳои камманбаи соҳавӣ берун аз Lean; ва якҷоя тафсир кардани вурудоти чандкипа ба монанди матн, ишораи математикӣ, диаграммаи вақт, схема ё тасвири озодшакл. Барои ҳалли ин масъалаҳо бошад, меъёрҳои арзёбӣ дар сатҳи назария, моделҳои умумимақсад ба ҷойи моделҳои аз ҳад ба як китобхонаи танг мутобиқшуда ва як намоиши миёнарави муштарак пешниҳод мешаванд, ки метавонад байни забонҳои гуногуни формалӣ пул созад.

Автоматии формализатсия чист?

Автоматии формализатсия (autoformalization) табдил додани донишест, ки бо забони табиӣ ё ишораҳои нимформалӣ пешниҳод шудааст, ба забони формалие, ки ёвари исбот ё санҷандаи формалӣ метавонад онро назорат кунад. Ин тарҷума танҳо бознависии синтаксисии ҷумлаҳо нест. Ифодаи формалии тавлидшуда бояд маъно, фарзияҳо, кванторҳо, истисноҳо ва вобастагиҳои матни аслиро нигоҳ дорад.

Мақола ду зервазифаи асосиро аз ҳам ҷудо мекунад:

• Автоматии формализатсияи ифода: Теорема, фарзия ё иддаои бо забони табиӣ ба изҳороти формалӣ табдил дода мешавад.
• Автоматии формализатсияи исбот: Исботи муайяни забони табиӣ бо нигоҳ доштани сохтори мантиқии он ба скрипти исботи аз ҷониби мошин санҷишаванда табдил дода мешавад.

Фарқи муҳиме, ки дар Замимаи B таъкид мешавад, ин аст, ки автоматии формализатсияи исбот бо исботи умумии теорема як чиз нест. Исботкунандаи формалии теорема метавонад ҳар гуна исботи дурустеро ҷустуҷӯ кунад, ки пешниҳоди ҳадафро тасдиқ мекунад. Аммо автоматии формализатсияи исбот бояд ба ҷараёни мушаххаси фикри исботи аслии забони табиӣ содиқ монад. Барои як теорема ду исботи гуногуни формалӣ метавонанд дуруст бошанд, аммо танҳо яке аз онҳо метавонад сохтори мантиқии далели аслии тарҷумашавандаро инъикос кунад.

Автоматии формализатсия дар сатҳи назария чиро тағйир медиҳад?

Мувофиқи таърифи муаллифон, автоматии формализатсия дар сатҳи назария сохтани аксиомаҳо, таърифҳо, ишораҳо, мисолҳо, пешниҳодҳои ёрирасон, теоремаҳо, исботҳо, тактикаҳо ва ҳамаи вобастагиҳои байни онҳо дар як доираи муайян ҳамчун китобхонаи ягонаи формалӣ мебошад. Ин равиш ба ҷойи тарҷумаи ифодаҳои ҳадафи ҷудогона, ҳадаф дорад меъмории донишеро созад, ки ин ифодаҳо бар он такя мекунанд.

«Бурҷи автоматии формализатсия дар сатҳи назария» дар Шакли 2 сохтори чорқабатаро бо мисоли геометрияи Евклид нишон медиҳад:

Мувофиқи натиҷае, ки дар мақола оварда шудааст, яке аз беҳтарин усулҳои мавҷуда дар ифодаҳои Қабати 3, бо фарз кардани он ки қабатҳои поёнӣ аз ҷониби одамон пешакӣ формализатсия шудаанд, ба %71,4 муваффақият мерасад. Аммо муаллифон мегӯянд, ки усулҳои мавҷуда ҳанӯз сохтани тамоми зерсохтори Қабатҳои 0–2-ро аз сифр ба таври автоматӣ ҳадаф нагирифтаанд. Аз ин рӯ, қимати %71,4 набояд ҳамчун сатҳи автоматии формализатсияи тамоми як назария тафсир шавад.

Чаро тарҷумаи як теорема кофӣ нест?

Як теоремаи ҳадаф дар муҳити формалӣ ба зерсохтори хеле васеътар аз он чизе, ки зоҳиран менамояд, такя мекунад. Навъи ҳар объекти дар теорема истифодашуда, маънои ҳар муносибат, ишораҳои истифодашаванда, натиҷаҳои ёрирасон ва қадамҳои исбот бояд пешакӣ таъриф шуда бошанд. Бисёр донишҳое, ки мутахассисон дар забони табиӣ ғайримустақим мегузоранд, дар низоми формалӣ бояд ошкоро гуфта шаванд.

Масалан, математик метавонад аз замина робитаи мафҳуми «мураббаъ»-ро бо хосиятҳои росткунҷа ва ромб фаҳмад. Дар низоми формалӣ бошад, таърифҳо ё теоремаҳои таъминкунандаи ин робита бояд дар китобхона мавҷуд бошанд. Ба ҳамин монанд, муҳандиси сахтафзор метавонад аз диаграммаи вақт бифаҳмад, ки сигнал бояд «аз даври навбатӣ сар карда устувор монад»; аммо дар хусусияти формалӣ оператори «даври навбатӣ» бояд ошкоро навишта шавад.

Чаро автоматии формализатсия муҳим аст?

Тавлиди додаҳо барои исботкунандагони нейронии теорема

Рушди низомҳои нейронии исботи теорема ба маҷмӯаҳои бузург ва боэътимоди додаҳои формалӣ вобаста аст. Тавлиди ҳамтоҳои формалии матнҳо ва исботҳои математикӣ бо забони табиӣ метавонад додаҳои омӯзишии параллелӣ байни забони табиӣ ва забони формалӣ эҷод кунад. Формализатсияи ифода ҳадафҳои нав тавлид мекунад, дар ҳоле ки формализатсияи исбот қадамҳои исботи мустақиман санҷишавандаро медиҳад.

Суръат бахшидан ба тасдиқи назариявӣ ва муҳандисӣ

Лоиҳаҳои тасдиқи формалӣ танҳо теорема ё низоми ниҳоиро санҷиш намекунанд; онҳо китобхонаи васеъ аз таърифҳо, натиҷаҳои миёна ва зерсохтори техникӣ месозанд. Дар Ҷадвали 1 нишон дода шудааст, ки лоиҳаҳои интихобшуда аз математика, илм, нармафзор ва сахтафзор вақти назаррас ва меҳнати мутахассис талаб кардаанд:

Паёми асосии ҷадвал ин аст, ки хароҷоти асосӣ дар тасдиқи формалӣ аксаран ёфтани як исбот нест, балки сохтани тамоми шабакаи таърифҳо ва натиҷаҳои ёрирасонест, ки ҳадаф дар он сохта мешавад. Мақола ҳамчун мисол меорад, ки формализатсияи теоремаи ададҳои аввал аз ҷониби инсон тақрибан 1,5 сол тӯл кашида, беҳбудии миқдорие бо дастгирии зеҳни сунъӣ дар се ҳафта формализатсия шудааст. Аммо доираи ин ду кор яксон нест ва вақтҳо набояд ҳамчун меъёрҳои мустақиман баробари лоиҳа муқоиса шаванд.

Асоснок ва роҳнамоӣ кардани мулоҳизаи забони табиӣ

Мулоҳизаҳое, ки моделҳои бузурги забонӣ бо забони табиӣ тавлид мекунанд, метавонанд пешфарзҳои номувофиқ, фарзияҳои вуҷуднадошта ё қадамҳои партофташударо дар бар гиранд. Санҷандаи формалӣ метавонад таърифҳои навъи нодуруст, зиддиятҳо ё қадамҳои тасдиқнашавандаро муайян кунад. Бо ҷудокунии истифодашуда дар мақола, «асосноккунӣ» аз байн бурдани қадамҳои нодуруст ва «роҳнамоӣ» истифодаи бозхӯрди санҷанда барои ислоҳи баромади худи модел мебошад.

Ҳамин фоида барои инсонҳо низ дахл дорад. Исботҳои забони табиӣ метавонанд қадамҳои маъмулро гузаранд, ҳолатҳои сарҳадии ҳассосро кофӣ шарҳ надиҳанд ё фарзияҳои нолозим дошта бошанд. Формализатсия метавонад ин камбудиҳоро намоён кунад. Бо вуҷуди ин, мақола ҷонибдори он нест, ки тасдиқи формалӣ мулоҳизаи забони табииро пурра иваз кунад, балки онро такмил диҳад.

Саҳм ба қобилиятҳои умумии мулоҳиза

Муаллифон баҳс мекунанд, ки бозхӯрди санҷишшаванда аз санҷандаи формалӣ метавонад рафторҳоеро омӯзонад, ки ба вазифаҳои мулоҳиза берун аз математика низ интиқол ёбанд. Ин иддао маънои онро надорад, ки омӯзиши формализатсияи математикӣ ба таври автоматӣ зеҳни умумиро эҷод кардааст. Мақола робитаҳои иҷроиш байни соҳаҳои гуногуни мулоҳиза ва корҳои омӯзишӣ бо мукофотҳои санҷишшавандаро ҳамчун нишонаҳои дастгиркунандаи ин самти таҳқиқот истифода мебарад.

Чаро лоиҳаҳои воқеии формализатсия дар сатҳи назария ҳастанд?

Гарчанде фарзияи Кеплер як иддаои математикӣ аст, тасдиқи формалии он сохтани садҳо таъриф ва пешниҳоди ёрирасонро талаб кардааст. Дар лоиҳаҳое мисли Liquid Tensor Experiment низ барои он ки теоремаи ҳадаф ифода шавад, қисмҳои муҳими математикаи конденсатсионӣ аввал дар муҳити Lean сохта шудаанд. Ин мисолҳо нишон медиҳанд, ки лоиҳаҳои воқеӣ кори «тарҷумаи як ҷумла ба забони дигар» нестанд.

Далели дуюми муаллифон ин аст, ки усулҳои сатҳи ифода ба китобхонаҳои пухта вобастаанд. Манбаъҳое мисли Lean Mathlib миқдори зиёди зерсохтори аз ҷониби инсон навишташударо дар алгебра, таҳлил, назарияи ададҳо ва соҳаҳои гуногуни математикаи асосӣ таъмин мекунанд. Агар соҳа дар Mathlib ба қадри кофӣ намояндагӣ нашуда бошад, пеш аз тарҷумаи ифодаи ҳадаф бояд таърифҳо ва теоремаҳои ёрирасони норасо сохта шаванд.

Далели сеюм ин аст, ки кашфи назариявӣ ба абстраксияҳои нав такя мекунад. Сохторҳои алгебравӣ мисли гурӯҳ, ҳалқа ва майдон ё равиши морфизм-марказ дар назарияи категория донишҳои қаблан ҷудогонаро зери сохтори умумӣ ҷамъ овардаанд. Мақола пешниҳод мекунад, ки дар оянда тавассути аз нав ташкил кардани пойгоҳҳои бузурги формалии дониш сохторҳои муштараки байни соҳаҳои гуногун пайдо шаванд ва абстраксияҳои нав кашфи назариявиро осон кунанд. Ин натиҷаи дар таҳқиқот татбиқшуда ё таҷрибавӣ нишон додашуда нест, балки диди дарозмуддати таҳқиқот аст.

Назари алтернативӣ ва ҷавобҳои муаллифон

Назари «мулоҳизаи забони табиӣ кофист»

Забони табиӣ чандир аст, зеро синтаксиси махсус талаб намекунад ва додаҳои омӯзишии хеле васеътар дорад. Моделҳои қавӣ метавонанд масъалаҳои душвори математикиро бо забони табиӣ ҳал кунанд. Муаллифон дар ҷавоб се бартарии такмилдиҳандаи усулҳои формалиро пешниҳод мекунанд: бозхӯрди аз ҷониби мошин санҷишшаванда, эътимоди модулӣ дар гурӯҳҳои калон бе аз нав хондани ҳар ҷузъиёти кор ва имкони миқёспазирӣ на танҳо бо омӯзиш, балки бо ҷустуҷӯ.

Назари «афзалият бояд ба исботи теорема дода шавад»

Исботи теорема барои ҳадафи формалии додашуда исботи дурустро меҷӯяд. Аммо пешниҳоди ҳадаф ва хусусиятҳои система бояд аввал ба таври формалӣ навишта шаванд. Масалан, дар тасдиқи сахтафзор, ҳатто агар санҷандаҳои модел ба қадри кофӣ пухта бошанд, то хусусиятҳоро бисанҷанд, дуруст ифода кардани он ки кадом хусусият бояд санҷида шавад, метавонад тангнои асосӣ бошад. Ба гуфтаи муаллифон, автоматии формализатсия ҳадафҳои маънодореро тавлид мекунад, ки исботкунандаи теорема бар онҳо кор мекунад.

Назари «беҳтар кардани усулҳои сатҳи ифода воқеӣтар аст»

Усулҳои сатҳи ифода маҷмӯаҳои додаҳои ченшаванда ва мисолҳои муваффақ доранд. Дар баъзе ҳамкориҳои инсон–зеҳни сунъӣ мутахассисон аввал «нақша» ё графи вобастагии ҷузъӣ омода мекунанд ва модел пешниҳодҳои ёрирасонро пайдарпай формализатсия мекунад. Муаллифон ин равишро «нимсатҳи назария» мешуморанд; зеро сохтани сохтори вобастагӣ ҳанӯз ба мутахассисон вогузор мешавад ва таърифҳои асосӣ аксаран аз Mathlib гирифта мешаванд.

Мушкилоти кушодаи аввал: Баробармаъноӣ чӣ гуна санҷида мешавад?

Дар автоматии формализатсия танҳо компилятсия шудани коди тавлидшуда кофӣ нест. Ифодаи формалӣ метавонад дуруст бошад, аммо чизеро ифода кунад, ки аз маънои аслии забони табиӣ фарқ дорад. Аз ин рӯ саволи асосии арзёбӣ ин аст, ки оё ду ифода як маъно доранд ё не.

Норасоии додаҳои боэътимоди истинодӣ

Тибқи санҷишҳои овардашуда дар мақола, дар 118 аз 371 масъалаи маҷмӯи додаҳои ProofNet хатои формализатсияи инсонӣ пайдо ва ислоҳ шудааст; ин таносуб %31,8 мебошад. Дар PutnamBench бошад, пас аз нашр дар ҳадди ақал 58 аз 672 формализатсияи Lean хато ислоҳ шудааст ва сатҳи гузоришшудаи хато %8,6 будааст. Муаллифон ҳамчунин мегӯянд, ки маҷмӯаҳои додаҳои махсус барои формализатсияи таъриф танҳо бо 56 таърифи Wikipedia ва 30 таърифи arXiv маҳдуданд; ProofFlowBench бошад дар баробари исботҳо 184 ифодаи сатҳи бакалавриро дар бар мегирад. Дар марҳилаи омода кардани мақола гуфта шудааст, ки меъёре барои арзёбии тамоми як назария вуҷуд надошт.

Масъалаи баробарии синтаксисӣ, баробармаъноии мантиқӣ ва замина

Ду ифодаи зерин як мундариҷаи математикӣ доранд:

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

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

Дар ин ҷо n адади табиӣ ва P хусусияте мебошад, ки бар ададҳои табиӣ таъриф шудааст. Ифодаи аввал маънои «ҳамаи ададҳои табиӣ хусусияти P доранд»-ро медиҳад, дуюм бошад «ягон адади табиие вуҷуд надорад, ки хусусияти P надошта бошад». Азбаски синтаксисашон фарқ мекунад, мувофиқати пурраи матн онҳоро яксон намешуморад; аммо аз ҷиҳати мантиқӣ баробармаъно ҳастанд.

Баръакс, баробармаъноии зерин на танҳо аз сохтори мантиқӣ, балки аз таърифҳо ва теоремаҳои геометрияи Евклид бармеояд:

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

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

a объекти геометрии мавриди баррасист. Дар назарияи мувофиқи геометрия, ҳам росткунҷа ва ҳам ромб будани объект боиси мураббаъ будани он мегардад. Аммо агар «росткунҷа», «ромб» ва «мураббаъ» ҳамчун муносибатҳои мантиқии ихтиёрӣ бе маънои муайян гирифта шаванд, ин натиҷа ба даст намеояд. Барои арзёбии баробармаъноӣ бояд муайян карда шавад, ки кадом назарияи замина истифода мешавад.

Чаро баробармаъноии таърифӣ танҳо кофӣ нест?

Ёварони исбот мисли Lean метавонанд бо кушодани таърифҳо баъзе ифодаҳоро мустақиман содда кунанд. Аммо аз сабаби самти рекурсивии таърифи ҷамъкунии ададҳои табиӣ, ифодаҳои зерин метавонанд ба як шакл коҳиш наёбанд:

[ m + 0 ]

[ 0 + m ]

m адади табиӣ аст ва воҳиди физикӣ надорад. Ифодаи аввал аз рӯи таъриф метавонад мустақиман ба m коҳиш ёбад, дар ҳоле ки ифодаи дуюм метавонад дар тағйирёбандаи абстрактӣ бимонад. Барои исботи баробарии дуюм бояд ба натиҷаҳои ёрирасони исботшуда, мисли хосияти коммутативии ҷамъкунӣ, муроҷиат кард.

Хатари баробармаъноии номаҳдуди пешниҳодҳо

Ҳамчунин боэътимод нест, ки ҳар ду пешниҳоди дуруст дар назарияи замина баробармаъно ҳисобида шаванд. Ин равиш метавонад ду пешниҳоди мазмунан тамоман гуногун, мисли «1 + 1 = 2» ва Теоремаи Охирини Ферма, баробармаъно шуморад. Санҷандаи BEq+ дар мақола бо маҳдуд кардани заминаи глобалӣ ва ҷустуҷӯи умумии исбот %98,0 дақиқӣ ва %48,3 ҳассосият ба даст меорад. Барои баробармаъноии софи таърифӣ бошад, арзишҳо %100 дақиқӣ ва %30,9 ҳассосият дода шудаанд.

Бо вуҷуди ин, шарти дуҷонибаи ду хусусияти гуногуни дурусти зерин метавонад вақте тактикаҳои автоматӣ ҳар ду тарафро мустақилона осон исбот мекунанд, таассуроти баробармаъноии нодуруст эҷод кунад:

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

Ҳар ду пешниҳод барои ададҳои табиӣ дурустанд, аммо яке ба элементи воҳидии зарб ва дигаре ба элементи воҳидии ҷамъ дахл дорад. Аз ҷиҳати маънои аслии формализатсияшаванда онҳо як хусусият нестанд.

Ҳадди субъективии баробармаъноӣ

Яке аз мисолҳои ҷолиби мақола интеграли зерин аст:

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

Шакли зерин, ки бо истифода аз хосияти коммутативии ҷамъкунӣ навишта шудааст, барои аксари хонандагон равшанан ҳамон маъноро дорад:

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

Вақте қимати интеграл ҳисоб карда мешавад, натиҷа метавонад ба ифодаи зерин низ коҳиш ёбад:

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

x тағйирёбандаи интегратсияи математикии бевоҳа аст, ки байни 0 ва 1 тағйир меёбад; мисол ченкунии физикӣ нест. Ду ифодаи аввал зоҳиран хеле монанданд, дар ҳоле ки ифодаи сеюм танҳо пас аз иҷрои интегратсия ҳамон натиҷаро медиҳад. Низоми арзёбӣ бояд то чӣ андоза ҳисоб кунад? Тибқи далели мақола, дараҷаи даркшудаи баробармаъноӣ вобаста ба дониш ва қобилияти ҳисоббарории арзёб тағйир мекунад.

Ҳолати сарҳадӣ бо айнияти алгебравии зерин боз ҳам равшантар мешавад:

\[ (x-1)^2 + 2x = x^2 + 1 \]

Барои шахсе, ки ин баробариро зуд мебинад, баробармаъноии интегралҳо равшан аст; барои арзёби дигар кушодан ва содда кардан лозим мешавад. Аз ин рӯ ҳар санҷандаи баробармаъноӣ бояд барои ҳаҷми ҳисоб ва дониши заминае, ки иҷозат медиҳад, остонае интихоб кунад.

Мушкилоти кушодаи дуюм: Ҷудокунии иерархӣ ва омӯзиши абстраксия

Формализатсияи як китоби дарсии дароз бештар аз тақсим кардани матн ба ҷумлаҳои мустақил талаб мекунад. Низом бояд муайян кунад, ки кадом таъриф бояд пештар ояд, кадом теорема ба кадом натиҷаҳои ёрирасон такя мекунад ва кадом мафҳумҳо метавонанд зери як абстраксияи аз нав истифодашаванда муттаҳид шаванд.

Усулҳои ҷудо кардани ҳадафҳои зерини исботи теорема пешрафти назаррас нишон додаанд. Дар мақола оварда шудааст, ки DeepSeek-Prover-V2 дар miniF2F %88,9 ва BFS-Prover-V2 %95,1 муваффақият гузориш кардаанд. Аммо ин низомҳо одатан як исботи ҳадафи ягонаеро ба зерҳадафҳо ҷудо мекунанд. Вазифаи сатҳи назария бошад, сохторбандии тамоми китобҳои дарсӣ ё ҳуҷҷатҳои техникиро талаб мекунад, ки даҳҳо теоремаи асосӣ ва вобастагиҳои амиқ дарҳампечида доранд.

Омӯзиши абстраксия ду вазифаи ҷудогона дорад:

1. Формализатсияи таъриф: Ёфтани мафҳумҳои такроршаванда дар матн ва табдил додани онҳо ба таърифҳои формалии аз нав истифодашаванда.
2. Фишурдани дониш: Кашфи сохторҳои умумӣ дар китобхонаҳои калони формалии мавҷуда барои сохтани абстраксияҳои кӯтоҳтар, модулитар ва умумитар.

Муаллифон бар онанд, ки дар марҳилаи истихроҷи мафҳум аз корпуси забони табиӣ агентҳои моделҳои умумимақсади забонӣ; ва пас аз сохтани китобхонаи формалӣ усулҳои рамзие, ки сохторҳои умумии кодро меомӯзанд, мувофиқтар буда метавонанд. Бо вуҷуди ин, аксари корҳои мавҷуда бо муносибатҳои математикии таркибӣ маҳдуданд; сохтани автоматии таърифҳои аксиоматикӣ ё алгоритмӣ то ҳадди зиёд ҳалношуда мондааст.

Мушкилоти кушодаи сеюм: Забонҳои камманбаи соҳавӣ берун аз Lean

Тасдиқи формалӣ дар ҷаҳони воқеӣ танҳо бо Lean анҷом дода намешавад. Муассисаҳо барои ҳалли маҳдудиятҳо, тасдиқи протокол, хусусиятҳои сахтафзор, таҳлили статикии амният ва сиёсати дастрасӣ забонҳои махсуси соҳавиро истифода мебаранд. Дар аксари ин забонҳо маҷмӯаҳои бузурги додаҳо бо ҷуфтҳои забони табиӣ–забони формалӣ вуҷуд надоранд.

Забонҳои автоматии исботи теорема

Ҳалкунандаҳои SMT шаклҳои монанди SMT-LIB ва исботкунандагони теоремаи тартиби аввал шаклҳои монанди TPTP-ро истифода мебаранд. Шакли 3 табдили хусусияти зеринро барои амали партофтани унсурҳо аз рӯйхат аз забони табиӣ ба формалӣ нишон медиҳад:

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

Дар ин ҷо L рӯйхат ва x ва w шумораи унсурҳои аз аввали рӯйхат хориҷшавандаро ифода мекунанд; воҳиди физикӣ надоранд. Ифода мегӯяд, ки аввал x ва баъд w унсурро партофтан ба он баробар аст, ки дар як қадам ҷамъан x+w унсур партофта шавад. Гарчанде маҷмӯи додаҳои Tons of Inductive Problems ифодаҳои формалӣ дорад, набудани ҳамтоҳои забони табиӣ тавлиди додаҳои параллелиро душвор мекунад.

Забонҳои тасдиқи протоколҳои тақсимшуда

Забонҳое мисли Ivy ва PVerifier месанҷанд, ки протоколҳои тақсимшуда дар ҳамаи ҳолатҳои дастрас хусусиятҳои амниятиро нигоҳ медоранд ё не. Дар Шакли 4 тавсифи забони табиии протоколи интихоби роҳбари Chang–Roberts ҳамроҳ бо топологияи ҳалқа, роҳбари ибтидоӣ, шиносаҳои гиреҳҳо ва амалҳои фиристодани паём ба модели формалӣ табдил дода мешавад. Танҳо 54 исботи протоколи формализатсияшуда доштани IvyBench камбуди додаҳо дар ин соҳаро нишон медиҳад.

Забонҳои тасдиқи сахтафзор

Хусусиятҳои сахтафзор метавонанд бо забонҳое мисли SystemVerilog Assertions тавассути рафтори сигналҳо дар вақт ифода шаванд. Дар Шакли 5 бояд ҳуҷҷати тарроҳии матнӣ ва диаграммаи вақт якҷоя хонда шаванд. Ифодаи «маълумоти назорати манбаъ устувор мемонад» дар ҳуҷҷат танҳо тавассути диаграммаи вақт ошкор мекунад, ки устуворӣ аз даври навбатии соат эътибор дорад.

Хусусияти формалӣ дар шакл чунин сохтор дорад:

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

VALID дуруст будани маълумот, READY омода будани қабулкунанда барои қабул, INFO маълумоти назорат ва ##1 даври навбатиро нишон медиҳад. Бе тафсири якҷояи матн ва диаграмма робитаи вақтии ##1 метавонад нодида монад. Ин мисол нишон медиҳад, ки автоматии формализатсияи дуруст на танҳо коркарди матн, балки мулоҳизаи байни кипҳоро талаб мекунад.

Забонҳои барномасозии декларативӣ

Дар Замимаи A шарҳ дода мешавад, ки чаро забонҳои декларативӣ мисли SQL, Cypher, CodeQL ва Cedar ба доираи автоматии формализатсия дохил мешаванд. Ин забонҳо на «чӣ гуна ҳисоб кардан», балки «кадом шарт бояд иҷро шавад»-ро изҳор мекунанд. Табдил додани талаботи забони табиӣ ба сиёсати Cedar бештар интиқоли маънои мавҷуда ба маҳдудиятҳои формалӣ аст, на тарҳрезии алгоритми нав.

Баръакс, тарҷума ба забонҳои амрии барномасозӣ мисли Python ё C++ ҷузъиёти татбиқиро илова мекунад, ки дар матни аслӣ нестанд, аз ҷумла сохтори додаҳо, ҷараёни назорат, алгоритм ва интихоби амният. Аз ин рӯ мақола синтези барномаҳои амриро на ҳамчун тарҷумаи нигоҳдорандаи маъно, балки ҳамчун вазифаи тавлидӣ тасниф мекунад.

Натиҷаҳои мисолие, ки барои забонҳои декларативӣ оварда шудаанд, чунинанд:

Дар Шакли 6 нишон дода мешавад, ки муқаррароти ҷудогонаи HIPAA дар бораи дастрасии бемор, намояндагони шахсӣ ва ноболиғон бо тағйирёбандаҳо ва шартҳои муштараки Cedar якҷоя формализатсия мешаванд. Дар матни садҳо саҳифаи ҳуқуқӣ муқаррарот, истисноҳо ва истинодҳои байниҳамдигарӣ ба ҳам вобастаанд. Муваффақияти мисолҳои ҷудогона дар сатҳи параграф маънои онро надорад, ки тамоми муқаррарот ба таври мутобиқ тарҷума шудааст.

Мушкилоти кушодаи чорум: Вурудоти чандкипа берун аз матн

Мақола дар вазифаҳои воқеии формализатсия чор навъи вурудро муайян мекунад:

• Тавсифҳои забони табиӣ ва ҳуҷҷатҳои техникӣ
• Ишораҳои математикӣ ё забонҳои формалии мавҷуда
• Диаграммаҳои вақт, схемаҳо, мошинҳои ҳолат ва нақшаҳои ҷараён
• Тасвирҳои озодшакл мисли расмҳои геометрӣ ё мисолҳои интерфейси корбар

Дар геометрия байни нуқтаҳо будан ё буриши хатҳо дар расм табиатан дида мешавад, дар ҳоле ки дар матн метавонад таърифи муфассал талаб кунад. Дар сахтафзор диаграммаҳои вақт, дар протоколҳо мошинҳои ҳолат ва дар нармафзор мисолҳои интерфейс метавонанд қисми муҳими мундариҷаи формалиро дошта бошанд. Низоми сатҳи назария бояд зиддиятҳоро байни ин манбаъҳо муайян кунад, фарзияҳои ғайримустақимро ошкор созад ва ҳамаи онҳоро дар як намоиши ягонаи мутобиқ муттаҳид намояд.

Пешниҳоди 1: Меъёрҳои боэътимоди арзёбӣ дар сатҳи назария

Танзими идеалии арзёбии сатҳи назария, ки муаллифон пешниҳод мекунанд, бояд се шартро иҷро кунад:

1. На танҳо ифодаҳои ҳадаф, балки таърифҳо ва вобастагиҳои назарияи заминаро низ фаро гирад.
2. Дақиқӣ ва ҳассосияти санҷандаи баробармаъноӣ нисбат ба арзёбии мутахассисон гузориш шавад.
3. Мавҷуд будани назарияи заминае, ки модел дар он санҷида мешавад, дар додаҳои омӯзишӣ пешгирӣ ё ошкоро назорат карда шавад.

Дар кӯтоҳмуддат сохтани маҷмӯаҳои додаҳои мувофиқ, дар миёнамуддат муқоисаи вақти формализатсия бо ва бе кӯмаки зеҳни сунъӣ ҳамроҳ бо меҳнати мутахассис ва дар дарозмуддат санҷидани он ки оё намоиши миёнарави муштарак воқеан нисбат ба формализатсияи мустақим бартарӣ дорад, пешниҳод мешавад.

Пешниҳоди 2: Моделҳои умумимақсад ба ҷойи моделҳои танги ихтисосӣ

Мувофиқи мисоли овардашуда дар мақола, Goedel-Formalizer-V2-32B дар маҷмӯи додаҳои LeanEuclidPlus берун аз Mathlib %0,0 муваффақият нишон додааст, дар ҳоле ки модели асосии Qwen3-32B аз ҳамон оилаи модел %20,6 ба даст овардааст. Муаллифон ин мисолро ҳамчун хатари умумият надоштани низомҳое тафсир мекунанд, ки ба қолабҳои як китобхона аз ҳад зиёд fine-tune шудаанд.

Равиши пешниҳодшуда моделҳои умумимақсадеро, ки бо додаҳои якчанд забон ва соҳаи формалӣ омӯзонида шудаанд, бо усулҳое мисли бозхӯрди санҷанда, дастрасии вобастагӣ, ислоҳи такрорӣ ва ҷустуҷӯ дар вақти inference дастгирӣ мекунад. «Умумимақсадӣ» дар ин ҷо на танҳо меъмории модел, балки омехтаи додаҳои омӯзишӣ, тарҳи мукофот ва доираи арзёбиро низ дар бар мегирад.

Пешниҳоди 3: Намоиши миёнарави муштарак

Шакли 7 меъмориеро пешниҳод мекунад, ки дар он забони табиӣ, забони формалӣ, диаграмма ва тасвир аввал ба як намоиши миёнарави муштарак табдил дода мешаванд ва баъдан ин намоиш ба забонҳои гуногуни соҳавӣ ба таври санҷишшаванда интиқол меёбад. Ҳамин шакл агентҳои модели умумимақсади чандкипа ва меъёрҳои сатҳи назария бо санҷандаи боэътимоди баробармаъноиро низ ҳамчун қисмҳои ин ҷараён нишон медиҳад.

Намоиши миёнарави муштарак се шарти тарроҳӣ дорад:

• Қудрати ифода: Бояд маъноҳои забонҳои гуногуни соҳавиро намояндагӣ карда тавонад.
• Санҷишпазирӣ: Дар дохили худи намоиши миёнарав бояд санҷиши навъ ва санҷиши исбот имконпазир бошад.
• Имкони ҷойгиркунӣ: Забонҳои ҳадафи соҳавӣ бояд ба қадри кофӣ амиқ дар намоиши миёнарав ҷойгир карда шаванд ва табдил санҷида шавад.

Муаллифон Lean-ро бинобар назарияи навъҳои вобаста, санҷандаи навъи дарунсохт ва имкониятҳои meta-programming ҳамчун номзади табиӣ нишон медиҳанд. Аммо ин пешниҳод маънои онро надорад, ки Lean ба таври таҷрибавӣ ҳамчун беҳтарин намоиши муштарак барои ҳамаи забонҳои соҳавӣ исбот шудааст. Хусусан барои вақтбандии сахтафзор, сиёсати ҳуқуқӣ, ҳолатҳои протокол ва забонҳои махсуси муассисавӣ қудрати ифода ва корбурди амалӣ бояд алоҳида арзёбӣ шавад.

Натиҷаҳое, ки таҳқиқот дастгирӣ мекунад

• Лоиҳаҳои воқеии тасдиқи формалӣ зерсохтори хеле васеътари таърифҳо ва натиҷаҳои ёрирасонро аз тарҷумаи ифодаҳои ҳадаф талаб мекунанд.
• Усулҳои мавҷудаи сатҳи ифода аксаран ба китобхонаҳои формалии аз ҷониби инсон омодашуда ва тарҳҳои вобастагӣ такя мекунанд.
• Арзёбии баробармаъноӣ масъалаест, ки танҳо бо мувофиқати синтаксисӣ ҳал намешавад ва ба назарияи замина вобаста аст.
• Забонҳои камманбаи соҳавӣ ва ҳуҷҷатҳои техникии чандкипа мушкилоти дигар аз маҷмӯаҳои додаҳои математикии Lean-марказ доранд.
• Маҷмӯаҳои додаҳои сатҳи назария, моделҳои умумимақсад ва намоиши миёнарави муштарак самтҳои мушаххаси таҳқиқотӣ мебошанд, ки бояд омӯхта шаванд.

Натиҷаҳое, ки таҳқиқот исбот ё санҷиш накардааст

• Мақола низоми коркунандаи пурраи автоматии формализатсияи сатҳи назария аз аввал то охирро пешниҳод намекунад.
• Ба таври таҷрибавӣ нишон дода нашудааст, ки намоиши миёнарави пешниҳодшуда аз тарҷумаи мустақим муваффақтар аст.
• Исбот нашудааст, ки Lean забони универсалии миёнарав барои ҳамаи соҳаҳои математикӣ, ҳуқуқӣ, нармафзорӣ ва сахтафзорӣ мебошад.
• Нишон дода нашудааст, ки автоматии формализатсия дар сатҳи назария кашфиёти нави математикиро ба таври автоматӣ тавлид мекунад.
• Азбаски иҷроишҳои моделии овардашуда маҷмӯаҳои додаҳо ва меъёрҳои арзёбии гуногунро истифода мебаранд, онҳоро набояд ҳамчун як рейтинги ягона тафсир кард.
• Тасдиқи формалӣ ҳамаи номуайяниҳо ё номувофиқиҳои семантикиро дар мулоҳизаи забони табиӣ худ аз худ бартараф намекунад.

Маъно аз ҷиҳати гузашта, имрӯз ва оянда

Лоиҳаҳои бузурги формализатсияи гузашта боэътимодии дониши аз ҷониби мошин санҷишшавандаро нишон додаанд, аммо солҳои зиёд меҳнати мутахассис талаб кардаанд. Имрӯз моделҳои бузурги забонӣ метавонанд вазифаҳое мисли тарҷума байни забони табиӣ ва формалӣ, ёфтани вобастагӣ ва таъмири исботро қисман автоматӣ кунанд. Саҳми мақола васеъ кардани ҳадафи таҳқиқот аз сатҳи муваффақияти ифодаҳои ҷудогона ба сохтани тамоми меъмории дониш мебошад.

Агар ин равиш дар оянда муваффақ шавад, китобҳои дарсии математикӣ, стандартҳои техникӣ, сиёсати амниятӣ, протоколҳои низомҳои тақсимшуда ва ҳуҷҷатҳои тарроҳии сахтафзор метавонанд ба китобхонаҳои формалии бештар санҷишшаванда табдил дода шаванд. Ин имконият барои боэътимодии нармафзор ва сахтафзор, тасдиқи низомҳои муҳим, идоракунии дониши математикӣ ва санҷишпазирии мулоҳизаи зеҳни сунъӣ аҳамият дорад. Аммо барои татбиқи воқеӣ бояд масъалаҳои миқёспазирӣ, садоқати маъно, ихроҷи додаҳо, тафсири чандкипа ва назорати мутахассис ҳал карда шаванд.

Усул ва натиҷаҳои таҳқиқот

Тарҳи таҳқиқот

Ин кор таҳқиқоти таҷрибавӣ, таҳқиқоти клиникӣ, таҷрибаи симулятсионӣ ё муқоисаи модели нав нест. Ин мақолаи мавқеъгирӣ мебошад, ки барои ICML Position Paper Track омода шудааст. Усул ба гурӯҳбандии консептуалии адабиёти мавҷудаи автоматии формализатсия, муқоисаи лоиҳаҳои тасдиқи формалӣ дар соҳаҳои гуногун, баҳси назари алтернативӣ, муайян кардани мушкилоти кушода ва таҳияи пешниҳодҳои таҳқиқотӣ такя мекунад.

Додаҳо, намуна ва таҳлили оморӣ

• Маҷмӯи нави додаҳои таҷрибавӣ сохта нашудааст.
• Иштирокчии инсонӣ, бемор, ҳайвон, ҳуҷайра, намунаи физикӣ ё гурӯҳи назоратӣ вуҷуд надорад.
• Ҷудокунии омӯзиш, санҷиш ва test барои модел анҷом дода нашудааст.
• Алгоритми нав омӯзонида ё иҷро карда нашудааст.
• Санҷиши фарзияи оморӣ, қимати p, фосилаи эътимод ё остонаи аҳамият гузориш нашудааст.
• Натиҷаҳои рақамӣ натиҷаҳои гузоришшудаи корҳои пешина ва маҷмӯаҳои додаҳое мебошанд, ки дар мақола баррасӣ шудаанд.

Нишондиҳандаҳои асосии миқдорӣ

Паёми методологии шаклҳо

• Шакли 1: Далели чорқисмаи мақоларо ҳамчун аҳамият, назари алтернативӣ, мушкилоти кушода ва даъват ба ҳал ҷамъбаст мекунад.
• Шакли 2: Сохтори вобастагии назариявии чорқабатаро аз аксиомаҳо то исботҳои ҳадаф нишон медиҳад.
• Шакли 3: Табдили ифодаи забони табиӣ дар бораи амали рӯйхат ба сохтори формалии монанд ба SMT-ро нишон медиҳад.
• Шакли 4: Моделсозии протоколи интихоби роҳбар дар топологияи ҳалқа бо аксиомаҳо, муносибатҳо ва амалҳоро нишон медиҳад.
• Шакли 5: Нишон медиҳад, ки барои тарҷумаи дурусти хусусияти сахтафзор матн ва диаграммаи вақт бояд якҷоя хонда шаванд.
• Шакли 6: Нишон медиҳад, ки муқаррароти гуногуни HIPAA тавассути шартҳои муштарак дар як сохтори сиёсати Cedar муттаҳид мешаванд.
• Шакли 7: Пешниҳоди табдили санҷишшавандаро аз вурудоти чандкипа ба намоиши миёнарави муштарак ва аз он ҷо ба забонҳои гуногуни соҳавӣ ҷамъбаст мекунад.

Натиҷаи асосӣ ва ҳудуди тафсир

Натиҷаи асосии таҳқиқот қимати таҷрибавии иҷроиш нест, балки як далели марбут ба рӯзномаи таҳқиқот аст: барои он ки автоматии формализатсия дар ҷаҳони воқеӣ миқёспазир шавад, бояд аз ифодаҳои ҳадафи ҷудогона ба сохтани тамоми назарияҳо гузарад. Муаллифон нишон медиҳанд, ки усулҳои мавҷуда зерсохтори таъриф, вобастагӣ, ишора ва исботҳои ёрирасонро асосан ба инсонҳо ё китобхонаҳои пухта вогузор мекунанд.

Ин натиҷа маънои онро надорад, ки низомҳои сатҳи назария имрӯз барои истифода омодаанд. Пешниҳодҳои мақола — меъёрҳои боэътимод, моделҳои умумимақсад ва намоиши миёнарави муштарак — самтҳои таҳқиқотие мебошанд, ки бояд дар оянда таҳия ва санҷида шаванд.

Ёддошт оид ба манбаъ ва усул

• Номи пурраи аслии таҳқиқот: Theory-Level Autoformalization: From Isolated Statements to Unified Formal Knowledge Bases
• Муаллифон ва тартиб: Marcus J. Min; Mike He; Zhaoyu Li; Zixuan Yi; Sharad Malik; Aarti Gupta; Xujie Si; Osbert Bastani
• Ҳаммуаллифи аввал ё саҳми баробар: Дар PDF маълумоти саҳми баробар ё ҳаммуаллифи аввал нишон дода нашудааст.
• Муаллифони номбаршуда барои мукотиба: Marcus J. Min, Mike He, Sharad Malik, Aarti Gupta, Xujie Si ва Osbert Bastani
• Муассисаҳо: University of Pennsylvania; Princeton University; University of Toronto
• Навъи манбаъ: Мақолаи мавқеъгирии конфронсии аз баррасии ҳамсолон гузашта
• Конфронс: 43rd International Conference on Machine Learning, ICML 2026
• Навъи пешниҳод/қабул: Position Paper Track, Spotlight
• Силсилаи нашр: Proceedings of Machine Learning Research, PMLR 306
• Ношири аслӣ: Proceedings of Machine Learning Research
• Ҷой ва соли конфронс: Сеул, Кореяи Ҷанубӣ, 2026
• Ҳолати баррасии ҳамсолон: Дар доираи ICML 2026 Position Paper Track арзёбӣ шуда, ҳамчун Spotlight қабул шудааст. Мақола инчунин ба баррасони беном ташаккур мегӯяд.
• DOI-и ниҳоии нашри конфронсӣ: Дар PDF-и боршуда DOI-и ҷудогонае барои нашри PMLR оварда нашудааст.
• Шиносаи arXiv: arXiv:2607.13292
• DOI-и DataCite-и arXiv: 10.48550/arXiv.2607.13292; дар саҳифаи arXiv ҳамчун сабти дар интизор нишон дода мешавад. Ин шиноса набояд ҳамчун DOI-и ҷудогонаи нашри конфронсии PMLR пешниҳод шавад.
• Сабтҳои расмӣ ё тасдиқшуда:Сабти таҳқиқот дар OpenReview, Сабти таҳқиқот дар arXiv, Сабти таҳқиқот дар SSRN

Ин мақолаи Verianla бо баррасии пурраи таҳқиқоти 16-саҳифагии боршуда аз аввал то охир таҳия шудааст. Дар баробари матни асосӣ, Ҷадвали 1, Шаклҳои 1–7, мисолҳои баробармаъноии математикӣ, адабиёт ва бахшҳои замимавӣ оид ба синтези барномаҳои декларативӣ ва автоматии формализатсияи исбот арзёбӣ шудаанд. Ягон натиҷаи илмӣ, иҷроиши усул ё натиҷаи таҷрибавие, ки берун аз PDF аст, илова нашудааст. Манбаъҳои беруна танҳо барои тасдиқи маълумоти библиографӣ мисли тартиби муаллифон, платформаи нашр, ҳолати Spotlight ва шиносаи arXiv истифода шудаанд.

Маҳдудияти асосии таҳқиқот ин аст, ки низоми нави татбиқшуда ва таҷрибавӣ арзёбишудаи сатҳи назария пешниҳод намекунад. Муваффақияти се самти пешниҳодшуда ҳанӯз бо таҷрибаҳои муқоисавӣ нишон дода нашудааст. Азбаски лоиҳаҳо ва маҷмӯаҳои додаҳои баррасишуда соҳа, доира ва меъёрҳои гуногун доранд, сатҳҳои гузоришшудаи муваффақият набояд барои рейтинги мустақими байниҳамдигарӣ истифода шаванд. Амалишавии намоиши миёнарави муштарак, ҳадди қабулшавандаи санҷиши баробармаъноӣ, то чӣ андоза коҳиш ёфтани меҳнати мутахассис ва чӣ гуна нигоҳ доштани садоқати маъно дар ҳуҷҷатҳои чандкипа ҳамчун саволҳои кушодаи таҳқиқотӣ боқӣ мемонанд.