Изследователи от българския институт INSAIT и швейцарския ETH Zurich представиха Open Proof Corpus (OPC) – най-големия в света корпус от математически доказателства, генерирани от изкуствен интелект и ръчно оценени от експерти.
„Радваме се да представим най-мащабното проучване на AI-генерирани математически доказателства в света досега – ключова стъпка към развитието на следващото поколение мислещи AI модели“, заявиха от INSAIT, като подчертаха, че зад проекта стоят „редица български лауреати от национални и международни математически олимпиади, както и ръководители на български национални отбори“.
В основата на изследването стои идеята, че следващата стъпка за т.нар. „разсъждаващи AI модели“ не е просто да дават верни отговори, а да могат да формулират логически издържани и математически коректни доказателства.
За целта екипът е подбрал 1 010 задачи от 20 престижни състезания, включително Международната олимпиада по математика (IMO), AIME и USAMO. Създаденият корпус включва над 5 000 доказателства, генерирани от водещите AI модели днес – сред които Gemini 2.5 Pro, о3/о4-mini, Grok 3, Qwen и DeepSeek R1 – като всяко решение е проверено от експерти за коректност.

Въпреки че едва 43% от генерираните доказателства са верни, изследването разкрива ключов напредък в друга посока – способността на най-съвременните модели да разпознават дали дадено доказателство е вярно. Според учените системите вече са „почти толкова добри, колкото експертите в оценката на доказателства“. Например, моделът Gemini 2.5 Pro на Google достига 85.4% точност при преценка на доказателства, което е близо до нивото на човешките аннотатори (90.4%). Почти същия резултат (83.8%) постига и много по-малък AI модел (OPC-R1-8B), обучен от екипа на INSAIT.
Изследването обръща внимание и на важната разлика между „верен краен отговор“ и „валидно доказателство“. Учените установяват, че някои AI модели често успяват да посочат правилния резултат, но без да могат да го подкрепят с логически последователна и математически издържана аргументация.
Друг интересен извод от изследването е, че естественият език превъзхожда формалния при генерирането на доказателства. Учените установяват, че AI моделите постигат до 11 пъти по-висока ефективност, когато формулират доказателства на естествен език, вместо на формален математически.
OPC е естествено продължение на предходна инициатива на INSAIT – платформата MathArena.ai, която вече се използва за оценка на AI модели от водещи компании като OpenAI и Google. „Вярваме, че проекти като този спомагат за позиционирането на България в света на изкуствения интелект и технологиите на най-високо световно ниво“, посочват от института.
Последвайте ни в социалните мрежи – Facebook, Instagram, X и LinkedIn!
Споделете: