Formal, Executable and Explainable Runtime Monitoring of Spoken Air Traffic Control Operational Procedures
Работа соединяет распознавание диспетчерской речи с исполняемыми правилами ICAO: система превращает переговоры и телеметрию ADS-B в временную трассу, а затем выдает трехзначный вердикт с доказательством. Ценность подхода в том, что языковая модель только разбирает реплику на факты, тогда как решение о нарушении принимает формальная темпоральная логика.
Метод. После распознавания речи языковая модель извлекает позывные, команды и параметры в заданную схему. Эти события объединяются с наблюдениями борта и земли, а обязательства ICAO записываются в метрической темпоральной логике. Монитор возвращает «выполнено», «нарушено» или «пока неизвестно» и связывает вывод с конкретными событиями. Проверка включает час расшифровок ATCO2, три часа движения KAGC с 12 размеченными нарушениями, 1495 синтетических ситуаций и две реконструкции происшествий.
Результаты. Все 1495 синтетических трасс дают ожидаемый логический вердикт. В полной цепочке Qwen3.8-27B без режима рассуждения достигает precision 0,79, recall 0,92 и F1 0,85; включение рассуждения снижает F1 до 0,67 прежде всего из-за падения полноты до 0,58. Распознавание работает с медианной скоростью 45,1x реального времени, малый разбор занимает 0,296 с, большой — 1,58 с, а проверка формулы — 0,119 с на событие. В статье для используемой модели распознавания указана WER 15,08% на диспетчерской речи.
Ограничения. В реальных трех часах всего 12 нарушений, пять из восьми семейств правил покрыты синтетикой, а происшествия реконструированы. Не оценены нагрузка на диспетчера, цена ложных предупреждений и работа при тяжелых ошибках распознавания. Формальная часть воспроизводима, но надежность всей системы ограничена извлечением фактов до нее.
Фишка из статьи. Режим пошагового рассуждения оказывается не страховкой, а помехой: для сильнейшей модели он одновременно замедляет разбор и пропускает больше событий. Структурная схема плюс короткий прямой ответ лучше длинной цепочки рассуждений.
| Разборщик | Precision | Recall | F1 |
|---|---|---|---|
| Qwen3.8-27B, без рассуждения | 0,79 | 0,92 | 0,85 |
| Qwen3.8-27B, с рассуждением | 0,78 | 0,58 | 0,67 |
| Gemma 4 26B, без рассуждения | 0,40 | 0,33 | 0,36 |
| Gemma 4 26B, с рассуждением | 0,67 | 0,33 | 0,44 |
| Qwen2.5-7B | 0,57 | 0,67 | 0,62 |
Как это читать: у Qwen режим рассуждения почти не меняет точность положительных срабатываний, но теряет треть истинных событий. Его медианное время разбора возрастает примерно до 3,9 с; для другого рассуждающего варианта в опытах оно доходит до 38 с, тогда как сама формальная проверка занимает доли секунды.