Effectively translating between natural language (NL) and formal logics like Linear Temporal Logic (LTL) requires expertise that limits formal verification's reach in safety-critical development. Template-based approaches sacrifice expressiveness for reliability; neural methods achieve fluency but provide no correctness guarantees. We present NeuroNL2LTL, a neurosymbolic architecture unifying learned translation with formal verification. NeuroNL2LTL routes translation through an intermediate representation whose mapping to LTL is structure-preserving by construction. Generated specifications undergo satisfiability and non-triviality checking; a minimal-edit repair mechanism corrects near-miss outputs before they reach downstream tools. The central innovation is verifier-in-the-loop training: verification outcomes serve as reward signals for reinforcement learning, producing neural components that optimize directly for formal correctness. On 200,000+ requirements spanning aerospace, robotics, autonomous vehicles, and ten additional domains, NeuroNL2LTL achieves 28\% semantic equivalence with reference specifications while ensuring 86\% of outputs are verified satisfiable. The system also generates contextually grounded explanations from LTL, enabling domain experts to validate specifications without specialized training. This work demonstrates that formal verification can function as both training objective and runtime filter for neural specification systems, allowing us to build neural-based tools whose reliability derives from logical guarantees rather than statistical confidence.

翻译：在自然语言（NL）与形式逻辑（如线性时序逻辑LTL）之间进行有效翻译需要专业知识，这限制了形式验证在安全关键开发中的应用范围。基于模板的方法为可靠性牺牲了表达能力；神经方法实现了流畅性，但无法保证正确性。我们提出NeuroNL2LTL，一种将学习翻译过程与形式验证相统一的神经符号架构。NeuroNL2LTL通过一种中间表示进行翻译，该表示到LTL的映射天然具有结构保持特性。所生成的规约需经过可满足性与非平凡性检查；一种最小编辑修复机制在接近正确的输出传递至下游工具前对其进行纠正。核心创新在于验证器参与循环的训练过程：验证结果作为强化学习的奖励信号，促使神经组件直接针对形式正确性进行优化。在涵盖航空航天、机器人、自动驾驶车辆及其他十个领域总计20万条以上的需求集上，NeuroNL2LTL实现了28%的语义等价率（与参考规约相比），同时确保86%的输出经验证为可满足。该系统还能从LTL生成具有上下文依据的解释，使领域专家无需专业培训即可验证规约。这项工作表明形式验证既能作为神经规约系统的训练目标，也能作为其运行时过滤器，从而构建出可靠性源自逻辑保证而非统计置信度的神经工具。