В Университете Южной Калифорнии студентка Минда Ли протестировала GPT-5 на 56 задачах по Idris — языке с зависимыми типами, который встречается всего в 2275 репозиториях против 24 миллионов у Python

В Университете Южной Калифорнии студентка Минда Ли протестировала GPT-5 на 56 задачах по Idris — языке с зависимыми типами, который встречается всего в 2275 репозиториях против 24 миллионов у Python. Базовая модель решала лишь 39 % заданий, поскольку почти не видела примеров этого языка в обучении. После внедрения цикла исправлений успех вырос до 96 % — 54 задачи из 56 решены верно.

Научный принцип прост: компилятор Idris выдаёт точные сообщения об ошибках — указывает на несоответствие типов, пропущенное имя или неполную ветвь именно в нужном месте кода. Модель получала это сообщение обратно, анализировала проблему и переписывала фрагмент. Общие руководства и документация давали лишь слабый прирост до 61 %, а вот локальная точная обратная связь работала революционно эффективно.

Похожие подходы уже применяют в других строгих системах: например, в CoCoGen для генерации кода с учётом контекста проекта или в инструментах для математических доказательств на Coq и Lean. Метод показывает, что для ИИ важнее не гигантский объём данных, а качество сигнала об ошибках — это открывает путь к обучению на редких языках, формальной верификации и даже юридических или научных рассуждениях.

Источник: vk.com

Комментарии: