Проблема изолированных утверждений
Большинство современных систем автоформализации (перевод естественного языка в формальные языки, такие как Lean или Coq) фокусируются на трансляции отдельных математических утверждений. Однако реальные формализационные усилия в математике и компьютерных науках носят «теоретический» характер: они требуют построения целой сети аксиом, определений и лемм, прежде чем можно будет сформулировать целевую теорему. Изолированный перевод часто терпит неудачу из-за отсутствия контекста.
Сдвиг парадигмы: Theory-Level Autoformalization
В работе, представленной на ICML 2026 (Spotlight), авторы Marcus J. Min, Mike He, Zhaoyu Li и соавторы аргументируют необходимость перехода к Theory-Level Autoformalization. Это подход, при котором система формализует не просто одно предложение, а целую теорию, включая все её внутренние зависимости, как структурированную библиотеку. Такой подход позволяет создавать единые базы формальных знаний (Unified Formal Knowledge Bases), которые можно переиспользовать и проверять комплексно.
Ключевые вызовы и направления развития
Авторы выделяют три основных пути решения проблем, связанных с масштабированием формализации:
- Управление зависимостями: Алгоритмы должны уметь выявлять и восстанавливать скрытые связи между определениями и теоремами в больших текстах.
- Структурирование библиотек: Переход от плоского списка утверждений к иерархическим структурам, отражающим логику математической дисциплины.
- Верификация целостности: Обеспечение того, что вся формализованная библиотека логически непротиворечива, а не только каждая отдельная строка.
Значение для индустрии
Переход к теоретическому уровню автоформализации открывает путь к созданию надежных AI-ассистентов, способных не просто переводить текст, а понимать и верифицировать сложные математические доказательства и программные спецификации в их полном объеме. Это снижает риск галлюцинаций моделей, так как проверка происходит на уровне всей системы знаний, а не изолированных фрагментов.
Источник: arXiv cs.AI ↗