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