Исследователи представляют LAMP, многоагентную платформу, которая синтезирует проверяемые в ядре доказательства Lean 4 для Комбинаторики на словах, предоставляя структурированные предметные знания через онтологию. Этот подход решает проблему отсутствия специализированных лемм в существующих доказывателях, обученных преимущественно на данных Mathlib.
- Авторы представляют новую формализацию Комбинаторики на словах в Lean 4, содержащую восемь модулей и 93 объявления основных определений и фундаментальных лемм.
- LAMP координирует Планировщик, Строитель и Верификатор с использованием доступа к предметной онтологии через Model Context Protocol без необходимости тонкой настройки доказывателя.
- В тестах на 90 теоремах трех уровней сложности LAMP синтезировал проверяемые доказательства для 96,7% случаев, превзойдя базовые варианты без каркаса и специализированные доказыватели.
- Исследования аблиации показывают, что удаление архитектуры с привязкой к инструментам или разделение Планировщика и Строителя снижает производительность примерно на 12 процентных пунктов.
Эта платформа обеспечивает надежный синтез доказательств в недостаточно представленных математических областях за счет использования явных структурных знаний, а не только возможностей модели.