用时间图约束验证大语言模型推理：一种结构化评估方法

爱丁堡大学MSci学位论文项目提出一种四层评估框架（预测、验证、评分、报告），将大语言模型的时间推理输出转换为时间图进行结构化验证，支持BEFORE/AFTER/SIMULTANEOUS/UNKNOWN四种时间关系标签。该方法既关注预测与标准答案的一致性，也能检测推理过程中的内在矛盾，为LLM时间推理能力评估提供新范式。

大语言模型在自然语言理解任务中表现出色，但时间推理可靠性存疑。时间推理涉及事件先后、持续、重叠关系，对文档摘要、问答等应用至关重要。现有评估方法仅关注最终答案正确性，忽视推理过程内在一致性。本项目提出将LLM时间推理输出转为时间图，通过时序逻辑约束进行结构化验证，解决这一问题。

项目核心为四层架构：

1. 预测层：解析模型输出为事件、关系及推理步骤，支持BEFORE/AFTER/SIMULTANEOUS/UNKNOWN四种关系标签，允许模型在不确定时弃权。
2. 验证层：无参考验证时间图内在有效性，检查传递闭包一致性、循环依赖、矛盾约束及时序逻辑公式满足性。
3. 评分层：双重策略比较预测与标准答案：直接边评分（比较直接时间边）、闭包级评分（比较传递闭包后的完整时序），AFTER归一化为BEFORE逆关系，SIMULTANEOUS压缩为单节点，UNKNOWN视为弃权。
4. 报告层：生成结构化输出确保可复现性，包括config.json（配置与版本）、predictions.jsonl（任务结果）、report.json（聚合指标）及可视化图表。

项目技术亮点包括：

• 时间图构建与LTL验证：轻量级时间图构建器将文本转为有向图，验证引擎结合类型化不变式库与基础LTL子集执行时序检查。
• 多数据集支持：兼容Canonical Synthetic（自建合成数据集）、TempEval-3、MAVEN-ERE、MATRES等标准时间推理数据集。
• Ollama集成：支持本地推理引擎批量评估多模型，通过JSON清单配置实验并生成对比报告。
• 浏览器可视化工具：verifier_explorer.html允许交互式检查预测结果，无需服务器。

项目遵循严格可复现标准：

1. 确定性执行：支持设置随机种子确保结果可重现。
2. 版本控制：记录代码版本与数据集版本。
3. 完整日志：可选记录原始模型输出便于调试。
4. 错误恢复：断点续传功能，单个任务失败不中断整体扫描。

该工作的意义与前景：

1. 细粒度诊断：定位推理链条中的具体失败点。
2. 内在质量评估：无需标准答案即可检测推理缺陷。
3. 可解释性：通过时间图可视化直观理解模型推理路径。
4. 基准测试：为时间推理模型开发提供标准化评估工具。四层框架还可推广至其他复杂推理NLP任务。

当前验证器为LTL模型检验器的实用子集，未来方向包括：

• 扩展支持更复杂的时序逻辑公式。
• 集成更多开源与商业大语言模型。
• 开发实时推理可视化界面。
• 探索将验证反馈用于模型微调。