Команда исследователей из Университета Саарланда (Katharina Stein, Chaahat Jain, Jörg Hoffmann, Alexander Koller) представила прорывной подход к автоматизированному планированию. В статье "Provably Complete Generalized Planning with LLMs" (arXiv:2609.27105, 22 сентября 2026 г.) описывается метод, который устраняет главный недостаток предыдущих решений: отсутствие гарантий полноты. Если ранее LLM могли генерировать Python-скрипты, работающие на тестовых данных, то новая система выдает не только план, но и математически строгое доказательство того, что этот план решает все возможные экземпляры задачи в заданной области.
Как это работает: от PDDL к Lean
Ключевая инновация заключается в использовании языка формальной верификации Lean. Авторы разработали семантически сохраняющее преобразование из языка описания планирования PDDL в Lean. Это позволяет перевести ограничения домена в форму, понятную для проверки теорем. Затем LLM (в данном случае GPT-5.6-Sol) генерирует два компонента:
- Обобщенный план (алгоритм решения).
- Формальное доказательство того, что план корректен для всех входных данных, удовлетворяющих спецификации домена.
Корректность доказательства проверяется ядром Lean, что исключает возможность ошибок, свойственных обычным LLM. Это переводит ИИ-планирование из категории эвристических методов в категорию математически доказуемых систем.
Результаты на бенчмарках
Эксперименты проводились на 13 широко используемых доменах планирования. Результаты демонстрируют высокую надежность подхода: система смогла сгенерировать валидные планы вместе с доказательствами полноты для абсолютного большинства тестовых случаев.
| Домен | Результат | Статус доказательства |
|---|---|---|
| 12 из 13 доменов | Успешно | Валидное (проверено ядром Lean) |
| 1 домен | Не удалось | — |
Таким образом, для 12 из 13 исследованных областей были получены не просто рабочие скрипты, а доказуемо полные обобщенные планы. Это значительный шаг вперед по сравнению с предыдущими работами, где полнота определялась только ручным анализом или тестированием на ограниченной выборке.
Почему это важно
Проблема «галлюцинаций» и непроверяемости решений LLM остается главным барьером для их внедрения в критически важные системы (логистика, робототехника, управление ресурсами). Представленный метод предлагает гибридный подход: генерация идей через LLM + строгая верификация через формальные методы. Это позволяет использовать мощь больших языковых моделей для поиска сложных решений, не жертвуя при этом надежностью и предсказуемостью.
Источник: arXiv cs.AI ↗