Проект Forall представляет собой специализированного ИИ-агента, предназначенного для автоматизации написания формальных доказательств на языке Lean. Инструмент интегрирует возможности LLM с системами автоматической проверки корректности кода, позволяя разработчикам и математикам генерировать верифицируемые доказательства теорем, минимизируя риск логических ошибок, свойственных стандартным генеративным моделям при работе со сложными математическими структурами.
Основная проблема существующих ИИ-кодеров заключается в склонности к «галлюцинациям» при написании кода, который должен строго следовать математической логике. Forall решает эту задачу через итеративный цикл обратной связи: агент генерирует фрагмент доказательства, отправляет его на компиляцию в Lean, анализирует сообщения об ошибках и автоматически корректирует код до тех пор, пока доказательство не будет успешно принято системой проверки.
Такой подход переводит процесс разработки из режима «генерации текста» в режим «верифицируемого программирования». Использование формальных методов в связке с LLM позволяет создавать надежные программные компоненты и математические выкладки, где каждый шаг подтвержден машинным алгоритмом, а не просто вероятностным предсказанием следующего токена.
Ключевые факты
- Forall использует язык формальной верификации Lean 4 для проверки корректности сгенерированных доказательств.
- Система реализует агентный цикл, включающий автоматическую обработку логов ошибок компилятора для самокоррекции.
- Инструмент ориентирован на автоматизацию задач в области формальной математики и верификации программного обеспечения.
- Проект опубликован с открытым исходным кодом на платформе GitHub под лицензией MIT.