Veliki jezični modeli oduševljavaju, ali i dalje griješe – ponekad s fatalnim posljedicama kada je riječ o financijama, medicini ili autonomnim sustavima. Otvoreni programski jezik i dokazivač teorema Lean4 nameće se kao rješenje koje takvu nepredvidivost pretvara u matematičku izvjesnost.
Što Lean4 donosi
• Svaki program ili teorem mora proći strogu provjeru jezgrom Lean4; rezultat je binaran – dokaz vrijedi ili ne vrijedi. • Determinističko ponašanje: isti ulaz uvijek daje isti, formalno provjeren izlaz. • Potpuna transparentnost, jer se svaki korak zaključivanja može naknadno auditirati.
Za razliku od neuralnih mreža koje se oslanjaju na vjerojatnosti, Lean4 jamči dokazivu točnost. Zato ga sve više istraživačkih skupina kombinira s LLM-ovima kako bi se dobili sustavi koji „razmišljaju ispravno po konstrukciji”.
Provjera protiv halucinacija
Okvir Safe iz 2025. prijevodom svakog koraka rezoniranja LLM-a u Lean4 otkriva grešku u trenutku kada dokaz zakaže – halucinacija se time zaustavlja na izvoru.
Startup Harmonic AI otišao je korak dalje: njihov chatbot Aristotle rješava matematičke zadatke tek nakon što u Lean4 napiše i provjeri vlastiti dokaz. Tvrtka tvrdi da time nudi „chatbot bez halucinacija” i navodi da je na zadacima Međunarodne matematičke olimpijade 2025. dosegnula razinu zlatne medalje – s razlikom da su rješenja formalno ovjerena.
Nova era sigurnog programiranja
Ista logika prelijeva se na razvoj softvera. Benchmark VeriBench pokazao je da trenutačni LLM-ovi samostalno formalno verificiraju tek oko 12 % zadataka, no iterativni „agentski” pristup diže uspjeh na gotovo 60 %. Vizija: zatražite od AI-ja program i dobijete ne samo kod, nego i dokaz da nema rupe za sigurnosne propuste niti mogućnost rušenja.
Tko sve ulaže
• OpenAI i Meta još 2022. trenirali su modele koji generiraju Lean dokaze za školske matematičke zadatke. • DeepMind je 2024. razvio AlphaProof, koji u Lean4 postiže razinu srebrnog olimpijca. • Harmonic AI prikupio je 100 milijuna dolara kako bi Lean4 pretvorio u komercijalni „kišobran” protiv halucinacija.
Izazovi ostaju – formalizacija realnih problema traži vrijeme, a sadašnji modeli još često griješe. No trend je jasan: formalna provjera prelazi iz akademskih krugova u industrijsku svakodnevicu.
Poruka za tvrtke
U doba kada povjerenje postaje najskuplja valuta, dokaz umjesto obećanja postaje konkurentska prednost. Lean4 ne rješava sve rizike umjetne inteligencije, ali omogućuje AI-ju da ne samo tvrdi da je u pravu – nego to i matematički dokaže.