ARI AML

47 views15:44

Модель может быть полезным собеседником — быстрым, начитанным, терпеливым, но не судьёй

Формальная система — тоже не судья: она не знает, хорошо ли поставлена задача, верно ли описание реального объекта, интересно ли получившееся утверждение, но она честно проверяет, что из заданных предпосылок действительно следует заявленный вывод

В этом контуре появляется новая компетенция: не «уметь спросить модель», а построить логический путь

Между этими режимами очень большая разница

На задачах Lean-IMO-Bench обычные большие языковые модели в одношаговом режиме решали мало задач

Агентный подход LEAP, разбивает работу на шаги и используя проверку компилятором Lean как обратную связь, довёл результат до 70 %

Модель не научилась мыслить как математик, но строгая среда проверки радикально меняет качество работы модели
Ошибка перестаёт быть финалом ответа — она становится продолжением решения, строит надёжные артефакты: доказательства, спецификации, фрагменты кода, модели

И это касается не одной чистой математики

В августе была представлена EconCSLib — библиотека и рабочий процесс для формализации исследований в экономике и вычислениях

Схема предельно инженерная: модель переводит определения и утверждения статьи в Lean, Lean проверяет код, а человек и дополнительные процедуры контроля проверяют, не исказился ли смысл исходного текста

В открытом репозитории проекта к июлю было почти миллион строк Lean-кода и 24 формализации работ — 20 полных и 4 частичных

Вот где проходит реальная граница будущей грамотности

Не между «гуманитариями» и «технарями»
И даже не между теми, кто пишет код, и теми, кто его не пишет

А между теми, кто принимает правдоподобный ответ на веру, и теми, кто умеет спросить: какие здесь предпосылки, что именно проверено, где границы модели и каким механизмом мы ловим ошибку?

Алгоритмы не отменяют необходимость думать
Они делают цену недуманья заметно выше

Впереди разговор о том, почему автоматическое доказательство меняет не только математику, но и темп инженерной работы

А в какой задаче вы уже сегодня готовы доверить алгоритмам черновую работу, но ни за что не доверите ему финальную проверку?

41 viewsedited 07:51

ARI AML

Autonomous_Agent_Architecture_Unifying_Context_Engineering_and_Memory….pdf

69 KB

42 views18:03

ARI AML

0:21

This media is not supported in your browser

VIEW IN TELEGRAM

42 views18:32

ARI AML

Даже если самые передовые модели завершены, они не публикуются сразу, а используются внутри для разработки моделей следующего поколения

Это «пересечением горизонта событий»
Это не то, что каузуэйлловская сингулярность в смысле технологической сингулярности, но в смысле того, что из петли самоускорения уже трудно вернуться, это может быть вполне справедливо

На Fellows Forum в конце сентября, руководитель прикладных исследований OpenAI, заявил, что сейчас 90 % исследований компании направлены на обучение GPT-7 и GPT-8 — там наибольшая ценность

И постепенные обновления внутри одного поколения, такие как 5.1 или 5.2, считаются краткосрочной ставкой и крайне недальновидными
То есть исследователи работают на два поколения вперед по сравнению с тем, что используется сейчас

Самые передовые модели уже разработаны, но не публикуются и удерживаются

Скоро такие модели следующего поколения перестанут быть общедоступными и начнут использоваться только для специфических целей внутри исследовательских институтов

Самое большое вознаграждение за токен в текущих фронтир-моделях, по крайней мере то, что генерирует наибольшую дисконтированную текущую стоимость в будущем, — это разработка еще более мощных моделей через рекурсивное самоулучшение

По этому пункту «горизонт событий» уже пересечён, именно поэтому это и называют сингулярностью

48 views18:40

ARI AML