INSAIT - Институтът за изкуствен интелект към Софийския университет "Св. Климент Охридски", съвместно с Швейцарския технологичен институт ETH Цюрих, представи най-мащабното изследване досега на математически доказателства, създадени от изкуствен интелект, предава БТА.
Проучването се основава на Open Proof Corpus (OPC) - най-големия етикиран корпус от математически доказателства, генерирани от AI и проверени от експерти. Проектът е естествено продължение на платформата MathArena.ai, чиито резултати вече намират приложение във водещи технологични компании при обучението на "мислещи" AI модели.
Целта на новото поколение AI не е просто да предоставя верни отговори, а да създава логически издържани и коректни математически доказателства, подчертават от Софийския университет.
OPC съдържа над 5 000 доказателства, създадени от водещи AI модели като Gemini 2.5 Pro, OpenAI O3 и O4-mini, Qwen и DeepSeek R1. Задачите са избрани от 20 елитни математически състезания, сред които Международната олимпиада по математика (IMO). Всяко решение е независимо оценено от експерти за коректност.
Резултатите от изследването сочат, че най-модерните AI модели започват да се доближават до човешкото ниво при оценка на математически доказателства по достоверност. Въпреки това, създаването на напълно формални и безупречни доказателства остава предизвикателство, отбелязват от INSAIT.
Изследването е дело на екип от INSAIT и ETH Цюрих, включващ Иво Петров, Кристиян Минчев, д-р Мислав Балунович и проф. Мартин Вечев. В изграждането на OPC участват и редица български лауреати от национални и международни математически олимпиади, както и техни ръководители, сред които Мирослав Маринов, Мария Дренчева, Люба Конова, Милен Шуманов, Калоян Цветков и други. Много от тях са стипендианти и участници в програмите на INSAIT.