StepFun-Formalizer: Unlocking the Autoformalization Potential of LLMs through Knowledge-Reasoning Fusion

--- title: КОНТЕКСТ И ПРОБЛЕМАТИКА --- ### message ## КОНТЕКСТ И ПРОБЛЕМАТИКА Autoformalization — это процесс преобразования математических утверждений на естественном языке в формальный язык, который может быть обработан системами формальной проверки доказательств или формальной верификации. Несмотря на значительные успехи, достигнутые благодаря применению моделей языкового обработки (LLMs), эта задача все еще столкнулась со значительными трудностями. Одной из главных проблем является низкая точность преобразования, вызванная недостаточным освоением моделями формального доменного знания и ограниченными способностями к резону при анализе естественного языка и выравнивании его с формальным представлением. Ключевыми требованиями для эффективного autoformalization являются: 1) полное понимание формальных объектов и знаний домена, необходимых для корректного идентификации и представления математических конструкций, и 2) способность к резонированию над естественным языком для точного отображения неформальных контекстов в формальные выражения. Без первого, модели не могут корректно опознавать формальные объекты; без второго, они не могут точно интерпретировать реальные контексты и сопоставить их с формальными выражениями. Существующие подходы часто падают в точности из-за нехватки этих ключевых способностей. Таким образом, необходимо разработать методологию, которая бы объединяла эти две составляющие в единый процесс обучения, позволяя моделям достигать высокой точности в autoformalization. ## ПРЕДЛОЖЕННЫЙ МЕТОД Чтобы решить выявленные проблемы, авторы представляют ThinkingF — комплексную пайплайн для синтеза данных и обучения моделей, нацеленную на улучшение обеих ключевых способностей. Эта пайплайн состоит из двух основных этапов: построение высококачественных датасетов и их использование в процессе обучения моделей. В первом этапе создаются два датасета. Первый датасет формируется путем дистилляции и выбора большого количества примеров, богатых формальным знанием. Этот датасет направлен на развитие глубокого понимания формального домена у моделей. Второй датасет формируется с помощью генерации неформально-формальных рассуждений, которые основываются на шаблонах, разработанных экспертами. Эти шаблоны помогают обучать модели к резонированию и выравниванию между неформальным и формальным языком. Во втором этапе применяются два метода обучения: Supervised Fine-Tuning (SFT) и Reinforcement Learning with Value-Reward (RLVR). Эти методы позволяют моделям не только освоить формальные знания, но и улучшить способность к резонированию и выравниванию. Архитектура моделей, полученных в результате этого процесса, основана на базовых LLMs размером 7B и 32B. Эти модели показывают высокую способность к формальному знанию и неформально-формальному выравниванию, что является результатом функционального слияния двух ключевых способностей. ## ЭКСПЕРИМЕНТАЛЬНЫЕ РЕЗУЛЬТАТЫ Для оценки эффективности предложенного подхода были проведены эксперименты на двух фундаментальных датасетах: FormalMATH-Lite и ProverBench. Модель StepFun-Formalizer-32B достигла рекордных результатов, показав BEq@1 (exact match accuracy) в 40.5% на FormalMATH-Lite и 26.7% на ProverBench. Эти результаты значительно превосходят результаты предыдущих моделей, как общего назначения, так и специализированных под autoformalization. Было показано, что модели, обученные с помощью ThinkingF, не только лучше понимают формальные объекты, но также эффективнее выравнивают неформальные контексты с формальными выражениями. Эти результаты демонстрируют значительный прогресс в решении проблем недостаточной точности, которая была характерна для предыдущих подходов. ## ПРАКТИЧЕСКАЯ ЗНАЧИМОСТЬ Предложенный подход имеет широкое применение в областях, требующих формальной верификации и автоматизации математических доказательств. Он может быть использован в разработке программного обеспечения, системах автоматической проверки доказательств, а также в образовательных целях для обучения студентов формальной математике. Преимущества этого подхода заключаются в высокой точности преобразования, что позволяет автоматизировать процесс преобразования неформальных математических утверждений в формальные, что значительно экономит время и усилия человека. Кроме того, этот подход может быть использован в различных научных и инженерных дисциплинах, где формальные выражения играют ключевую роль. ## ВЫВОДЫ И ПЕРСПЕКТИВЫ StepFun-Formalizer представляет собой значительный шаг вперед в области autoformalization. Он не только показывает высокую точность, но также открывает новые возможности для применения LLMs в формальных задачах. Будущие исследования могут фокуссироваться на дальнейшем улучшении моделей, особенно в области резонирования и выравнивания между неформальным и формальным языками, а также на расширении областей применения этого подхода.