Harmonic привлекла $120 млн на создание математического суперразума Aristotle

[NeriaLab]

Мир постепенно начинает понимать, что "чистые" LLM ненадежны и неэффективны - будущее за гибридами. В данной новости, хоть расплывчато, но указано, что все перспективные системы, по своей сути, являются специализированными нейро-символьными архитектурами с акцентом на верификацию через формальные методы.

[Hivemaster]

Мир надул пузырь ещё на 120 мегабаксов.

[vlad4kr7]

Так как ИИ вообще не может в логику, то чем быстрее пузырек лопнет на формальных критериях, тем быстрее лопнет весь ИИ.

[NeriaLab]

Кто "не может в логику"? Утверждение, что системы вообще "не могут в логику" - это применимо только к определенному подходу, а именно к "чистым" нейросетям/LLM, но не ко всему полю исследований искусственного интеллекта.

Когнитивно-символьные системы как раз и "заточены" под формальную логику. Первые программы, которые вообще считаются началом интеллектуальных систем, были чисто символьными и логическими. Давайте посмотрим на исторические факты:

1. "Логик-теоретик" (Logic Theorist, 1956) от Аллена Ньюэлла и Герберта Саймона была разработана специально для автоматизированного доказательства математических теорем;

2. "Универсальный решатель задач" (General Problem Solver, 1957) развивал идеи "LT", используя эвристики и метод "средства-цели" для решения логических задач. Система хорошо работала с формальными логическими задачами.

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

Так что когнитивные системы "могут в логику", просто сейчас, в центре внимания, находится другая архитектура - LLM, у которых с этим действительно есть проблемы. Будущее за гибридными нейро-символьными архитектурами и CESP (совсем без LLM и с логическим ядром) системами.

[vlad4kr7]

Вы много так написали, а статью читали?

Языковая часть помогает искать идеи и шаги решения, но каждое решение должно быть записано в виде строгого доказательства на языке Lean4 и пройти проверку ядром этой системы. Если формальный проверяющий не принимает доказательство, ответ не считается найденным.

Где здесь использование чего-то другого кроме ЛЛМ или использование логики в поиске решения, а не проверке чего-то найденного?

[Pshir]

Так ведь решение именно так и ищется: генерятся идеи, а потом проверяются. Поиск решения формальной логикой эффективен только для уже решённых заранее задач. Например так делается в учебниках, где сначала пишут решение задачи, а потом просят повторить это же решение этой же задачи ещё сотню раз.

[NeriaLab]

Вот только в когнитивно-символьных системах, "сотня раз" превращаются в десятки, а то и в единицы

[Pshir]

Мир постепенно начинает понимать, что "чистые" LLM ненадежны и неэффективны - будущее за гибридами.

Я так думаю, что те, кто занимаются вопросами ИИ, понимали это всегда. Просто у инвесторов начали кончаться деньги на поддержку попыток решить все проблемы брутфорсом, то есть тупым закидыванием в топку грузовиков с видеокарточками и петабайтов мусорных текстов. И чтобы двигаться дальше, придётся опять применять старые добрые мозги.

[chuzhiegrably]

«Старые добрые мозги» тут несильно помогут: новая типа умная модель-оценщик ошибки поверх типа тупой дефолтной сетки может снизить ошибку, но принципиально не влияет на качество.

Грубо говоря, такой фильтр ответа от модели, когда его (ответ) запускают на второй круг, например, для фактографической проверки, но подобное уже доступно в новых моделях и — сюрприз! — тоже не гарантирует 100% защиты от галлюцинаций.

[Pshir]

Проверка одного генератора случайных чисел вторым генератором случайных чисел, конечно, не гарантирует от галлюцинаций. Тут же описывается другой принцип.