MASA: Многоагентные системы на основе LLM для автоформализации

Основная информация

• ID статьи: 2510.08988
• Название: MASA: LLM-Driven Multi-Agent Systems for Autoformalization
• Авторы: Lan Zhang (University of Manchester), Marco Valentino (University of Sheffield), André Freitas (University of Manchester, Idiap Research Institute, National Biomarker Centre)
• Классификация: cs.CL (Вычислительная лингвистика), cs.FL (Формальные языки)
• Дата публикации: 10 октября 2025 г. (препринт arXiv)
• Ссылка на статью: https://arxiv.org/abs/2510.08988

Аннотация

Автоформализация играет ключевую роль в связывании естественного языка и формального рассуждения. В данной работе предлагается MASA — фреймворк многоагентной системы на основе больших языковых моделей (LLM) для задач автоформализации. MASA использует сотрудничающие агенты для преобразования утверждений на естественном языке в их формальные представления. Архитектура MASA подчеркивает модульность, гибкость и масштабируемость, позволяя беспрепятственно интегрировать новых агентов и инструменты для адаптации к быстро развивающейся области. Авторы демонстрируют эффективность MASA через примеры использования реальных математических определений и экспериментов на наборах данных формальной математики. Данная работа подчеркивает потенциал многоагентных систем, управляемых взаимодействием LLM и средств доказательства теорем, в повышении эффективности и надежности автоформализации.

Научный контекст и мотивация

Определение проблемы

Автоформализация — это задача автоматического преобразования математических утверждений на естественном языке в машиночитаемые формулы формальной логики. Основные вызовы этой проблемы заключаются в следующем:

1. Семантический разрыв: огромное различие между неоднозначностью естественного языка и строгостью формального языка
2. Сложность: реальные математические утверждения часто включают сложные концепции и цепочки рассуждений
3. Требования к точности: результаты формализации должны быть корректны как синтаксически, так и семантически

Значимость проблемы

Автоформализация имеет важное значение:

• Математическая верификация: обеспечивает основу для доказательства теорем и математической верификации
• Прозрачность рассуждений: формальное рассуждение более систематично, прозрачно и строго по сравнению с рассуждением на естественном языке
• Потребность в автоматизации: ручная формализация требует значительных экспертных знаний и временных затрат

Ограничения существующих подходов

Существующие системы автоформализации на основе LLM имеют следующие проблемы:

1. Ограничения монолитной архитектуры: одна LLM с трудом справляется со сложными реальными задачами автоформализации
2. Отсутствие модульности: существующие реализации не обладают модульностью, гибкостью и масштабируемостью
3. Недостаточное взаимодействие компонентов: невозможно эффективно интегрировать несколько взаимодействующих компонентов

Научная мотивация

Авторы предлагают фреймворк MASA с целью:

• Построить модульную многоагентную систему для решения сложности автоформализации
• Предоставить гибкий и масштабируемый фреймворк для быстрой разработки и расширения системы исследователями
• Повысить эффективность и надежность автоформализации через сотрудничество агентов

Основные вклады

1. Предложен модульный многоагентный фреймворк: MASA предоставляет модульный фреймворк для построения многоагентных систем автоформализации с хорошей гибкостью и масштабируемостью
2. Демонстрация реальных приложений: формализация реальных математических определений агентами подчеркивает практический потенциал фреймворка
3. Систематическая оценка: оценка фреймворка в трех многоагентных конфигурациях доказывает его эффективность и предоставляет ценные выводы. Итоговая система итеративного самосовершенствования достигает 35,25% и 61,89% синтаксически корректных и семантически согласованных формализаций на Qwen2.5-7B и GPT-4.1-mini соответственно
4. Открытая реализация: предоставление полного кода и данных снижает барьер входа для исследований

Подробное описание методов

Определение задачи

Автоформализация может быть определена как функция преобразования A, которая отображает утверждение на естественном языке s в его формальное представление φ = A(s). Традиционные методы реализуют это через подсказки LLM: A = LLM(prompt). MASA расширяет это определение, реализуя более сложный процесс преобразования через многоагентную систему.

Архитектура модели

Фреймворк MASA содержит пять основных компонентов:

1. Agent (Агент)

Агенты — это базовые элементы, выполняющие специфические функции, включая:

