Dirbtinio intelekto (DI) proveržis matematikos srityje sukuria įrodymus, kurie savo apimtimi ir sudėtingumu kelia pasitikėjimo iššūkių. Nors technologijų bendrovės, tokios kaip „OpenAI“, pristato mašininio patikrinimo rezultatus, mokslininkai analizuoja ribas tarp natūralios kalbos teiginių ir kompiuterinio kodo, atkreipdami dėmesį į galimus netikslumus ir spragas.

Mašininė patikra tampa naujuoju standartu

Matematika istoriškai rėmėsi pasitikėjimu ir kolegų atliekama peržiūra, tačiau XX a. viduryje atsiradę įrodymų asistentai (angl. proof assistants) leido matematines teorijas paversti kompiuteriui suprantama kalba. Šis procesas, vadinamas formalizavimu, reikalauja absoliutaus tikslumo, kur kiekvienam veiksmui būtinas pagrindimas. „Kiekvieną kartą, kai rašote įrodymą natūralia kalba, pavyzdžiui, anglų ar prancūzų, jūsų samprotavimuose gali būti spragų. Jei formalizuojate įrodymą, esate priversti būti daug aiškesni dėl visų savo veiksmų“, – teigia Wesley Fussneris, Čekijos mokslų akademijos Kompiuterių mokslo instituto tyrėjas.

Šioje srityje išsiskiria 2013 m. sukurta „Lean“ sistema. Dėl savo efektyvaus dizaino ji tapo de facto pasirinkimu daugeliui matematikų, norinčių verifikuoti įrodymus. Iki šiol formalizuota matematika dažniausiai buvo „vadovėlinė“, dėl kurios visi sutaria, kaip pažymi Silvainas Rideau-Kikuchi, Paryžiaus École Normale Supérieure logikas. Tačiau DI įsitraukimas dramatiškai pagreitino procesą.

„OpenAI“ pasiekimai po didinamuoju stiklu

Kai DI susiduria su dviprasmiška formuluote, išlieka rizika, kad mašininis formalizavimas neatitiks natūralia kalba suformuluoto teiginio. Rugsėjo mėnesį, po to, kai bendrovė „OpenAI“ paskelbė įveikusi „Navier-Stokes“ problemą, tyrėjai pradėjo nagrinėti šį rezultatą. Vertimo iš natūralios kalbos į kompiuterinį kodą netikslumai gali sukurti situaciją, kai patikrinamas kitoks teiginys, nei buvo skelbiama iš pradžių.

„Sistema yra daug mažiau tobula, nei būtų galima tikėtis, jei jai teikiame tiek daug svorio“, – sako Silvainas Rideau-Kikuchi. Jis priduria, kad kyla pagunda pasakyti: „Žiūrėkite, galbūt straipsnis neturi prasmės, bet mes turime formalizavimą, todėl tai turi būti teisinga“. Tačiau toks požiūris ignoruoja galimus „vertimo“ netikslumus. Andersas Hansenas iš Kembridžo universiteto pabrėžia, kad prastam DI autoformalizatoriui tektų „kasytis galvą ir sakyti: „Ką, po velnių, tai reiškia?“

Sistemos spragos ir „atlygio hakavimas“

Ekspertai ir tyrėjai pripažįsta, kad programinės įrangos klaidų buvimas kelia riziką, ypač kai DI agentai yra linkę į „atlygio hakavimą“ (angl. reward hacking) – taisyklių arba sėkmės kriterijų apėjimą, siekiant formaliai patvirtinti rezultatą. Milo Mosesas, matematikos doktorantas Kalifornijos technologijos institute, teigia, kad tai „sulaužo visą DI saugumo atvejį“.

Didžioji dalis šiuolaikinės matematikos remiasi aibių teorija, kurią patikrino „mokslo fanatikų armijos“. Tačiau DI įsitraukimas reikalauja papildomo atidumo vertinant automatinio formalizavimo procesus. Jei „Lean“ ateitis bus tokia, kad kiekviena sąveika bus tarpininkaujama per autoformalizavimą, Anne Baanen, „Mathlib“ prižiūrėtoja, tai laiko „labai nuobodžia ateitimi“. Leonardo de Moura, „Amazon Web Services“ kompiuterių mokslininkas ir „Lean“ kūrėjas, perspėja, kad „tai ir toliau vyks“. Pasitikėjimas DI generuojama matematika priklausys nuo to, kaip bus užtikrinamas tikslus teiginių perkėlimas į verifikavimo sistemas ir kaip bus šalinamos programinės įrangos nepilnatvės.

Pateikiama informacija yra aiškinamasis aprašas; ji neskirta teisinių, politinių ar investicinių sprendimų priėmimui.

Šaltiniai

  1. [1] [Science.org | 2026-10-30] AI is shaking up math. But can its proofs be trusted?
  2. [2] [Lrt.lt | 2026-10-30] Vilkauskas – apie nakties įvykius: reikia kompleksinės technologinės sistemos
  3. [3] [Esa.int | 2026-10-30] What happened this month at the European Space Agency? (October 2026)
  4. [4] [Aa.com.tr | 2026-10-30] Iran says navy destroyed 'enemy' unmanned vessel, 2 tankers damaged in Strait of Hormuz