LLM-ы ускорили работу исследователей: от багов к доказательствам теорем

От «мусора» к рабочим решениям

Два года назад использование LLM в серьезных математических и программных проектах часто приводило к катастрофическим результатам. Модели могли переопределять переменные в середине доказательства или выдавать код, требующий полного переписывания. Однако, по словам исследователя Джона Суэнтуорта (John Swentworth), за последние ~4 месяца ситуация кардинально изменилась. LLM-ы начали существенно ускорять работу, позволяя сосредоточиться на архитектуре решений, а не на рутинном написании кода.

Конкретные кейсы ускорения

Суэнтуорт приводит два ярких примера, где LLM сыграли ключевую роль в решении задач, за которые ранее были объявлены вознаграждения (bounty):

• Контрпример к гипотезе: Гриша Почуев использовал LLM для создания контрпримера к гипотезе о существовании детерминированного максимального избыточного латента. Это решение оценивается в $300 из $500 возможных.
• Доказательство теоремы: Дэвид (соавтор поста) разработал доказательство того, что существование стохастического натурального латента влечет за собой существование детерминированного. Весь код доказательства был написан с помощью LLM в системе Lean. Хотя само доказательство сложное, именно ИИ позволил обработать множество случаев.

Качественный скачок в программировании

Особое внимание уделено инструменту Claude Code. Суэнтуорт отмечает, что модель достигла уровня, когда он может полностью делегировать ей повседневные задачи по написанию кода для интерпретации данных (interp experiments). Ему больше не нужно писать код вручную — достаточно проверить графики и таблицы на наличие ошибок.

Хотя интерпретация результатов и предложения по следующим шагам от ИИ все еще часто бесполезны, способность генерировать рабочий код без глубоких багов стала «качественным скачком» (qualitative jump).

Сравнение: прошлое vs настоящее

Ранее эксперты, включая Рейя Кортена (Ray), предполагали, что проблема была в сложности задач, а не в моделях. Теперь же, несмотря на то, что LLM все еще не способны выполнять все ключевые части сложной работы, они ускоряют значимые фрагменты настолько, что это меняет сам подход к исследованию.

Этот сдвиг означает, что LLM перестали быть просто «поисковиком для StackOverflow» и стали полноценными соавторами в научных вычислениях.

Источник: LessWrong ↗