Translating Natural Language to Strategic Temporal Specifications via LLMs

1. 构建了包含1100条专家标注实例、涵盖5类语言歧义（右/左移位、VP省略、右节点抬升、量词作用域）的首个NL-to-ATL/ATL*基准数据集，专家间标注一致性κ=0.99，为战略规范合成任务奠定可重用基础。思考链：工业形式验证缺乏系统化的自然语言→逻辑表达转换资源，本数据集通过双专家共同编写、三方标注验证、多读数平衡设计，解决了这一资源空白。
2. 通过混合推理架构和LoRA微调，证明参数量3-7B的开权重模型在最人类对齐的评判标准下达到0.844的语义准确率，与GPT-5.4的0.856基本持平（配对引导程序p=0.71），同时支持隐私保护的本地部署。思考链：与其接受商业API的数据泄露风险，不如通过任务内微调使小模型达到同等性能，此举同时降低了形式验证对非专家用户的专业门槛。
3. 发现了评判模型质量与生成能力呈反向关系的现象——开权重Llama-3.3-70B与人类标注的一致性最高（κ=0.59），而最先进的GPT-5.4/5.2一致性最低（κ=0.24/0.16），系统性地过度拒绝了忠实的输入接地释义，即使对自身生成的输出亦然。思考链：此发现对自动评估的可信度提出深刻质疑，强暗示依赖闭源模型作为评判标准的论文需要格外谨慎。

数据集规模：1100条自然语言-ATL/ATL*公式对，其中7条保留用于少样本提示，余下1093条按70/10/20比例分为765条训练、110条验证、218条测试样本。语言现象：5类目标歧义各占约20%，时序算子X/G/F/U分别出现590/590/598/586次，接近均衡。模型评估：6个独立LLM评判者（DeepSeek-V3.2、GPT-4.1、GPT-5.2、GPT-5.4、Gemma-2-27B、Llama-3.3-70B），4279条预测结果，598条预测经人类专家双标注验证（初始不一致3条，讨论后达成共识598条）。微调配置：4个开权重模型（Mistral-7B、Qwen-3B、Qwen-Coder-7B、Phi-3.5）采用LoRA微调（秩32-64、α64-128、QLoRA 4bit量化）、8个epoch、AdamW优化器、余弦衰减，在NVIDIA A100 GPU上训练；专有基线（GPT-4.1、GPT-5.4）采用零样本和少样本提示，不微调。评估协议：两层计分（精确字符串匹配+LLM判别），多种子实验（3个训练种子），显著性检验（配对引导置信区间、随机排列测试）。