Automated Formalization via Conceptual Retrieval-Augmented LLMs

## Контекст Интерактивные теоремпроверы (ITPs) требуют ручного формализации, которая трудоемка и требует специальной экспертной подготовки. Рост интереса к искусству математического программирования привел к развитию автоматизированных методов формализации, которые могут существенно сократить время и усилия для формализации. Однако эти методы сталкиваются с двумя ключевыми проблемами: потенциальной халтурностью (например, неопределенные предикаты, неправильное использование символов, несовместимость версий) и семантическим пробелом, вызванным неясностью или отсутствием подробных данных в естественном языке. Эти проблемы значительно ограничивают эффективность автоматизации. Работа статьи призвана решить эти задачи, предлагая новую модель, которая будет улучшать работу существующих автоматизированных инструментов. ## Метод Мы предлагаем разработать CRAMF (Concept-driven Retrieval-Augmented Mathematical Formalization), которая улучшает LLM-based autoformalizer. Работа CRAMF основывается на поисковой методологии, которая позволяет внедрять контекстные сигналы в процесс генерации кода. Мы предлагаем автоматическую конструкцию классификации математических понятий и их определений из Mathlib4 — стандартной математической библиотеки Lean 4. Для улучшения точности и устранения проблемы полиморфизма мы предлагаем стратегию контекстного запроса, используя дополнительные доменные сигналы. Также мы разрабатываем двухканальную стратегию поиска с повторным оцениванием, чтобы обеспечить высокую точность поиска. ## Результаты Мы проводим эксперименты на стандартных тестовых наборах miniF2F, ProofNet и произвольном AdvancedMath бенчмарке. CRAMF показывает последовательные улучшения в точности формализации. Мы сравниваем результаты с текущими стандартными методами и показываем, что CRAMF добивается до 62.1% улучшения в точности и 29.9% в среднем. Это указывает на последовательность CRAMF в сильном значительном улучшении существующих методов. ## Значимость Мы отмечаем, что CRAMF может быть широко применена в сфере автоматизированной формализации математических задач. Эта модель может быть применена в широких областях, включая формализацию математических теорий, автоматическое проверивание теорем, а также в образовательных целях, помогая учащимся и экспертам в математике. Мы также отмечаем, что CRAMF может повысить эффективность работы существующих систем, таких как Lean 4 и другие ITPs, и улучшить пользовательский опыт. ## Выводы Мы представляем CRAMF, новую модель для автоматизированной формализации, которая позволяет улучшить методы, исполь