Проблема слепой выборки
Автоматические доказатели теорем часто полагаются на выборку (sampling) языковых моделей. Однако в таких системах, как Lean 4, каждый неудачный шаг отвергается компилятором с точным сообщением об ошибке. Традиционные подходы игнорируют эту ценную информацию, просто отбрасывая неудачную тактику и пробуя новую. Авторы работы — Haotian Deng, Chris Farber, Sonal Narasimha, Samskrithi Sivakumar и Yexiang Xue — предлагают иной подход: исправлять провалившуюся тактику на месте, используя подсказки от компилятора.
Механика Bounded Repair
Предложенный модуль работает в режиме реального времени на уровне каждого шага. Алгоритм генерирует $K$ кандидатов тактик. Если выбранная тактика вызывает ошибку, система не отбрасывает её, а подает сообщение об ошибке в предварительно обученную модель-репаратор. Этот процесс ограничен: каждая тактика может быть исправлена не более $R$ раз. Это позволяет находить баланс между поиском новых решений и исправлением существующих.
Результаты на LeanDojo
Эксперименты проводились на подмножестве из 1 990 теорем бенчмарка LeanDojo. Метод исправления превзошел базовый подход только на основе выборки при всех протестированных бюджетах кандидатов ($K \in \{1, 3, 5, 8\}$). Ключевые метрики эффективности представлены ниже:
| Метрика | Значение / Описание |
|---|---|
| Относительный прирост | До 32% по сравнению с базовой выборкой |
| Дополнительные решенные теоремы | 82 теоремы на subset из 1 990 |
| Эффективность первого исправления | 84–96% от общего прироста дает первая попытка ремонта |
| Тип ошибок | Прирост достигается за счет исправления мелких ошибок выполнения, а не структурных (например, несоответствия типов) |
Компромисс: время против результата
Исправление тактик не бесплатно: оно увеличивает время выполнения (runtime). Однако этот компромисс предсказуем. Наибольшую отдачу метод приносит, когда выборка ограничена. Прирост «фронтально загружен»: первая попытка ремонта захватывает подавляющую часть выгоды. Это означает, что система быстро находит решения, не тратя ресурсы на глубокие переборы.
Валидация на Lean Workbook
Для подтверждения надежности метода результаты были реплицированы на втором бенчмарке — Lean Workbook. Там подход не только сохранил эффективность, но и практически удвоил скорость решения задач (solve rate) без единой регрессии (zero regressions). Это доказывает, что использование обратной связи от компилятора для целевого исправления тактик является надежным путем к повышению автономности AI-доказателей.
Источник: arXiv cs.AI ↗