Il-provi ta’ DeepMind u t-test tan-novità

Prova matematika tista’ tinqara b’mod sabiħ u xorta jkun fiha lakuna li ħadd ma jinduna biha għal snin sħaħ. L-aġent tal-intelliġenza artifiċjali AlphaProof Nexus ta’ Google DeepMind ipproduċa provi għal disa’ problemi mressqa minn Paul Erdős, u softwer ivverifika kull pass. Ix-xogħol deher għall-ewwel darba fi preprint f’Mejju (arXiv) u ġie ppubblikat wara reviżjoni minn esperti fil-qasam f’Science fit-8 ta’ Ottubru (Science). Is-softwer seta’ jikkonferma l-loġika, iżda kien f’idejn il-matematiċi jiddeċiedu jekk dik il-loġika kinitx tgħid xi ħaġa ġdida.

Eżaminatur li ma jitqarraqx bi kliem sabiħ

Is-sistemi taċ-chat huma tajbin biex jiktbu matematika li tidher korretta. Paragrafu kunfidenti jista’ jgħatti pass nieqes, u qarrej attent biss jinduna bih. AlphaProof Nexus jevita din in-nassa billi jaħdem f’Lean, lingwaġġ ta’ programmazzjoni li jintuża biex jinkitbu definizzjonijiet, stqarrijiet u provi bi preċiżjoni li tippermetti lill-kompjuter jivverifikahom.

Aħseb f’Lean bħala eżaminatur li jaqra kull linja ta’ prova lesta u japplika regoli fissi. L-istil ma jiswa ebda punt. Jekk pass wieħed ma jirriżultax minn dawk ta’ qablu, il-prova tfalli, tkun kemm tkun eleganti l-bqija tagħha.

It-tim jiddeskrivi lill-aġent bħala sistema li tfittex provi miktubin b’Lean. Ir-riċerkaturi tawh aċċess ukoll għal AlphaProof, sistema preċedenti ta’ DeepMind mibnija apposta għall-provi. Fit-testijiet tat-tim, konfigurazzjoni aktar sempliċi tat l-istess riżultati: mudell lingwistiku flimkien ma’ Lean, mingħajr AlphaProof, xorta rnexxielu jikseb id-disa’ provi ta’ Erdős (The Decoder). Għal dawk il-problemi, il-komponent speċjalizzat irriżulta bla bżonn.

L-artiklu jirrapporta provi aċċettati għad-disa’ stqarrijiet ta’ Erdős u għal 44 konġettura (stqarrijiet meqjusa veri iżda li qatt ma ġew ippruvati) mill-Online Encyclopedia of Integer Sequences, katalgu vast ta’ xejriet fin-numri (Science). Fost ir-riżultati dwar Erdős hemm mistoqsija f’żewġ partijiet dwar in-numri sħaħ li Erdős u András Sárközy ressqu fl-1970. Din baqgħet bla soluzzjoni għal aktar minn nofs seklu (ABC).

Dak li l-eżaminatur ma jistax jara

Il-garanzija ta’ Lean għandha limitu preċiż: tikkonferma li prova tistabbilixxi l-istqarrija eżatt kif inkitbet fil-kodiċi. Hemm tliet mistoqsijiet li jmorru lil hinn minnha: jekk il-kodiċi jaqbilx ma’ dak li ried ifisser Erdős, jekk xi ħadd kienx wieġeb il-mistoqsija ħafna qabel, u jekk it-tweġiba tgħallimniex xi ħaġa.

Il-problema tal-1970 turi għaliex huma importanti l-aħħar żewġ mistoqsijiet. It-tieni parti tagħha timplika l-ewwel waħda, għalhekk prova waħda ssolvihom it-tnejn. Wara li bdew jiċċirkolaw il-provi tal-aġent, ħareġ li aġġustament żgħir għal kostruzzjoni fl-artiklu oriġinali tal-1970 iwieġeb iż-żewġ partijiet ukoll (arXiv). Il-provi tal-aġent kienu korretti. Il-problema kienet sempliċement eqreb lejn is-soluzzjoni milli kien jissuġġerixxi l-istatus tagħha bħala problema “miftuħa”.

Biex jinqabdu każijiet bħal dan, hemm bżonn nies li jafu sew il-qasam. Gergely Bérczi, matematiku fl-Università ta’ Aarhus fid-Danimarka u wieħed mill-awturi, għen fl-għażla ta’ mistoqsijiet xierqa u fil-validazzjoni tas-soluzzjonijiet (Aarhus University). Għen ukoll fil-kitba ta’ verżjonijiet tal-provi li l-qarrejja umani jistgħu jsegwu. Lean ta garanzija għal kull linja, filwaqt li Bérczi u l-kollegi tiegħu ġġudikaw x’kienu jżidu dawk il-linji meta jitqiesu flimkien.

Din id-diviżjoni tax-xogħol tagħmel dan l-istudju differenti minn kisba importanti tax-xahar li għadda. Dakinhar, Claude ta’ Anthropic ikkonverta l-prova diġà magħrufa tal-Aħħar Teorema ta’ Fermat f’Lean (To Brief). It-traduzzjoni ta’ prova magħrufa ma tqajjem ebda dubju dwar in-novità tagħha. Tfittxija fost stqarrijiet meqjusa bħala mhux solvuti tqajjem dubji bħal dawn, u f’dak il-każ il-verifika tan-novità ssir l-aktar parti importanti.

It-tim ippubblika l-fajls tal-provi, biex ħaddieħor ikun jista’ jgħaddihom mill-istess eżaminatur (GitHub). L-avvanz muri f’dan l-istudju huwa speċifiku. Aġent tal-intelliġenza artifiċjali pproduċa provi li magna tista’ tivverifika għal xi stqarrijiet li l-matematiċi kienu jqisu bħala mhux solvuti, u l-garanzija tkopri dawk l-istqarrijiet kif inkitbu f’Lean. Biex jiddeterminaw x’żiedet kull prova mal-matematika, kien għad hemm bżonn il-matematiċi li qrawhom.