NeuroNL2LTL：线性时序逻辑自然语言翻译的神经符号框架

arXiv:2605.22874v1 公告类型：新 摘要：在自然语言 (NL) 和线性时序逻辑 (LTL) 等形式逻辑之间进行有效转换需要专业知识，而这限制了形式验证在安全关键型开发中的影响范围。基于模板的方法牺牲了表现力以换取可靠性；神经方法可以达到流畅性，但不能保证正确性。我们提出了 NeuroNL2LTL，一种将学习翻译与形式验证相结合的神经符号架构。 NeuroNL2LTL 通过中间表示路由翻译，中间表示到 LTL 的映射是通过构造保留结构的。生成的规范经过可满足性和非平凡性检查；最小编辑修复机制可以在未命中的输出到达下游工具之前对其进行纠正。核心创新是验证者在环训练：验证结果作为强化学习的奖励信号，产生直接优化形式正确性的神经组件。针对涵盖航空航天、机器人、自动驾驶汽车和 10 个其他领域的 200,000 多个要求，NeuroNL2LTL 与参考规范实现了 28% 的语义等效性，同时确保 86% 的输出经过验证可满足。该系统还根据 LTL 生成基于上下文的解释，使领域专家无需专门培训即可验证规范。这项工作表明，形式验证可以充当神经规范系统的训练目标和运行时过滤器，使我们能够构建基于神经的工具，其可靠性源自逻辑保证而不是统计置信度。