INSAIT и ETH Цюрих представят най-мащабното проучване на математически доказателства, генерирани от изкуствен интелект

Институтът INSAIT към Софийския университет „Св. Климент Охридски“ и ETH Цюрих представиха най-мащабното проучване до момента на математически доказателства, генерирани от изкуствен интелект, съобщиха от пресцентъра на университета.
Проучването обхваща 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 вида елитни състезания, включително Международната олимпиада по математика (IMO). Всяко доказателство е етикирано от човешки експерти за коректност.
Изследването показва, че мислещите AI модели вече се доближават до експертите в оценката на доказателства по отношение на вярност, но създаването на формални доказателства остава предизвикателство за системите с изкуствен интелект, обясниха от СУ.
Автори на изследването са изследователи от INSAIT и ETH Цюрих: Иво Петров, Кристиян Минчев, д-р Мислав Балунович и проф. Мартин Вечев. Допринесли за създаването на OPC са редица български лауреати от национални и международни математически олимпиади, както и ръководители на български национални отбори: Мирослав Маринов, Мария Дренчева, Люба Конова, Милен Шуманов, Калоян Цветков, Николай Дренчев, Лазар Тодоров, Калина Николова, Николай Георгиев, Ванеса Калинкова, Маргулан Исмолдаев. Много тях са и стипендианти и участници в различни програми на INSAIT, казаха от университета.
 
/ИПК