NeuroNL2LTL：面向自然语言到线性时序逻辑转换的神经符号框架
人工智能
2026-05-25 v1 计算机科学中的逻辑
摘要
在自然语言（NL）与线性时序逻辑（LTL）之间进行有效转换需要专业知识，这限制了形式化验证在安全关键领域的应用范围。模板化方法以可靠性为代价牺牲表达力；神经方法实现流畅性却无法提供正确性保证。我们提出 NeuroNL2LTL，一种神经符号架构，统一学习转换与形式化验证。NeuroNL2LTL 将转换路由通过中间表示，其映射到 LTL 由构造方式保证结构保持。生成的规范经过满意性和非平凡性检查；最小编辑修复机制在输出触及下游工具前对接近缺失的结果进行纠正。核心创新在于验证器-in-the-loop 训练：验证结果作为强化学习的奖励信号，产生优化直接针对形式正确性的神经组件。在 20 万+条覆盖航空航天、机器人、自动驾驶等十个领域的需求数据集上，NeuroNL2LTL 实现 28% 的语义等价性，同时确保 86% 的输出通过验证满足。该系统还能从 LTL 生成情境化的解释，使领域专家无需专业训练即可验证规范。本工作表明，形式化验证既可作为训练目标亦可作为神经规范系统的运行时过滤器，使我们能够构建基于神经的工具，其可靠性源于逻辑保证而非统计置信度。
引用
@article{arxiv.2605.22874,
title = {NeuroNL2LTL: A Neurosymbolic Framework for Natural Language Translation of Linear Temporal Logic},
author = {Paapa Kwesi Quansah and Ernest Bonnah},
journal= {arXiv preprint arXiv:2605.22874},
year = {2026}
}