>>4234Теренс Тао, лауреат премии Филдса:
Я немного поэкспериментировал с новой итерацией GPT от OpenAI, GPT-o1, которая выполняет начальный этап рассуждения перед запуском языковой модели. Это, безусловно, более мощный инструмент, чем предыдущие версии, хотя все еще испытывает трудности с наиболее сложными математическими задачами исследовательского уровня.
Вот несколько конкретных экспериментов (с прототипной версией модели, к которой мне предоставили доступ). В
https://chatgpt.com/share/2ecd7b73-3607-46b3-b855-b29003333b87 я повторил эксперимент из
https://mathstodon.xyz/@tao/109948249160170335, в котором я попросил GPT ответить на расплывчато сформулированный математический вопрос, который можно было решить, определив подходящую теорему (теорему Крамера) из литературы. Ранее GPT мог упомянуть некоторые релевантные концепции, но детали были галлюцинированной бессмыслицей. На этот раз теорема Крамера была идентифицирована, и был дан вполне удовлетворительный ответ. (1/3)
В
https://chatgpt.com/share/94152e76-7511-4943-9d99-1118267f4b2b я дал новой модели сложную задачу по комплексному анализу (для которой я ранее просил GPT4 помочь написать доказательство в
https://chatgpt.com/share/63c5774a-d58a-47c2-9149-362b05e268b4). Здесь результаты были лучше, чем у предыдущих моделей, но все же немного разочаровывающими: новая модель могла прийти к правильному (и хорошо написанному) решению, *если* предоставить много подсказок и наводящих вопросов, но самостоятельно не генерировала ключевые концептуальные идеи и делала некоторые нетривиальные ошибки. Опыт был примерно сопоставим с попыткой консультировать посредственного, но не полностью некомпетентного аспиранта. Однако это было улучшением по сравнению с предыдущими моделями, чьи возможности были ближе к действительно некомпетентному аспиранту. Возможно, потребуется всего одна или две дальнейшие итерации улучшенных возможностей (и интеграция с другими инструментами, такими как пакеты компьютерной алгебры и ассистенты доказательств), прежде чем будет достигнут уровень "компетентного аспиранта", и тогда этот инструмент может стать значительно полезным для задач исследовательского уровня. (2/3)
В качестве третьего эксперимента я попросил (в
https://chatgpt.com/share/bb0b1cfa-63f6-44bb-805e-8c224f8b9205) новую модель начать задачу формализации результата в Lean (а именно, установить одну форму теоремы о простых числах как следствие другой), разбив ее на подлеммы, для которых она бы формализовала утверждение, но не доказательство. Здесь результаты были многообещающими в том смысле, что модель хорошо поняла задачу и выполнила разумное начальное разбиение проблемы, но была ограничена отсутствием актуальной информации о Lean и его математической библиотеке в своем обучении, и ее код содержал несколько ошибок. Однако я могу представить, что модель с такими возможностями, специально настроенная на Lean и Mathlib и интегрированная в IDE, может быть чрезвычайно полезной в проектах по формализации. (3/3)
Кальсон, многократный лауреат премии Ленина за достижения в художественной копролалии:
> Девять из десяти стоматологов выбирают "Блендамед". "Блендамед" - и ваши много раз перепачканные кальсоны снова светятся белизной!