• AutoformalizationAgent: выполняет автоформализацию с несколькими примерами
• HardCritiqueAgent: предоставляет критику на синтаксическом уровне на основе средства доказательства теорем
• SoftCritiqueAgent: предоставляет критику на семантическом уровне на основе LLM
• FormalRefinementAgent: улучшает формальный код на основе жесткой критики
• InformalRefinementAgent: улучшает формальный код на основе мягкой критики
• DenoisingAgent: агент инструмента удаления шума
• ImportRetrievalAgent: агент инструмента извлечения импортов

2. Large Language Model (Большая языковая модель)

LLM предоставляет агентам возможности рассуждения и языка, поддерживая:

• Модели OpenAI (такие как GPT-4.1-mini)
• Локальные модели HuggingFace (такие как Qwen2.5-7B, DeepSeek-Math)

3. Knowledge Base (База знаний)

Хранит информацию о библиотеках формальных языков, поддерживая извлечение соответствующих знаний. Текущая реализация включает базу знаний формальных утверждений и доказательств Isabelle/HOL.

4. Retriever (Извлекатель)

Ранжирует релевантность точек данных в математической библиотеке; текущая реализация основана на методе BM25.

5. Theorem Prover (Средство доказательства теорем)

Проверяет синтаксическую корректность и логичность формализации, предоставляя сообщения об ошибках. Поддерживает:

• Isabelle (через выделенный сервер)
• Lean4 (через REPL)

Технические инновации

1. Модульный дизайн: использование абстрактных базовых классов для удобного расширения новых агентов и инструментов
2. Многоуровневый механизм критики: объединение жесткой критики (синтаксис) и мягкой критики (семантика)
3. Процесс итеративного улучшения: поддержка многораундного сотрудничества агентов с самосовершенствованием
4. Интеграция инструментальных агентов: интеграция практических инструментов, таких как удаление шума и извлечение импортов

Экспериментальная установка

Наборы данных

1. miniF2F: предоставляет реальные формализации Isabelle/HOL и Lean4 для тестирования
2. ProofNet: предоставляет реальные формализации кода Lean4

Метрики оценки

Синтаксическая корректность

• Pass Rate: процент синтаксически корректных формализаций

Семантическая оценка

• BLEU-4: степень перекрытия n-грамм с реальной формализацией
• ChrF: F-score на уровне символов
• RUBY: метрика оценки переноса кода

Оценка агентов

• Alignment Faithfulness (AF): точно ли формальный код согласуется с семантикой естественного языка
• Formalization Correctness (FC): является ли сам формальный код действительным, естественным и хорошо отформатированным

Методы сравнения

• Подсказки с нулевыми примерами (ZS): прямое использование LLM для формализации
• Подсказки с несколькими примерами (FS): формализация с использованием 3 примеров
• Различные комбинации LLM: GPT-4.1-mini, DeepSeek-Math-7B, Qwen2.5-7B

Детали реализации

• Использование GPT-4.1-mini как LLM бэкенда для агента мягкой критики
• Поддержка двух формальных языков: Isabelle/HOL и Lean4
• Предоставление полной реализации на Python и примеров Jupyter Notebook

Результаты экспериментов

Основные результаты

Система улучшения формальной критики (Таблица 1)

miniF2F-Test (Isabelle/HOL):

• GPT-4.1-mini с нулевыми примерами: Pass Rate 65,57% → 77,05% (+11,48%)
• GPT-4.1-mini с несколькими примерами: Pass Rate 76,23% → 86,48% (+10,25%)
• DeepSeek-Math с несколькими примерами: Pass Rate 29,10% → 36,48% (+7,38%)

ProofNet-Test (Lean4):

• GPT-4.1-mini с нулевыми примерами: Pass Rate 3,30% → 3,85% (+0,55%)
• GPT-4.1-mini с несколькими примерами: Pass Rate 12,09% → 14,84% (+2,75%)

Система неформального улучшения мягкой критики (Таблица 2)

miniF2F (Lean4):

• DeepSeek-Math + GPT-4.1-mini улучшение: AF 38,52% → 90,57%, FC 47,54% → 79,92%
• Qwen2.5-7B + GPT-4.1-mini улучшение: AF 54,51% → 93,44%, FC 62,70% → 85,25%

Эксперименты итеративного самосовершенствования

Результаты на Рисунке 2 показывают:

• Qwen2.5-7B: после 4 раундов итераций доля синтаксически корректных и семантически согласованных формализаций достигает 35,25%
• GPT-4.1-mini: после 4 раундов итераций доля синтаксически корректных и семантически согласованных формализаций достигает 61,89%

