INSAIT публикува отворен корпус от доказателства — най-голямата публична колекция от експертно анотирани математически доказателства, генерирани от изкуствен интелект

INSAIT и ETH Zurich обявяват пускането на Open Proof Corpus (OPC) — най-големият публичен набор от математически доказателства, генерирани от големи езикови модели (LLM) и щателно анотирани за коректност от човешки експерти. Наред с набора от данни, INSAIT публикува мащабно проучване, анализиращо производителността на днешните модели с изкуствен интелект при генериране на математически доказателства. Както наборът от данни, така и проучването са достъпни на proofcorpus.ai.

Отвореният корпус на доказателствата (OPC) се основава на по-ранната платформа на INSAIT, MathArena.ai, чиито резултати са възприети от големи технологични компании за сравняване и разработване на собствени „мислещи“ модели на изкуствен интелект. OPC представлява значителна стъпка напред в развитието на системите с изкуствен интелект отвъд генерирането на правилни отговори към генериране на валидни и строги математически доказателства.

Корпусът включва над 5000 доказателства, създадени от водещи модели на изкуствен интелект, като Gemini 2.5 pro, OpenAI O3, OpenAI O4-mini, Qwen и DeepSeek R1. Задачите са взети от 20 елитни математически състезания, включително Международната математическа олимпиада (IMO) и Математическата олимпиада на САЩ (USAMO). Всички доказателства са внимателно прегледани и анотирани от опитни експертни съдии.

Проучването разкрива няколко ключови открития: големите езикови модели се доближават до нивото на човешките експерти при преценката на правилността на математическите доказателства, но генерирането на формални доказателства (например в Lean) остава основно предизвикателство за настоящите системи с изкуствен интелект.

Наборът от данни OPC, придружаващата го изследователска работа, в която са описани тези резултати, и фино настроените модели на изкуствен интелект на INSAIT са достъпни на proofcorpus.ai.

Автори: Яспър Деконинк, Иво Петров, Кристиян Минчев, Мислав Балунович, Мартин Вечев. Сътрудници на набора от данни (български състезатели по математика и треньори на национални отбори): Мирослав Маринов, Мария Дренчева, Люба Конова, Милен Шуманов, Калоян Цветков, Николай Дренчев, Лазар Тодоров, Калина Николова, Николай Георгиев, Ванеса Калинкова, Маргулан Исмолдаев