在安全关键系统的开发中，形式验证是确保系统可靠性的重要手段，但使用线性时序逻辑（LTL）等形式逻辑需要高度专业知识，这限制了形式验证的广泛应用。传统的基于模板的翻译方法虽然可靠，却牺牲了表达灵活性；而纯神经方法虽然能生成流畅的翻译，却无法保证正确性。为了解决这一矛盾，研究者提出了 NeuroNL2LTL，一种将学习翻译与形式验证统一的神经符号架构。
NeuroNL2LTL 的核心设计是让翻译过程经过一个中间表示，该表示到 LTL 的映射在构造上保持结构。生成的规格会经过可满足性和非平凡性检查，确保输出在逻辑上合理。对于接近正确的输出，系统还采用最小编辑修复机制，在交付下游工具前自动纠正细微错误。这种设计使得系统既能利用神经模型的灵活性，又能通过符号验证提供硬性保证。
该论文最重要的创新是“验证器在环训练”。传统神经翻译模型仅通过监督学习优化与参考译文的相似度，而 NeuroNL2LTL 将验证结果作为强化学习的奖励信号，让神经组件直接以形式正确性为目标进行优化。这意味着模型在训练过程中就能学会生成逻辑上可验证的规格，而不仅仅是表面流畅的文本。
为了评估系统性能，作者构建了包含超过 20 万条需求的测试集，覆盖航空航天、机器人、自动驾驶等十二个领域。实验结果显示，NeuroNL2LTL 在语义等价性上达到 28%，同时确保 86% 的输出通过可满足性验证。虽然 28% 的语义等价率看似不高，但考虑到 LTL 翻译的复杂性和严格性，这一结果展示了神经符号方法的潜力。更重要的是，系统能保证大部分输出在逻辑上可满足，这为下游验证工具提供了可靠输入。
除了翻译，NeuroNL2LTL 还能从 LTL 生成上下文相关的解释，帮助领域专家在没有专业逻辑训练的情况下理解和验证规格。这降低了形式验证的使用门槛，使更多工程师能够受益于形式化方法。
总之，这项研究展示了形式验证可以作为神经规格系统的训练目标和运行时过滤器，从而构建出可靠性源于逻辑保证而非统计置信度的神经工具。这为安全关键领域中的自然语言接口开辟了新途径，有望推动形式验证在工业界的更广泛应用。