DeepSeek представи DeepSeek-Prover-V2, новаторски голям езиков модел (LLM) с отворен код, щателно създаден за сложната област на формалното доказване на теореми в рамките на Lean 4 framework. Този нов модел използва рекурсивен тръбопровод за доказване на теореми, използвайки силата на най-съвременния модел DeepSeek-V3 на DeepSeek. Lean 4, най-новата итерация на теоремата Lean prover, е интерактивен асистент за доказване, разработен от Microsoft Research. Този сложен функционален език за програмиране и интерактивна система за доказване на теореми дава възможност на математици и компютърни специалисти да конструират формални доказателства с несравнима машинно проверена верификация.
Проектът означава монументална стъпка към преодоляване на пропастта между формалното и неформалното математическо разсъждение. Като се възползват от присъщите възможности на универсалните LLM, те се стремят ефективно да се справят с високо структурираната област на формалното доказване на теореми. Изследователският екип на DeepSeek постулира, че техният иновативен подход отразява когнитивните процеси, използвани от човешките математици при конструиране на доказателства, като щателно дисектират сложни теореми в по-управляеми и разбираеми компоненти.
Разширяване на рамката за оценка: Представяне на ProverBench
В значителен ход за засилване на строгостта на техните изследвания, екипът на DeepSeek значително разшири тяхната рамка за оценка с въвеждането на ProverBench, изцяло нова колекция от бенчмаркове, щателно проектирана специално за цялостната оценка на възможностите за формално доказване на теореми. Тази изчерпателна колекция служи като ценен ресурс за оценка на производителността на LLM в контекста на формалната математика.
"Отвъд конвенционалните анализи, ние с гордост представяме ProverBench, щателно подбрана колекция от 325 формализирани проблема, за да обогатим нашия процес на оценка. Тази колекция включва 15 внимателно подбрани проблема, взети директно от скорошните състезания American Invitational Mathematics Examination (AIME), по-специално от годините 24-25,", обясниха изследователите.
Включването на AIME проблеми в набора от данни на ProverBench е особено забележително, тъй като представя набор от предизвикателни и добре установени математически проблеми, които са широко признати в рамките на математическата общност. Това осигурява стандартизирана и строга основа за оценка на производителността на DeepSeek-Prover-V2 и за сравняването му с други подходи.
Обещаващи първоначални резултати: Справяне с AIME проблеми
Първоначалните резултати, произтичащи от строги тестове върху тези предизвикателни AIME проблеми, разкриха изключително обещаващо представяне от техния щателно проектиран специализиран модел за доказване на теореми. Екипът на DeepSeek с гордост съобщава, че DeepSeek-Prover-V2 демонстрира своята мощ, като успешно реши впечатляващите 6 от 15-те AIME проблема, представени му. В сравнение с това, универсалният модел DeepSeek-V3, когато използваше техниките за гласуване с мнозинство, успя успешно да реши 8 проблема.
Тези открития подчертават потенциала както на специализираните, така и на универсалните LLM за справяне със сложни математически проблеми. Докато универсалният модел показа малко по-висок процент на успех в този конкретен бенчмарк, специализираният модел за доказване на теореми демонстрира своята компетентност във формалното математическо разсъждение.
Подражаване на човешката конструкция на доказателства: Подход „Верига на мисълта“
"Като се имат предвид добре документираните предизвикателства, които универсалните модели често срещат, когато се опитват да генерират пълни Lean доказателства, ние стратегически инструктирахме DeepSeek-V3 да генерира само скица на доказателство на високо ниво, като нарочно пропуснахме сложните подробности. Получената верига от мисли завършва с Lean теорема, съставена от поредица от have statements, всяко от които старателно завършва със sorry placeholder, ефективно показващо подцел, която трябва да бъде решена. Този иновативен подход елегантно отразява човешкия стил на конструиране на доказателства, при който сложна теорема постепенно се свежда до поредица от по-управляеми леми,", обясни екипът на DeepSeek.
Този иновативен подход за генериране на скици на доказателства на високо ниво се привежда в съответствие с това как математиците често подхождат към сложни доказателства. Като се фокусира върху цялостната структура и ключови стъпки, моделът може ефективно да насочи последващото усъвършенстване и завършване на доказателството.
Методична стратегия: Индивидуално адресиране на всеки компонент от доказателството
След това системата щателно прилага методична и структурирана стратегия за адресиране на всеки отделен компонент от доказателството. Този систематичен подход гарантира, че всеки аспект от доказателството е внимателно разгледан и адресиран по логичен и последователен начин. Системата създава високо структуриран подход към доказването на теореми, надграждайки върху вече установени резултати, за да осигури солидна основа за всяка следваща стъпка.
"Използвайки подцелите, генерирани от DeepSeek-V3, ние възприемаме рекурсивна стратегия за решаване, за да разрешим систематично всяка междинна стъпка на доказателството. Извличаме изрази на подцели от have statements, за да ги заместим с оригиналните цели в дадените проблеми и след това включваме предходните подцели като предпоставки. Това конструиране позволява последващите подцели да бъдат решени, като се използват междинните резултати от по-ранните стъпки, като по този начин се насърчава по-локализирана структура на зависимости и се улеснява разработването на по-прости леми,", уточниха изследователите.
Рекурсивната стратегия за решаване е ключов аспект от способността на системата да се справя със сложни доказателства. Като разбива проблема на по-малки, по-управляеми подцели, системата може ефективно да приложи своите възможности за разсъждение към всеки отделен компонент.
Оптимизиране на изчислителните ресурси: Специализиран модел със 7B параметри
За ефективно оптимизиране на изчислителните ресурси и осигуряване на ефективна обработка, системата стратегически използва по-малък, високо специализиран модел със 7B параметри за обработка на декомпозираните леми. Този подход е от решаващо значение за ефективно управление на изчислителните изисквания, свързани с широките търсения на доказателства, като гарантира, че системата може да работи ефективно, без да бъде затрупана от сложността на пространството за търсене. Подходът в крайна сметка завършва с автоматично изведено пълно доказателство, когато всички разложени стъпки са успешно решени.
"Алгоритмичната рамка работи на два отделни етапа, използвайки два допълващи се модела: DeepSeek-V3 за разлагане на леми и модел prover със 7B за попълване на съответните детайли на формалното доказателство,", описаха изследователите.
Този двустепенен подход позволява на системата да използва силните страни както на голям универсален модел, така и на по-малък специализиран модел. Големият модел се използва за генериране на скици на доказателства на високо ниво, докато по-малкият модел се използва за попълване на детайлите и завършване на формалното доказателство.
Синтезиране на данни за формално разсъждение: Естествен път
Тази щателно проектирана архитектура ефективно установява естествен и интуитивен път за синтезиране на данни за формално разсъждение, безпроблемно сливане на математическо разсъждение на високо ниво със стриктните и строги изисквания на формалната проверка. Тази интеграция е от съществено значение за гарантиране на надеждността и достоверността на резултатите на системата.
"Ние курираме подмножество от предизвикателни проблеми, които остават нерешени от модела prover със 7B по цялостен начин, но за които всички разложени подцели са успешно разрешени. Като съставим доказателствата за всички подцели, ние конструираме пълно формално доказателство за оригиналния проблем,", обясниха изследователите.
Този подход позволява на системата да се учи от своите грешки и да подобрява способността си да решава сложни проблеми. Като идентифицира конкретните подцели, които причиняват трудности, системата може да фокусира усилията си върху подобряване на своята производителност в тези области.
Притеснения и предизвикателства: Подробности за изпълнението под проверка
Въпреки неоспоримите технически постижения, демонстрирани от DeepSeek-Prover-V2, някои експерти в областта повдигнаха уместни опасения относно някои подробности за изпълнението. Елиът Глейзър, високо уважаван водещ математик в Epoch AI, посочи потенциални проблеми, които изискват по-нататъшно разследване.
Някои опасения относно статията DeepSeek-Prover-V2. Потенциално неправилно формализирани примери и дискусията относно Lean zulip предполага, че PutnamBench доказателствата са безсмислици и използват имплицитно sorry (вероятно скрито в apply? tactic), което не е докладвано в техния read-eval-print-loop.
Тези опасения ярко подчертават текущите предизвикателства, присъщи на пространството за формална проверка, където дори най-малките и на пръв поглед незначителни подробности за изпълнението могат да окажат непропорционално голямо въздействие върху цялостната валидност и надеждност на резултатите. Процесът на формална проверка изисква непоколебимо внимание към детайлите и щателно придържане към установените стандарти.
Потенциалът за неправилно формализирани примери и възможността за скрити "sorry" тактики в PutnamBench доказателствата повдигат важни въпроси относно строгостта и пълнотата на процеса на проверка. Тези опасения подчертават необходимостта от продължаваща проверка и независима проверка на резултатите.
Наличност и ресурси: Демократизиране на достъпа до формално доказване на теореми
DeepSeek направи своя Prover-V2 достъпен в два различни размера на моделите, за да отговори на разнообразен набор от изчислителни ресурси и изследователски цели. Първата версия е модел със 7B параметри, изграден върху предишния им Prover-V1.5-Base, включващ разширена дължина на контекста до 32K токена. Втората версия е значително по-голям модел с 671B параметри, обучен на DeepSeek-V3-Base. И двата модела вече са лесно достъпни в HuggingFace, водеща платформа за споделяне и сътрудничество върху модели за машинно обучение.
В допълнение към самите модели, DeepSeek също направи пълния набор от данни ProverBench, съдържащ 325 щателно формализирани проблема за целите на оценката, достъпен в HuggingFace. Този изчерпателен набор от данни предоставя на изследователи и разработчици ценен ресурс за оценка на производителността на техните модели и за сравняването им с DeepSeek-Prover-V2.
Като направи тези ресурси свободно достъпни, DeepSeek демократизира достъпа до технология за формално доказване на теореми и насърчава сътрудничеството в рамките на изследователската общност. Този подход с отворен код вероятно ще ускори напредъка в областта и ще доведе до нови пробиви в автоматизираното разсъждение и проверка.
Това издание дава възможност на изследователите и разработчиците с ресурсите, необходими за да се впуснат във възможностите и ограниченията на тази технология. Чрез предоставяне на отворен достъп до моделите и набора от данни на ProverBench, DeepSeek насърчава по-нататъшно проучване и съвместни усилия за справяне с опасенията, повдигнати от експерти в областта. Този съвместен подход държи ключа към разплитането на сложността на формалното доказване на теореми и затвърждаването на надеждността на тези новаторски постижения.