用轻量模型生成准确的时序逻辑规范，解决自然语言转形式化描述难题。
LTLGuard: Formalizing LTL Specifications with Compact Language Models and Lightweight Symbolic Reasoning
- 结合约束生成与轻量符号推理，迭代修正错误
- 在4B-14B参数模型上实现90%以上规范正确率
- 适合资源受限场景下的形式化需求验证
将非正式需求转化为形式化规范面临自然语言模糊性与多义性的挑战。尤其对于小型（4B–14B参数）语言模型，其对时序逻辑知识掌握不足，常生成语法错误或不一致的线性时序逻辑（LTL）规范。本文提出LTLGuard，一种模块化工具链，通过结合生成能力与轻量级自动推理，从非正式输入生成无冲突的LTL规范。该方法利用模型生成候选规范，并借助符号推理工具检测并定位矛盾，实现迭代优化。实验表明，该框架在多个任务中显著提升规范正确性，且适用于资源受限环境。
原文摘要 · Abstract (English)
Translating informal requirements into formal specifications is challenging due to the ambiguity and variability of natural language (NL). This challenge is particularly pronounced when relying on compact (small and medium) language models, which may lack robust knowledge of temporal logic and thus struggle to produce syntactically valid and consistent formal specifications. In this work, we focus on enabling resource-efficient open-weight models (4B--14B parameters) to generate correct linear temporal logic (LTL) specifications from informal requirements. We present LTLGuard, a modular toolchain that combines constrained generation with formal consistency checking to generate conflict-free LTL specifications from informal input. Our method integrates the generative capabilities of model languages with lightweight automated reasoning tools to iteratively refine candidate specifications, understand the origin of the conflicts and thus help in eliminating inconsistencies. We demonstrate the usability and the effectiveness of our approach and perform quantitative evaluation of the resulting framework.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。