Изследователски екип от Лабораторията за език и интелигентност на Принстънския университет (PLI) публикува новаторска статия за Goedel-Architect, агентна рамка за доказване на формални теореми, която постига най-съвременни резултати на малка част от цената на съществуващите системи. Гръбнакът на рамката е DeepSeek-V4-Flash, най-новият голям езиков модел с отворен код от китайската AI компания DeepSeek.
Резултатите са поразителни. На бенчмарка PutnamBench — стандартен тестов набор от 672 задачи от математическото състезание на William Lowell Putnam — Goedel-Architect постигна 75,6% проходимост при обща цена на API от само 294 USD. За сравнение, Hilbert, конкуриращ се конвейер с отворен код, захранван от Gemini 2.5 Pro на Google, струва приблизително 170 000 USD, за да завърши същото бенчмарк — приблизително 500-кратно предимство в разходите. Goedel-Architect също надмина Hilbert по отношение на преминаването (75,6% срещу 70,0%), демонстрирайки, че архитектурните иновации на рамката, а не превъзходният хардуер, са движещи за подобрението.
Името Goedel-Architect отдава почит на Kurt Goedel, който е прекарал последните си години в Принстънския институт за напреднали изследвания. Екипът на Принстън се ръководи съвместно от Санджив Арора, теоретик на изчислителната сложност и носител на наградата ACM за 2011 г. в областта на компютърните технологии, и Данки Чен, професор от Принстън с над 90 000 цитирания в Google Scholar и опит в университета Цинхуа.
Основната иновация в Goedel-Architect е неговата "план" подход. Преди да опита каквото и да е доказателство, системата генерира насочена ациклична графика, определяща всички необходими дефиниции и леми заедно с техните зависимости. Всеки недоказан възел се изпраща към паралелни Lean теореми за доказване, а грешките задействат структуриран диагностичен процес. Когато даден възел не може да бъде доказан, доказващият изготвя доклад за анализ, който идентифицира дали предложението е невярно или твърде трудно, заедно с предложени поправки. Това създава итеративен цикъл на усъвършенстване, при който планът се развива в кръгове, като успешните доказателства се запазват, а неуспешните възли се заменят или разлагат.
Екипът потвърди подхода си в пет бенчмарка. На MiniF2F-теста, най-утвърденият състезателен тест по математика в гимназията с 244 задачи, Goedel-Architect реши 242 при pass@1 (99,2%), превръщайки се в първата система, която решава всички проблеми, когато е допълнена с помощта на естествен език. На IMO 2025 той реши 4 от 6; на Putnam 2025, 11 от 12. Системата реши 3 от 6 проблема от USAMO 2026, набор от тестове, създаден след прекъсване на всички модели за обучение, изключвайки замърсяване на данни.
Експериментите с контролирана аблация потвърдиха, че глобалната стратегия на Goedel-Architect фундаментално превъзхожда подходите за рекурсивно разлагане. Когато Hilbert беше пренесен към същия гръбнак на DeepSeek-V4-Flash, той достигна само 84,4% на MiniF2F срещу 99,2% на Goedel-Architect. Скелето на естествен език от по-големи модели може да помогне при проблеми, изискващи нелокално структурно вникване, но повечето проблеми не изискват тази патерица.
Тази работа представлява важен крайъгълен камък в правенето на инфраструктура за формално доказателство на теорема достъпна на два порядъка по-ниска цена.