Материал подготовлен автоматически по первоисточникам: ссылки на них — в конце статьи.
Ошибку в логическом доказательстве научились находить до того, как LLM формулирует подсказку студенту. В нерецензированном препринте North Carolina State University, Purdue University и Kennesaw State University, где числа получили сами авторы, дообучение подняло макро-F1 детектора с 0,191 до 0,709, но не устранило систематические ошибки. Для продуктов с формально проверяемыми действиями это аргумент в пользу отдельного детерминированного проверяющего компонента, а не ещё одного запроса к LLM.
Формальные правила отделили от генерации текста
Система работает в три этапа. Сначала детектор определяет тип ошибки, затем отдельный агент объясняет диагноз, а последний агент превращает объяснение в короткую наводящую подсказку без готового решения.
Детектор получает текущее состояние доказательства, выбранные студентом высказывания и правило вывода, которое тот пытался применить. Он выбирает один из четырёх диагнозов: шаг верен, выбрано неверное число высказываний, высказывания подходят другому правилу или не подходят ни одному правилу.
Авторы сравнили три варианта детектора. Первый использовал Llama 3.1 8B Instruct без дообучения, второй — ту же модель после обучения на размеченных действиях, третий — символический верификатор. Все последующие компоненты и их инструкции оставались одинаковыми, поэтому результат зависел именно от первоначального диагноза.
Верификатор не рассуждает на естественном языке. Он сначала сверяет число выбранных высказываний с требованиями правила, затем проверяет, совпадает ли их структура со схемой этого правила. Если нет, он перебирает остальные допустимые правила и определяет, подходит ли выбор хотя бы одному из них.
Например, переменная, которая несколько раз встречается в схеме правила, должна каждый раз соответствовать одному и тому же высказыванию. Модель может счесть внешне похожий шаг правильным, а формальная проверка обнаружит структурное несовпадение.
Хорошо написанная подсказка может объяснять не ту ошибку
Проверку провели на 600 сбалансированных действиях студентов. Макро-F1 — среднее качество распознавания по всем классам, где каждый класс имеет равный вес. Без дообучения детектор получил 0,191, после дообучения — 0,709.
Дообученная модель всё ещё путала структурно близкие случаи. В приведённом в работе примере базовая модель решила, что студент выбрал неверное число высказываний, а дообученная признала шаг правильным. Формальная проверка показала другую причину: выбранные высказывания соответствовали не тому правилу.
Следующие этапы обычно послушно сохраняли полученный диагноз. Это полезное свойство, когда диагноз верен, но опасное — когда ошибся первый компонент. Объяснение оставалось связным, а подсказка могла быть уместной по тону, не раскрывать решение и при этом направлять студента исправлять несуществующую проблему.
Поэтому верность передачи и правильность нельзя объединять в одну метрику. Первая показывает, сохранила ли LLM исходный диагноз при переформулировке. Вторая отвечает, соответствовал ли сам диагноз формальным правилам задачи.
Символический вариант использовали как источник эталонных меток, поэтому его результат нельзя считать независимой победой над моделями на обычном бенчмарке. Корректность реализации дополнительно проверяли люди на части примеров, однако автоматические оценщики не полностью воспроизвели экспертные оценки, особенно когда судили о педагогической уместности подсказок.
Архитектуру стоит менять там, где ошибку можно вычислить
Работа меняет планы команд, если продукт уже располагает формальными правилами, тестами или ожидаемым результатом отдельного шага. Такой источник истины стоит поставить перед LLM: программа определяет, что именно неверно, а модель решает, как это сообщить понятным языком.
Между проверкой и пользовательским текстом полезно сохранить отдельное объяснение диагноза. Оно создаёт проверяемую границу: по журналу видно, ошибся ли верификатор, исказил ли диагноз агент объяснения или потерял ли его генератор подсказки. При прямой генерации ответа из действия пользователя эти причины сливаются в один правдоподобный текст.
Подход может переноситься на проверку алгебраических преобразований, программ по тестам и запросов к базе по ожидаемому результату. Это пока направление для следующих экспериментов, а не подтверждённый результат работы.
Сам эксперимент охватывает один курс, один репетитор по пропозициональной логике, 32 задачи и 15 правил вывода. Проверялись локальные ошибки применения правил, но не выбор общей стратегии доказательства; влияние подсказок на обучение студентов также не измеряли. Поэтому для открытых рассуждений без формальной спецификации работа не даёт основания заменять LLM символическим модулем.
Верификатор тоже наследует ошибки схем и классификации, которые заложила команда. Практический вывод не в том, чтобы считать его безошибочным, а в том, чтобы сделать критический диагноз детерминированным, тестируемым и наблюдаемым отдельно от генерации текста.
Источники
Похоже на вашу задачу?
Расскажите, что собираете. За полчаса разложим на этапы и назовём сроки — это бесплатно и ни к чему не обязывает.
