«Proof in the Code» — новая книга о цифровой проверке математических истин
Книга рассказывает об истории компьютерных программ, способных решать сложные математические задачи и которые сегодня используют как математики, так и разработчики систем искусственного интеллекта.
Отправная точка повествования — неофициальное участие созданной командой DeepMind системы искусственного интеллекта AlphaProof в Международной математической олимпиаде 2024 года, где лучшие студенты-математики со всего мира в течение двух дней решали сложные математические задачи. В итоге AlphaProof показала результат на уровне серебряного призёра.
Итак, AlphaProof — это «решатель теорем», то есть программа, которая проверяет математические утверждения. Всего несколько лет назад обучение систем искусственного интеллекта автоматизации математических рассуждений считалось очень сложной задачей. Но разработчики надеялись, что их усилия позволят развить у ИИ более широкие способности к логическому рассуждению. Автор книги Кевин Хартнетт отмечает, что подобные системы в состоянии потенциально понизить склонность моделей к так называемым «галлюцинациям» — выдумыванию несуществующих фактов.
Успех таких программ во многом связан с Lean — инструментом для проверки программного кода, который Лео де Мура будучи инженером Microsoft Research запустил ещё в 2013 году. В своей книге Хартнетт прослеживает превращение узкоспециализированного софтверного проекта Lean в инструмент, важный сегодня прежде всего для математиков и специалистов по ИИ. История Lean – пример сотрудничества множества людей, увидевших в нём новый способ оценки математических истин и повлиявших на то, чтобы сделать его более удобным для пользователей.
Чтобы объяснить, как использование Lean может быть применено к математическим задачам, автор проводит параллели между математикой и программированием: последовательная логическая цепочка доказательства похожа на код программы, а пробел в логике доказательства подобен «багу» в коде.
Lean и другие подобные программы-ассистенты сами не создают доказательства, но помогают проверять правильность уже существующих для подтверждения новых фактов при использовании их в новых доказательствах. Однако, проверка существующих математических доказательств объёмом в сотни страниц может занимать месяцы.
Громоздкость таких программ требовала другого представления математических данных. Проблема была в том, что математикам приходилось «переводить» задачи на язык кода и с нуля создавать библиотеки базовых понятий. Автор приводит забавный пример: прежде чем использовать элементарное неравенство программа предложила учёному доказать, что 2 не равно 1 — утверждение, которое в обычной жизни никто и не подумал бы обосновывать.
Долгое время в библиотеках Lean попросту не хватало данных, чтобы стать полезным математикам, — а новых не появлялось без притока новых пользователей. Одним из переломных стал проект 2018 года по переводу «перфектоидных пространств» на язык Lean работа заняла месяцы и тысячи строк кода. К 2025 году, как пишет Хартнетт, десятки тысяч пользователей в науке и технологической индустрии уже вели на основе Lean масштабные проекты . В их число вошли и исследователи ИИ, использующие обширную математическую библиотеку Lean для обучения таких ИИ-моделей, как AlphaProof.
Инженеров и математиков объединило стремление создать «машину истины» — программу, способную гарантировать стопроцентную корректность логической цепочки. Если для де Муры это означало уверенность в безошибочности кода обычных программ вроде Microsoft Word, то для математиков — возможность сделать поиск доказательств более строгим и упорядоченным.
В рецензии к книге Хартнетта отмечается, что для интересующихся математикой это очень увлекательное и насыщенное деталями чтение о новой главе в истории математической науки.
Источник: ScienceNews
Изображение для иллюстрации. Источник: Magnific.com.
