Суть проблемы: синтаксис против семантики
ИИ-системы генерируют огромное количество доказательств, но их стиль кардинально отличается от человеческого. Авторы ввели методологию «симулированного сотрудничества» для анализа 9 крупных человеческих коллабораций в Lean. В датасет вошло 4,7 млн определений и более 6 000 коммитов. Цель — понять, как ИИ выбирает следующие шаги и где его предпочтения расходятся с математиками.
Три ключевых отклонения ИИ-агентов
Анализ показал систематические слепые зоны алгоритмов:
- Охота за «дырами»: ИИ-агенты значительно чаще людей обращают внимание на явно отмеченные пробелы в коде (placeholders), игнорируя общую структуру.
- Избегание сложности: Агенты демонстрируют явную антипатию к плотно связанным центрам доказательств и сложным, неожиданным целям (goals). Они предпочитают «легкие» пути.
- Регуляризация неожиданного: ИИ привлекают неожиданные тела доказательств, но тут же «сглаживают» их, приводя к базовому, предсказуемому виду, теряя математическую изюминку.
Сравнение предпочтений: Люди vs AI
| Характеристика | Предпочтения людей | Предпочтения AI-агентов |
|---|---|---|
| Фокус внимания | Глубокая семантика и связи | Поверхностный синтаксис и явные маркеры |
| Отношение к сложности | Принятие сложных целей | Избегание плотно связанных узлов |
| Обработка неожиданностей | Использование как инструмента | Регуляризация к базовому уровню |
Почему это важно
Результаты указывают на критические «слепые зоны» в текущих моделях. Для эффективного человеческого-машинного сотрудничества в математике необходимы новые вмешательства, которые заставят ИИ выходить за рамки поверхностного синтаксиса и учиться работать с глубокой семантикой сложных доказательств.
Источник: arXiv cs.AI ↗