Проект Ankyra представляет подход к нейро-символическим рассуждениям, объединяющий языковые модели с детерминированными символьными решателями. Метод направлен на снижение галлюцинаций моделей: символьный решатель проверяет факты и выводит заключения, выступая в роли логического каркаса для вероятностных ответов нейросети.
Алгоритм работает циклично, совершая «волны» рассуждений. На каждом этапе модель извлекает из текста факты и правила для формирования теории, а решатель пытается вывести ответ. Если решение не найдено, модель дополняет теорию новыми данными. Тестирование показало, что для большинства задач требуется не более семи таких циклов.
Система автоматически подбирает тип логики в зависимости от структуры извлеченной теории. Поддерживаются логика первого порядка с хорновскими правилами, логика с кванторами и отрицанием, а также арифметика и системы линейных уравнений для решения прикладных задач.
Автор протестировал алгоритм на модели DeepSeek V4 Flash, используя бенчмарки AI2, ProntoQA, FOLIO и логические игры уровня LSAT. Результаты сравнивались с реализациями Logic-LM и LINC. На срезе L2 система показала результат 29–31 из 45 в режиме работы с моделью, при этом на срезе с отрицанием результат составил 11 из 13.
