Cruthúnais DeepMind á dtástáil ar úire

Is féidir le cruthúnas matamaiticiúil a bheith galánta ar fad agus bearna a bheith ann fós nach dtugann aon duine faoi deara go ceann blianta. Tháirg gníomhaire IS AlphaProof Nexus de chuid Google DeepMind cruthúnais ar naoi bhfadhb a leag Paul Erdős amach, agus rinne bogearraí gach céim a sheiceáil. Tháinig an saothar chun solais ar dtús i réamhfhoilseachán i mí na Bealtaine (arXiv), agus foilsíodh é in Science tar éis piarmheasúnú ar 8 Deireadh Fómhair (Science). Bhí bogearraí in ann an loighic a dheimhniú, ach faoi na matamaiticeoirí a bhí sé a mheas ar chuir an loighic sin rud nua ar bith ar fáil.

Réiteoir nach féidir a mhealladh

Tá comhrá-róbónna go maith ag scríobh matamaitice a bhfuil cuma cheart uirthi. Is féidir le halt muiníneach céim ar iarraidh a cheilt, agus ní thabharfaidh ach léitheoir cúramach faoi deara í. Seachnaíonn AlphaProof Nexus an gaiste sin trí oibriú in Lean, teanga ríomhchlárúcháin chun sainmhínithe, éilimh agus cruthúnais a chur in iúl chomh beacht sin gur féidir le ríomhaire iad a sheiceáil.

Smaoinigh ar Lean mar réiteoir a léann gach líne de chruthúnas críochnaithe agus a chuireann rialacha seasta i bhfeidhm. Ní thugtar aon phointe as stíl. Mura leanann céim amháin ó na céimeanna roimhe sin, teipeann ar an gcruthúnas, is cuma cé chomh galánta is atá an chuid eile.

Deir an fhoireann gur cuardaigh an gníomhaire cruthúnais a bhí scríofa in Lean. Thug na taighdeoirí rochtain dó ar AlphaProof freisin, córas de chuid DeepMind a tógadh go speisialta chun cruthúnais a aimsiú. Ina gcuid tástálacha, fuair leagan níos simplí na torthaí céanna: d’éirigh le samhail teanga in éineacht le Lean, gan AlphaProof, cruthúnais Erdős ar fad a fháil (The Decoder). Ní raibh gá leis an gcomhpháirt shaineolach i gcás na bhfadhbanna sin.

Tuairiscítear sa pháipéar gur glacadh le cruthúnais ar na naoi ráiteas Erdős agus ar bharúlacha ón Online Encyclopedia of Integer Sequences — 44 san iomlán. Is éard is barúil ann éileamh a mheastar a bheith fíor ach nár cruthaíodh riamh. Catalóg fhairsing de phatrúin uimhreach atá san chiclipéid sin (Science). Ar thorthaí Erdős tá freagra ar cheist dhá chuid faoi shlánuimhreacha a chuir Erdős agus András Sárközy in 1970. Níor réitíodh í le breis agus leathchéad bliain (ABC).

Rudaí nach bhfeiceann an réiteoir

Tá teorainn shoiléir le ráthaíocht Lean. Deimhníonn sé go gcruthaíonn cruthúnas an ráiteas díreach mar atá sé scríofa sa chód. Tá trí cheist nach dtugann sé freagra orthu: an léiríonn an cód an rud a bhí i gceist ag Erdős; ar fhreagair duine éigin an cheist fadó; agus an gcuireann an freagra rud ar bith le heolas na matamaitice.

Léiríonn fadhb 1970 cén fáth a bhfuil tábhacht leis an dá cheist dheireanacha. Tugann an dara cuid den fhadhb an chéad chuid le fios, mar sin réitíonn cruthúnas amháin an dá chuid. Nuair a scaipeadh cruthúnais an ghníomhaire, tháinig sé chun solais go bhfreagraíonn athrú beag ar cheann de na tógálacha sa bhunpháipéar ó 1970 an dá chuid freisin (arXiv). Bhí cruthúnais an ghníomhaire ceart. Ní raibh an fhadhb ach níos gaire do réiteach ná mar a thabharfadh an lipéad “gan réiteach” le fios.

Teastaíonn daoine a bhfuil eolas acu ar an réimse chun a leithéid a thabhairt faoi deara. Chabhraigh Gergely Bérczi, matamaiticeoir in Ollscoil Aarhus sa Danmhairg agus duine d’údair an pháipéir, le ceisteanna oiriúnacha a roghnú agus na réitigh a bhailíochtú (Aarhus University). Chabhraigh sé freisin le leaganacha de na cruthúnais a scríobh a bhféadfadh léitheoirí daonna iad a leanúint. Dhearbhaigh Lean gach líne, agus mheas Bérczi agus a chomhghleacaithe an méid a chuir na línte sin leis ina n-iomláine.

Is é an deighilt sin sa saothar a chuireann an staidéar seo ar leith ó chloch mhíle a baineadh amach an mhí seo caite. An uair sin, chuir Claude de chuid Anthropic cruthúnas a bhí ar eolas cheana féin ar Theoirim Dheireanach Fermat i bhfoirm Lean (To Brief). Ní ardaíonn aistriú cruthúnais cháiliúil ceist ar bith faoin úrnuacht. Nuair a chuardaítear ráitis a mheastar a bheith gan réiteach, tagann ceist na húrnuachta chun cinn agus bíonn a seiceáil lárnach.

Tá comhaid na gcruthúnas foilsithe ag an bhfoireann, ionas gur féidir le daoine eile iad a chur tríd an réiteoir céanna (GitHub). Is dul chun cinn sonrach atá léirithe sa staidéar seo. Tháirg gníomhaire IS cruthúnais is féidir le meaisín a sheiceáil ar roinnt ráiteas a bhí á meas ag matamaiticeoirí mar ráitis gan réiteach, agus baineann an ráthaíocht leis na ráitis sin mar atá siad scríofa in Lean. Is ar na matamaiticeoirí a léigh na cruthúnais a bhí sé fós a mheas cad a chuir gach ceann acu leis an matamaitic.