В сфере формальной верификации и теоретического машинного обучения произошло событие, демонстрирующее новый уровень симбиоза человека и ИИ. Исследователь Дэвид Лорелл (David Lorell) опубликовал результат, в котором с помощью автоматизированного доказательства в системе Lean4 подтвердил теорему: (∃ Stochastic Natural Latent) Implies (∃ Deterministic Natural Latent). Это означает, что если в системе существует стохастическое латентное переменное (с некоторой степенью аппроксимации), то обязательно существует и детерминированное латентное переменное, чья ошибка ограничена константой, умноженной на ошибку стохастического.
Суть прорыва и роль LLM
Изначально эта теорема была опровергнута из-за ошибки в промежуточном шаге доказательства, найденной исследователями Джереми Гилленом и Альфредом Харвудом. Вместо того чтобы искать «гениальное исправление» вручную, Лорелл потратил месяц на эксперименты с интеграцией современных LLM в процесс формализации и доказательства на языке Lean4. Этот подход, схожий с методологией проекта Resolution, позволил получить машино-сертифицированное доказательство, которое компилируется и является корректным.
Ключевое отличие нового результата от предыдущих попыток — в силе утверждения. Теперь доказано, что существует единая детерминированная латентная переменная, работающая для всех возможных кандидатов стохастических латентных переменных, а не для каждого по отдельности. Это достигается за счет того, что минимизатор функции потерь D достигается при конечных наблюдаемых величинах.
Магическая константа 1771
Самым интригующим числовым результатом стало определение верхней границы ошибки. Теорема гласит, что сумма ошибок детерминированного латентного переменного ограничена константой C, умноженной на сумму ошибок стохастического латентного. В ходе формализации с помощью «машинной магии» (через ядро Lean) было строго доказано, что:
C = 1771
Хотя это число значительно хуже первоначальной гипотезы авторов (где ожидалась константа 9), оно является строгим математическим фактом. Однако эмпирические тесты показывают, что реальная граница ошибки гораздо ближе к единице. В процессе разработки постоянно всплывало число ~1.838, что указывает на огромный разрыв между теоретической верхней оценкой и практической производительностью модели.
Сравнение результатов
| Параметр | Исходная гипотеза (2025) | Новое доказательство (2026) | Эмпирические данные |
|---|---|---|---|
| Теоретическая константа C | 9 | 1771 | ~1.838 |
| Метод получения | Человеческое доказательство (ошибочное) | Lean4 + LLM (автоматизированное) | Наблюдения в тестах |
| Универсальность | Для каждого стохастического латентного | Единое для всех стохастических латентных | Применимо |
Почему это важно для AI-индустрии
Этот кейс становится эталонным примером того, как LLM трансформируют фундаментальные исследования. Доказательство, которое могло бы занять у человека месяцы или годы мучительных вычислений, было получено за месяц итеративного взаимодействия с ИИ-ассистентами. Следующие шаги исследователя — снижение константы C до более реалистичных значений (2–5) и поиск конструктивного доказательства. Успех этого подхода открывает путь к автоматизации сложных математических открытий, где ИИ берет на себя рутинную формализацию, а человек — стратегическое направление.
Источник: LessWrong ↗