Сейчас появляется много сообщений о решении тех или иных проблем в математике, доказательстве известных теорем, обобщении существующих результатов на более широкую область и т.п. Результаты действительно впечатляют. С другой стороны, каждый из нас сталкивался в той или иной степени с галлюцинациями языковых моделей, когда модель придумывает несуществующие факты, а легковерные пользователи принимают их за чистую монету.Причина такого поведения моделей состоит в вероятностной природе ее алгоритма рассуждений. Токены (слова) в модели представляют векторами вещественных чисел (динамическими эмбеддингами), а механизм self-attention реализован так, что очень хорошо ловит рассуждения на основе аналогий (ассоциаций), но легко может ошибиться, когда таких аналогий не существует. В этом случае, модель начинает строить ложные аналогии и фантазировать.Исследователи давно осознали этот факт и в направлении способности моделей к улучшению точности рассуждений ведется большая работа. В данной статье я хочу рассказать о работе в направлении т.н. нейро-символических рассуждений, когда рассуждения модели ведутся не в одиночестве, а в тандеме с т.н. символьным решателем - реализованным на основе детерминированного алгоритма. Этот решатель использует хорошо разработанный за последние несколько десятков лет аппарат формальной логики. Читать далее