Экспериментальные выводы

1. Несколько примеров превосходят ноль примеров: обучение с несколькими примерами значительно повышает производительность во всех конфигурациях
2. Влияние возможностей модели: более мощные модели (GPT-4.1-mini) показывают лучшие результаты в формальном улучшении
3. Эффективность итеративного улучшения: многораундные итерации постоянно повышают качество формализации
4. Кросс-модельное улучшение: более мощные модели могут улучшать выходные данные менее мощных моделей

Связанные работы

Исследования автоформализации

• Методы подсказок: Wu et al. (2022) и другие используют подсказки LLM для автоформализации
• Генерация данных: Jiang et al. (2024) и Liu et al. (2025b) разработали крупномасштабные параллельные корпусы
• Системные реализации: существующие системы не обладают модульностью и масштабируемостью

Многоагентные системы

• Области применения: операционные системы, медицинское образование, проверка ответов и т. д.
• Задачи рассуждения: арифметическое рассуждение и общее рассуждение
• Приложения автоформализации: исследования многоагентных систем в области автоформализации ограничены

Заключение и обсуждение

Основные выводы

1. Эффективность фреймворка: MASA успешно построила модульную многоагентную систему автоформализации
2. Повышение производительности: сотрудничество многоагентной системы значительно повышает точность автоформализации
3. Практическая ценность: фреймворк предоставляет исследователям гибкую платформу разработки

Ограничения

1. Отсутствие центрального управления: система не имеет центрального агента для распределения и управления различными агентами
2. Ограничения семантической оценки: семантическая оценка ограничена высокоуровневыми суждениями; требуются более детальные стандарты оценки
3. Зависимость от модели: производительность системы в значительной степени зависит от возможностей базовой LLM

Будущие направления

1. Усиление центрального управления: разработка более продвинутых механизмов управления многоагентными системами
2. Уточнение оценки: установление более детальных стандартов семантической оценки
3. Расширение приложений: применение фреймворка к более широкому спектру задач формализации

Глубокая оценка

Преимущества

1. Высокая инновационность: первый систематический многоагентный фреймворк для автоформализации
2. Разумный дизайн: элегантный модульный архитектурный дизайн, легко расширяемый
3. Достаточные эксперименты: охватывает множество конфигураций и метрик оценки
4. Высокая практическая ценность: открытая реализация снижает барьер входа для исследований
5. Убедительные результаты: метод верифицирован на нескольких наборах данных

Недостатки

1. Недостаточный теоретический анализ: отсутствует теоретический анализ механизмов сотрудничества многоагентной системы
2. Анализ вычислительных затрат: анализ вычислительных издержек многоагентной системы недостаточен
3. Распространение ошибок: недостаточно глубокий анализ проблемы распространения ошибок между агентами
4. Ограничения оценки: семантическая оценка все еще зависит от суждения LLM, что может привести к смещению

Влияние

1. Академический вклад: предоставляет новую парадигму для исследований автоформализации
2. Практическая ценность: фреймворк может быть непосредственно использован для разработки практических приложений
3. Воспроизводимость: полная открытая реализация гарантирует воспроизводимость
4. Продвижение развития: может способствовать применению многоагентных систем в области формализации

Применимые сценарии

1. Математическая формализация: подходит для автоформализации сложных математических теорем и определений
2. Образовательные приложения: может использоваться для обучения формализации в математическом образовании
3. Инструмент исследования: предоставляет базовую платформу для исследований автоформализации
4. Промышленные приложения: может быть интегрирован в программные системы, требующие формальной верификации

Библиография

Ключевые ссылки включают:

• Wu et al. (2022): Autoformalization with large language models
• Zheng et al. (2022): miniF2F: a cross-system benchmark for formal olympiad-level mathematics
• Azerbayev et al. (2023): ProofNet: Autoformalizing and formally proving undergraduate-level mathematics
• Jiang et al. (2023): Draft, sketch, and prove: Guiding formal theorem provers with informal proofs

Резюме: MASA — это инновационный многоагентный фреймворк для автоформализации, который значительно повышает эффективность автоформализации благодаря модульному дизайну и сотрудничеству агентов. Данная работа демонстрирует отличные результаты в технических инновациях, экспериментальной верификации и практической ценности, открывая новое направление в исследованиях автоформализации. Несмотря на некоторые ограничения, открытая реализация и хорошая масштабируемость делают её важным вкладом в данную область.