nl2spec++

一句话描述 A 与 B，另一句话描述 B 与 C，但都没有直接说明 A 与 C。逐句翻译可以保留显式信息，却不一定回答我们真正关心的关系。

nl2spec++ 在开源 nl2spec 的基础上加入跨句关系推理。输入是两句相关的自然语言，以及分别来自两句中的两个目标实体。共享实体连接这两句话，输出则是用线性时序逻辑（LTL）表达的候选关系。

方法一：先推理，再翻译

先由语言模型用自然语言描述两个目标实体之间的关系，再通过翻译模块转成 LTL。中间保留自然语言表达，便于检查模型究竟推断了什么。

方法二：先翻译，再进行公式推理

先分别翻译两个输入句子，再将两条公式和目标实体交给语言模型，得到候选 LTL 关系。这里的形式化中间表示更明确，但推理仍由 LLM 完成，并非定理证明器的推导。

两条路径由用户选择，不是前后串联的两个阶段。

仓库的公式推理提示词包含下面这个例子，其中 G 表示“始终”，F 表示“最终”：

G(A → F B)
G(B → F C)
────────────
G(A → F C)

A 出现后最终会出现 B，而 B 出现后最终会出现 C，因此 A 出现后最终会出现 C。这表达的是时序依赖，不是因果关系。它用于解释方法，来自提示词示例，不是一次基准实验的结果。

命令行入口通过 src/backend.py 选择流程。方法一先调用语义推理，再调用翻译模块；方法二先翻译两个句子，再调用公式推理。语义提取、公式推理与翻译被拆成独立模块，便于观察中间结果。

翻译路径对模型输出进行多次采样，尝试用 LTLf 解析器解析公式，再按出现频率选择结果并计算 certainty score。这个分数反映采样输出的一致程度，不是经过校准的正确率。解析失败的结果仍可能以原始字符串保留，而方法二最终生成的公式也没有经过同等的端到端证明检查。

看起来形式化的输出仍可能是错的。语法正确不代表公式可以从输入推出，多次生成相同答案也可能只是重复同一个错误。此外，提示词使用 LTL 术语，解析模块使用 LTLf 库；真正验证前，需要明确有限轨迹与无限轨迹的语义。

部分提示词示例也需要审查：事件的先后顺序不能单独证明因果关系。不能把模型补出的解释直接当成有效推论。

仓库将应用场景、更多句子的关系推理与专门 benchmark 列为后续工作，目前没有对比实验可以证明哪条路径更准确。本文解释已有代码设计，不声称重新运行了其中较早的模型接口。

这个方向连接了灵活的语言理解与明确、可检查的约束。LLM 可以提出候选关系，形式化工具则可以检查它是否成立。下一步可以加入蕴含检查，寻找违反候选公式的反例，并通过基准分别分析翻译错误与推理错误。

生成规约是验证的起点，而不是验证的完成。