Машинна проверка на доказателство от 13 милиона реда

5.09

време за четене: 4 мин.

На 4 септември Anthropic обяви, че вътрешен изследователски модел е произвел пълно формално доказателство на Голямата теорема на Ферма. Работата е отнела 11 дни и около 6 милиарда изходни токена. Забележителното не е обемът, а че всеки ред от резултата е проверен от програма и не се приема на доверие.

Робот подава на математик свитък, който се разгъва до пода и продължава извън кадъра, а човекът проверява ред по ред с лупа и още не е кимнал, докато роботът чака встрани

Какво точно е произведено

Голямата теорема на Ферма е формулирана през 1637 г. и доказана от Андрю Уайлс през 1994 г. Доказателството на Уайлс е човешки текст: стотици страници, четени и рецензирани от хора. Формализацията е друго нещо - превод на това доказателство на език, на който компютър може да провери всяка стъпка. Езикът тук е Lean.

Числата идват от самото съобщение. Моделът е написал 13 милиона реда на Lean за 11 дни и е доказал по пътя 30 300 междинни теореми, от които 29 500 влизат в крайния резултат. Полученото доказателство е над пет пъти по-голямо от Mathlib, основната библиотека на общността, върху която стъпва.

Едно уточнение съобщението прави само: това не е публично достъпният Claude, а вътрешен изследователски модел, сравним по възможности с Claude Fable 5.1.

Защо машинна проверка сменя правилата

Обичайното възражение срещу текст от езиков модел е, че звучи убедително и въпреки това може да е грешен, а тежестта на проверката пада върху читателя. При формално доказателство това възражение отпада по устройство: ядрото на Lean отхвърля всяка стъпка, която не следва логически от предходните.

Машинна проверка означава, че резултатът не се приема на доверие, а се преизчислява от отделна програма. Тук проверките са три: пълно построяване на всичките 60 475 модула, сверяване на крайната формулировка с тази в Mathlib и повторно потвърждение от независимо ядро, написано на друг език. Крайният резултат стъпва само на трите стандартни аксиоми на Lean и построяването се проваля, ако това престане да е вярно.

Какво моделът не е направил

Ограниченията са в самото съобщение и си струва да се четат наред с числата.

Това не е нова математика. Доказателството следва опростен вариант на разсъжденията на Уайлс по изложението на Дармон, Даймънд и Тейлър. Стъпва и върху вече свършена чужда работа: части от проекта на Imperial College London, воден от Кевин Бъзард от 2024 г., и от flt-regular. Имало е и човешка намеса, макар оскъдна, на равнище указания кое да се свърши по-напред.

Първите опити се провалят. Агентите губят следата на състоянието и спират да си сътрудничат; неуспешните им опити дават около 7% от редовете в крайния резултат. Обемът също не е достойнство - самата статия отбелязва, че доказателството вероятно е доста по-дълго, отколкото е необходимо.

Цената е следващото ограничение. Шест милиарда изходни токена не са дребна сметка и Anthropic описва задачата като изискваща много токени. Тоест подходът засега е по силите на организация, която може да отдели такъв ресурс за една-единствена задача, а не е нещо, което се пуска между другото.

Остава и едно ограничение, което никаква програма не покрива: проверката потвърждава, че всяка стъпка следва от предходната, но не и че всяка междинна теорема значи онова, което името ѝ подсказва. Това остава работа за човека. Кевин Бъзард, който води отделния общностен проект и тук е рецензент, потвърди, че резултатът доказва теоремата без допускания извън аксиомите на математиката.

Какво следва от това за всекидневната работа

Изводът се пренася извън математиката и е по-полезен от самата новина.

Слабостта на езиковите модели е известна: убедителен изход без вградена гаранция за вярност. Тази слабост обаче не тежи еднакво навсякъде. Там, където резултатът може да се провери автоматично, грешката се хваща от проверката, а не от читателя, и рискът от уверено изречена неистина спада рязко.

На практика това значи да се търсят задачи с вградена проверка: код, покрит с тестове, данни със схема, изчисление с контролна сума, справка, която се сверява с първичния запис. Обратното също е вярно и се среща по-често. Оферта, анализ или обобщение на среща няма как да бъдат проверени от програма, затова отговорността там остава изцяло човешка и не се прехвърля на инструмента.

Заключение

Единайсет дни и 13 милиона реда впечатляват, но новото не е скоростта. Новото е, че при задача с машинна проверка резултатът от езиков модел може да се приеме, без да се вярва на самия модел, и точно такива задачи си струва да се търсят нарочно.

Помагаме на български организации да въвеждат AI там, където резултатът може да бъде проверен, а не само да изглежда убедителен. Услугите ни покриват одит, оценка на готовност, обучение на екипи и имплементация на специализирани AI автоматизации за всяка организация. Препоръчваме консултация при избор на задачи, в които автоматичната проверка е възможна. [Свържете се с нас за консултация: academy@razvivai.se]