Проблема доверия в семантических сетях
Традиционные редакторы онтологий (например, Protégé) и текстовые диффы (git diff) скрывают логические последствия изменений. Изменение одной строки может незаметно повлиять на сотни триплетов, что критично для production-сред. Open Ontologies решает эту проблему, предоставляя не просто вывод, а доказательство (certificate), которое можно проверить независимо от исходного движка.
Техническая архитектура: Rust + Lean 4
Движок написан на Rust и поставляется как единый бинарный файл. Ключевая особенность — интеграция с верифицируемым доказательным помощником Lean 4. Это позволяет отделить «мнение» эвристического_reasoner_ от математически строгого доказательства. Система генерирует сертификат, который любой аудитор может проверить без доступа к сети или самому инструменту.
Ключевые метрики и бенчмарки
На примере фреймворка HQDM (Human and Qualitative Data Model) инструмент продемонстрировал высокую точность в выявлении ошибок:
| Метрика / Фреймворк | Результат / Детали |
|---|---|
| HQDM (RDFS) | 23 undeclared terms, 12 rdfs:range ошибок, 13 пар с опечатками. Не проходит проверку на непротиворечивость. |
| HQDM (OWL) | 190 классов удовлетворимы, 39 классов не удовлетворимы (coherence check failed). HermiT подтверждает 39 unsatisfiable. |
| Безопасное изменение | 1 триплет изменен → 0 затронутых триплетов (blast radius 0). Risk score: low. |
| Рискованное изменение | 1 триплет изменен → 901 новых следствий. Conservativity: not_conservative_under_rule_table. |
| Скорость проверки | Генерация 901 следствия через rule table owl-rl заняла 0.04s. |
Интеграция с AI-ассистентами (MCP)
Open Ontologies поддерживает протокол MCP (Model Context Protocol), что позволяет Claude Code, Cursor и другим AI-клиентам напрямую запрашивать анализ графа знаний. Это закрывает разрыв между генерацией кода/онтологии и её верификацией: AI может предложить изменение, а система — мгновенно вернуть «proof» или отказ с указанием нарушенного правила.
Сравнение подходов к верификации
| Критерий | Обычный Reasoner | Open Ontologies |
|---|---|---|
| Обоснование ответа | «Reasoner says so» (черный ящик) | Сертификат с указанием каждого правила и преамбулы |
| Кто может проверить | Только вторая реализация (возможна ошибка в обеих) | Любой человек с валидатором Lean 4 (независимый код) |
| Защита от подделки | Невозможно обнаружить редактирование вывода | Checker exit 1 + имя нарушенного правила |
Поддерживаемые форматы и правила
Инструмент поддерживает загрузку данных из CSV, JSON, XML, YAML, XLSX, Parquet, PostgreSQL и DuckDB. Логический слой работает с OWL, RDFS, SHACL, а также пользовательскими правилами SWRL, RIF Core и Horn tables. Для сложных логических задач предусмотрена трансляция в TPTP, CLIF, SMT-LIB и LADR.
Источник: Github ↗