Автоматизированная формализация не гарантирует корректность
Автоформализация — процесс перевода математических текстов с естественного языка в формальные системы, такие как Lean, — становится всё более распространённым инструментом проверки математических утверждений, включая те, что создаёт ИИ. OpenAI недавно анонсировала доказательство существования blow-up решений уравнений Navier-Stokes именно таким методом. Однако новое исследование Alexander Bastounis, Fabian Circelli и Anders C. Hansen указывает на фундаментальную проблему: сама по себе успешная формальная верификация в Lean не означает, что исходное доказательство на естественном языке корректно.
Почему перевод столь сложен
Авторы исследования пришли к математически строгому выводу: проблема семантически точного перевода математического текста имеет бесконечный уровень сложности в иерархии Solvability Complexity Index (SCI). Иными словами, она сложнее любой вычислимой задачи, включая проблему остановки Тьюринга, которая находится на уровне SCI = 1.
Главная причина — неоднозначность естественного языка. Математические тексты полны скрытых предположений, сокращений и двусмысленных формулировок, которые люди способны правильно интерпретировать на основе контекста и опыта. ИИ-система, выполняющая автоформализацию, должна разрешить все эти неоднозначности, чтобы создать семантически корректное формальное доказательство. Это теоретически неразрешимо в общем случае.
Практические примеры ошибок перевода
Чтобы продемонстрировать масштаб проблемы, авторы приводят конкретные примеры, где ИИ неправильно перевёл математические утверждения и доказательства в Lean. В частности, они проанализировали анонсированное OpenAI доказательство blow-up для уравнений Navier-Stokes и обнаружили, что формализованное Lean-доказательство не соответствует исходному доказательству на естественном языке.
Хотя формальная верификация в Lean проходит успешно (Lean может автоматически проверить синтаксис и логику формального текста), это лишь подтверждает, что переведённое утверждение логически верно внутри формальной системы. Это не гарантирует, что переведённая версия выражает именно то, что было написано в оригинальном доказательстве на естественном языке.
Подразумеваемые последствия
Результаты исследования ставят под сомнение надёжность автоматизированной проверки как замены человеческой проверке для критических математических результатов. Даже если ИИ успешно формализует доказательство и оно проходит механическую верификацию, нет гарантии, что результат корректен в том виде, как его исходно сформулировал человек.
Это не означает, что автоформализация бесполезна — она может быть полезным вспомогательным инструментом. Однако её нельзя рассматривать как окончательное подтверждение корректности математического результата без дополнительной проверки человеком.