INSAIT

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

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.