Что не так с нейро-символьным обучением на описательных логиках
Онтологии OWL 2 DL, основанные на описательной логике SROIQ, давно стали рабочим инструментом в биомедицине и на Semantic Web — они позволяют компактно описать большие базы знаний. Но когда речь заходит об обучении нейросетей с использованием таких онтологий, начинаются проблемы. Классические подходы либо «размывают» логику, встраивая онтологию в непрерывные векторные пространства, из-за чего теряется строгое логическое следование, либо ограничиваются хорновским фрагментом EL++, у которого есть лишь одна каноническая модель. Из-за этого выразительные онтологии часто оказываются недоступны для гибридных систем.
Компиляция онтологии в дифференцируемую схему
Система Baobab предлагает не идти на компромисс: она компилирует полную онтологию SROIQ с конечной ABox в Sentential Decision Diagram (SDD). Процесс идёт в два этапа: сначала пропозициональное ядро насыщается с помощью исчисления следствий (consequence-based calculus), затем специфические для SROIQ конструкции — номиналы, ограничения на число ролей и аксиомы ролей — инстанцируются на активной области. На выходе получается схема, по которой можно выполнять взвешенный подсчёт моделей (weighted model count, WMC). Именно WMC становится связующим звеном между нейронной сетью и логическими ограничениями.
Обучение нейросети с сохранением логики
Взвешенный подсчёт моделей SDD с учётом свидетельств позволяет обучать сеть восприятия — например, свёрточную нейросеть — распознавать изображения даже тогда, когда только часть данных размечена в ABox. В эксперименте авторы построили онтологию, задействующую все отличительные особенности SROIQ, и обучили CNN распознавать цифры MNIST, связанные отношением следования. Сеть не просто классифицировала изображения — она восстановила латентные онтологические концепты. При независимом обучении восприятия такие концепты остаются на уровне случайности, а здесь они были выучены благодаря логическим ограничениям.
Reasoning shortcuts и калиброванный апостериор
Когда супервизорный сигнал допускает несколько вариантов завершения, одинаково согласованных с онтологией, независимо обученная сеть часто «схлопывается» к одному из них. Авторы называют это явление reasoning shortcut. В статье показано, что смесь, индексированная обоснованиями (justifications) запроса, способна представить калиброванный апостериор — то, что недостижимо для одиночной модели. Более того, если инициализировать такую смесь из перечисленных завершений схемы, можно получить байесовски-оптимальный апостериор на задаче MNIST с реальными изображениями. Для сравнения: одиночный WMC и обученные смеси-ансамбли такой результат не дают.
Проверка корректности и доступность
Авторы отмечают, что это первая работа, в которой reasoning shortcuts охарактеризованы и смягчены для не-хорновской описательной логики. Корректность компилятора и результат о представимости проверены машинно в Lean 4 — это серьёзный аргумент в пользу надёжности подхода. Код системы открыт, так что результаты можно воспроизвести и развить.
Вывод
Baobab показывает, что ради обучаемости не обязательно жертвовать выразительностью описательной логики. Компиляция SROIQ в дифференцируемую схему сохраняет логические следствия и одновременно даёт возможность обучать нейросети на реальных данных. А решение проблемы reasoning shortcuts через смеси, индексированные обоснованиями, — важный шаг к более надёжным и калиброванным гибридным моделям.
