Проблема фрагментации в STKG
Инженерия графов знаний часто сталкивается с проблемой распределения состояния, наблюдений, ограничений и процессов по разным артефактам. Итоговый контракт их выполнения остается внешним, что создает риски несогласованности. Авторы Dongxu Yang и Ziyi Liang предлагают решение — язык PULSE, вдохновленный Object-Process-Methodology (OPM), который локализует четыре операционные роли и их эффекты записи в одном типизированном рантайме.
Механика и безопасность
Ключевая особенность PULSE — фиксация контракта на уровне ядра. Язык гарантирует:
- Неизменяемость доказательств (evidence non-overwrite): данные нельзя перезаписать, только дополнить.
- Изоляцию ветвей: параллельные процессы не конфликтуют.
- Привязку таймеров: многопользовательские таймеры привязаны к пространству и времени.
- Защищенное изменение состояния: переходы возможны только при соблюдении guard-условий.
Стандарты GeoSPARQL, SOSA и SHACL генерируются как представления (views), а не как ядро системы.
Верификация через Lean 4
Для доказательства корректности ядро PULSE проверено в доказательной системе Lean 4. Это позволило формально доказать лемму об изоляции эффектов и шесть свойств безопасности. Тестирование включало 88 тестов, 3 534 проверенных ограничения и 32 случая рантайм-ядра (Lean/Python).
Результаты бенчмарков
Эффективность PULSE оценена на реальных сценариях, включая отслеживание температурного режима (cold-chain trace) и анализ данных NOAA IBTrACS (ураганы с 1980 года). Язык продемонстрировал паритет трасс с существующими рабочими процессами и способность выявлять мутации.
| Метрика / Сценарий | Результат / Объем | Значение |
|---|---|---|
| Генерация временных трасс | 37 440 трасс | Паритет с внешним workflow, выявление 10 мутаций |
| Анализ NOAA IBTrACS | 1 476 290 пар переходных зон | Согласие с GEOS и event sweep |
| Выборка событий | 4 800 событий | Включая 12 831 событий с квалификацией по длительности |
| Формальная верификация | 3 534 bounded checks | Доказательство 6 свойств безопасности в Lean 4 |
Значение для индустрии
Работа PULSE закрывает критический пробел в инженерии знаний, переводя контракты из внешней документации в исполняемый код. Это особенно важно для критических инфраструктур, где пространственно-временные данные (логистика, климат, IoT) требуют абсолютной согласованности и аудита. Исходный код доступен под лицензией Apache-2.0.
Источник: arXiv cs.AI ↗