Материал подготовлен автоматически по первоисточникам: ссылки на них — в конце статьи.
Олимпиадного ИИ-агента научили исправлять ранние ошибки, запрашивать недостающие знания и проверять, что итог действительно решает исходную задачу. В нерецензированном препринте, где все числа получили сами авторы, HOA решил на Lean-Eval 251 задачу из 304 против 112 у официального результата GPT-5.6. Для команд это аргумент в пользу нескольких специализированных сессий вместо одного длинного диалога с моделью.
Три канала обратной связи закрывают разные сбои
HOA работает на уровне процесса: управляет несколькими сессиями модели, инструментами и общим решением. Рабочая сессия строит текущий артефакт — текст решения, программу или формальное доказательство. Отдельная сессия-рецензент проверяет его по исходному условию и заранее заданным критериям.
Рецензент получает зафиксированную версию артефакта и не видит скрытые рассуждения рабочего агента. Он не может молча исправить решение, а возвращает конкретные замечания: пропущен случай, использован неверный переход, доказано соседнее утверждение. Рабочая сессия вносит правки, после чего цикл повторяется в пределах выделенного бюджета.
Вики закрывает другой класс проблем. Когда агент может сформулировать, какого факта или метода ему не хватает, поиск возвращает небольшую подборку записей с указанием происхождения. Математическая вики хранит проверенные объявления Lean и переиспользуемые леммы, химическая — определения, реакции, формулы и шаблоны решений из подготовленных источников.
Третий канал — предметный верификатор. Для математики и формализованной физики Comparator собирает доказательство в изолированной среде, сверяет формулировку с доверенным условием, ограничивает допустимые аксиомы и передаёт результат ядру Lean. Для программирования агент запускает код и тесты. Кандидат принимают, только когда прошли и смысловая проверка, и доступные машинные проверки.
Процесс продолжает находить решения после остановки одиночного агента
HOA получил полные баллы на наборах IMO, IPhO и IOI, почти полный результат на IChO и решил 672 задачи из 672 на PutnamBench. Формальные математические результаты проверяло ядро Lean, поэтому успешная попытка означает не только положительную оценку другой модели.
На подмножестве PutnamBench открытая модель Kimi K3 с прямым вызовом решила 2% задач, а с полным процессом HOA — 94%. Разрыв показывает, что базовая модель определяет не весь результат: независимая проверка и повторный ремонт позволяют использовать знания, которые модель не смогла собрать в одной попытке.
Деталь из одной траектории показывает роль вики. При доказательстве разложения тензорного квадрата агент извлёк ранее проверенные записи о представлениях G2 и применил готовые объявления Lean, не воспроизводя их доказательства. Вики здесь работает как библиотека типизированных строительных блоков, а не как набор текстовых подсказок.
Проверки охватывали школьные олимпиады по математике, физике, химии и программированию, PutnamBench и формальную математику Lean-Eval. Использовались закрытая и открытые модели, но тесты не доказывают перенос результата на произвольные исследования. Сравнения также различаются по времени работы, доступным инструментам и вычислительному бюджету, поэтому из них нельзя вывести экономию стоимости.
Командам стоит копировать границы ответственности, а не весь стек
Работа меняет планы проектов, где модель ведёт длинную задачу и ошибка на раннем шаге портит весь результат. Вместо одного агента, который одновременно создаёт, оценивает и принимает собственный ответ, полезно разделить построение артефакта, смысловую приёмку и объективную проверку.
Такой процесс требует явного критерия готовности. Рецензент должен видеть исходную постановку и неизменённый кандидат, а не пересказ рабочего агента. Машинный верификатор должен проверять именно то свойство, которое команда считает успехом: компиляцию недостаточно считать доказательством корректности, если система может изменить условие или подключить запрещённую зависимость.
Вики имеет смысл строить вокруг подтверждённых результатов с происхождением, версиями и статусом проверки. Обычный поиск по истории диалогов не даёт той же гарантии: текст может оказаться устаревшим или ошибочным. В HOA принятые доказательства превращаются в записи, которые следующая сессия может подключить непосредственно к формальному решению.
Авторы предоставляют реализацию процесса, подсказки, схему рецензирования, снимок вики, журналы запусков и артефакты Lean. Это делает воспроизводимым управляющий слой, хотя используемые закрытые модели по-прежнему остаются внешней зависимостью. Для прикладной команды главный вывод уже проверяем: дополнительный бюджет приносит пользу, когда новые попытки получают независимые замечания и объективный сигнал, а не просто продолжают прежнюю цепочку рассуждений.
Источники
Иллюстрация: рисунок из статьи «Humanize Olympiad Agents: A Multi-Session Workflow for Olympiad Problem Solving with Solve, Review, Wiki, Verify», Zhengyang Zhang, Jing Xiong, Hongzhou Lin и др., CC BY 4.0
Похоже на вашу задачу?
Расскажите, что собираете. За полчаса разложим на этапы и назовём сроки — это бесплатно и ни к чему не обязывает.
