在形式化需求规格生成与验证的实际项目中最容易被低估的问题往往不是“模型看不懂逻辑公式”而是“模型把同一套公式默认成了同一套语义”。比如 □(p → q) 这个公式在时序逻辑里可以表示“p 之后 q 永远成立”在道义逻辑里表示“义务上 p 蕴含 q”在认知逻辑里又可能被理解为“智能体知道 p 蕴含 q”。公式的语法一模一样语义解释却天差地别。这也正是标题所反映的核心问题Same Formulas, Different Semantics: Do Language Models Follow Modal Logic Specifications?——大语言模型在多大程度上会遵守我们给定的模态逻辑语义规范这篇文章会把这个问题拆成一个可以动手复现的评测工程。我们会先讲清楚模态逻辑的语法与语义分层再设计一套“同一公式、不同语义、不同模型”的评测思路最后给出完整的 Python 代码包含公式构造、Kripke 模型验证器、LLM 评测脚本和 ReAct 风格推理增强。无论你是做 NLP 评测、形式化验证还是想用 LLM 自动生成安全策略都能直接复用这套方法。1. 背景与核心概念1.1 模态逻辑到底是什么模态逻辑Modal Logic是在经典命题逻辑的基础上引入“必然”□和“可能”◇两个模态算子的逻辑系统。它要回答的问题不是“命题是否为真”而是“命题在什么条件下必然为真在什么条件下可能为真”。举个直观的例子。经典逻辑里语句“北京是中国的首都”是真命题它不依赖任何视角或场景。但语句“明天会下雨”就不能用经典逻辑直接判定真假因为它的真值取决于“未来状态”这个语义背景。模态逻辑通过引入可能世界possible world和可达关系accessibility relation把这类依赖语境的真假判断形式化。在形式化验证领域模态逻辑的变体应用非常广泛线性时序逻辑LTL用来描述系统运行轨迹上的属性计算树逻辑CTL用来描述分支时间上的属性动态逻辑和描述逻辑则用于程序验证与知识表示。可以说模态逻辑是连接自然语言需求与机器可验证规范之间的桥梁。1.2 为什么大模型需要理解模态逻辑规范大语言模型近年来被越来越多地用于生成形式化规范从自然语言需求自动生成 LTL 断言从代码注释提取前置条件甚至把安全策略转换成约束规则。这背后的假设是模型不仅懂得自然语言还懂得形式逻辑背后的语义。但这里有一个工程上非常现实的问题形式逻辑的“规范”不是一个写在纸面上的字符串而是一套语义解释规则。同一个公式在 A 系统里成立在 B 系统里可能不成立。如果模型不知道当前应该采用哪套语义它就会按照训练语料里最常见的语义模式来猜测而这种猜测往往与用户设定的语义不一致。比如训练语料里大量出现“必然”这个词模型可能默认把它理解为“所有情况都成立”的常识必然性。但如果在道义逻辑里□ 表示“应当”那么“□p”的含义就完全不同。因此评估大模型是否遵守模态逻辑规范本质上是在评估模型能否把“语境中的语义约定”内化到推理过程里。1.3 本文要评测的问题我们关注三个递进的问题语法层面模型能否识别模态逻辑公式的结构比如区分 □(p → q) 与 (□p → q)语义层面给定同一公式和不同的语义约定模型是否会产生不同的判断规范遵守层面模型给出的判断是否与 Kripke 模型上的真实真值一致这三个问题层层递进。语法识别是基础语义区分是关键规范遵守是最终目标。把这三个问题拆开评测就能定位模型在哪个环节出了问题。2. “同公式不同语义”的本质2.1 语法层与语义层的分离模态逻辑公式是语法对象本身不包含含义。同一个字符串“□(p → q)”可以出现在不同的逻辑系统中关键是解释它的模型结构不同。解释模态公式的标准框架是 Kripke 模型记作 M (W, R, V)其中W 是非空的世界集合R 是 W 上的二元可达关系用于刻画“从某个世界能看到哪些世界”V 是赋值函数决定每个世界上哪些原子命题为真。公式 □φ 在世界 w 上为真当且仅当对所有满足 w R w 的世界 wφ 在 w 上为真。公式 ◇φ 在世界 w 上为真当且仅当存在某个满足 w R w 的世界 wφ 在 w 上为真。注意这里的 R 是整个语义的核心。同一个公式只要 R 的性质不同真值就可能发生变化。2.2 四种典型的语义差异在自然语言与工程场景里□ 和 ◇ 最常见的四种解释如下逻辑系统□ 的含义◇ 的含义典型场景真势模态Alethic必然可能哲学、形而上学认知逻辑Epistemic知道 / 根据知识可得与知识相容Agent 推理、知识库道义逻辑Deontic应当 / 义务允许安全策略、合规检查时序逻辑Temporal所有未来时刻某个未来时刻系统验证、运行时监控同一公式 □φ 在这四种系统里分别读作“必然 φ”“知道 φ”“应当 φ”“永远 φ”。如果不显式声明当前使用的是哪种语义任何 LLM 都没有充分信息做出正确判断——它只能靠猜。2.3 帧条件带来的隐藏差异除了模态算子的含义可达关系的性质也会改变公式的真值。常见的帧条件包括自反性每个世界都能到达自身传递性如果 w1 可达 w2w2 可达 w3则 w1 可达 w3对称性如果 w1 可达 w2则 w2 可达 w1系列性seriality每个世界至少有一个可达世界。例如公式 □p → ◇p在自反帧上恒真但在非自反且非系列的帧上可能为假。再比如公理 4□p → □□p只有当可达关系满足传递性时才在所有模型上成立。这些帧条件属于语义的一部分但很多 LLM 并不知道或者说模型没有把它作为约束纳入推理。2.4 一个例子看懂差异假设我们有如下 Kripke 模型世界w0, w1, w2 可达关系w0 可达 w1w0 可达 w2w1、w2 不可达其他世界 赋值V(w1) {p}V(w2) {}在这个模型里公式 ◇p 在 w0 上为真因为 w1 是 w0 的可达世界且 p 在 w1 为真。□p 在 w0 上为假因为 w2 可达且 p 在 w2 为假。这里不需要知道 ◇ 是“可能”还是“允许”公式在给定模型上的真值已经确定。但如果换一个模型只把可达关系改成 w0 可达 w1w1 可达 w2w2 可达 w2那么 □p 在 w0 上的真值就可能改变。这说明公式相同模型不同结果不同。LLM 评测的关键就在于模型能否感知到这些结构差异而不是死记硬背公式的“常见答案”。3. 评测思路设计3.1 评测目标我们设计的评测不是简单地问“这个公式成立吗”而是构造一组对照组。每组对照共享同一个公式但语义背景不同、Kripke 模型不同因此标准答案也不同。只有模型在每组的判断都正确才说明模型真正遵守了给定的语义规范。具体来说每条评测样本包含四部分公式文本语义约定文本例如“□ 表示必然”或“□ 表示应当”Kripke 模型描述世界、可达关系、命题赋值标准答案某个指定世界上的真值。评测时我们把前两部分作为 Prompt 发给模型让模型输出 TRUE 或 FALSE再与标准答案对比。3.2 评测管线四步走整个评测管线可以分成四步。第一步构造公式池。选取一定数量的模板例如 □p、◇p、□(p → q)、◇(p ∧ q)、□p → ◇p 等覆盖不同算子组合和嵌套深度。第二步为每个公式生成多组带语义标注的样本。同一公式至少配对两种不同的语义约定例如把 □ 分别声明为“必然”和“应当”这样就能观察模型是否会因为语义说明不同而改变判断。第三步用验证器求标准答案。基于给定模型用可靠的求值代码算出公式真值作为 ground truth。第四步调用 LLM 获取预测并比较。记录模型输出、标准答案以及二者的差异最后按公式类型、语义类型、嵌套深度等维度做统计。3.3 为什么引入 ReAct 风格推理直接让 LLM 回答“TRUE 还是 FALSE”模型很容易凭模式匹配快速作答跳过了真正的语义计算。ReActReasoning Acting的核心思想是让模型在推理过程中交替执行“思考”和“工具调用”把外部工具的结果作为观察反馈从而减少幻觉。在模态逻辑评测里我们可以把 Kripke 模型验证器封装成一个工具。模型被允许先思考公式是什么结构符号在哪个世界求值需要检查哪些可达世界然后调用工具进行验证最后根据工具返回结果给出答案。这种方式既能提升答案可靠性也让我们能观察到模型在推理过程中的中间状态。当然ReAct 不是必须的。如果你只需要快速判断模型的基础语义理解能力直接 Prompt 就够了。但如果你想用模型去完成“生成规范并验证规范”这种复合任务ReAct 是更符合生产形态的评测方式。4. 环境准备与项目结构4.1 环境清单本文示例代码以 Python 3.10 为基础需要以下依赖pip install openaiopenai SDK 用于调用 OpenAI 兼容接口。如果你使用的是内部部署的模型比如 vLLM、Ollama 或者企业网关只需要把client.chat.completions.create替换成对应 SDK 的调用即可。其余逻辑完全不变。模型版本建议根据你实际可用的模型来配置本文不做假设示例中默认使用gpt-4o-mini占位实际使用时替换成你的模型名。操作系统不限Windows / macOS / Linux 均可。建议在虚拟环境中运行避免依赖冲突。4.2 项目结构eval_modal_llm/ ├── formula.py # 公式表示与文本转换 ├── kripke.py # Kripke 模型与真值求值器 ├── prompts.py # Prompt 模板 ├── evaluator.py # LLM 评测主脚本 ├── react_evaluator.py# ReAct 风格评测脚本 └── samples.py # 评测样本构造下面逐个文件实现。5. 核心代码实现5.1 公式表示我们使用元组来递归表示模态逻辑公式规则如下命题p 否定(not, phi) 合取(and, phi, psi) 蕴含(imp, phi, psi) 必然(box, phi) 可能(dia, phi)代码位于formula.py# 文件路径eval_modal_llm/formula.py def formula_to_text(f): 将公式元组转成便于阅读的文本形式。 if isinstance(f, str): return f op f[0] if op not: return f¬{formula_to_text(f[1])} if op and: return f({formula_to_text(f[1])} ∧ {formula_to_text(f[2])}) if op imp: return f({formula_to_text(f[1])} → {formula_to_text(f[2])}) if op box: return f□({formula_to_text(f[1])}) if op dia: return f◇({formula_to_text(f[1])}) raise ValueError(f未知算子: {op})这个函数的作用是让公式在 Prompt 中显示得更自然同时在日志里也方便观察。它不承担任何语义计算只负责字符串转换。5.2 Kripke 模型与真值求值器接下来实现 Kripke 模型类与真值求值器。代码位于kripke.py# 文件路径eval_modal_llm/kripke.py from dataclasses import dataclass, field dataclass class KripkeModel: Kripke 模型世界集合、可达关系、命题赋值。 worlds: list accessible: dict valuation: dict def eval_formula(model, formula, world): 在 model 的 world 节点上对公式求值返回布尔值。 if isinstance(formula, str): return formula in model.valuation.get(world, set()) op formula[0] if op not: return not eval_formula(model, formula[1], world) if op and: return eval_formula(model, formula[1], world) and eval_formula( model, formula[2], world ) if op imp: left eval_formula(model, formula[1], world) right eval_formula(model, formula[2], world) return (not left) or right if op box: for next_world in model.accessible.get(world, []): if not eval_formula(model, formula[1], next_world): return False return True if op dia: for next_world in model.accessible.get(world, []): if eval_formula(model, formula[1], next_world): return True return False raise ValueError(f未知算子: {op})这里有几个实现细节需要解释。第一命题求值直接查 valuation 字典如果世界不在字典中按原子命题为假处理。第二box 算子使用all语义遍历所有可达世界只要有任意一个可达世界使公式为假结果就为假如果可达世界集合为空box 公式在这个世界上“空真”为真。第三imp 算子按经典蕴含语义实现即前件为假或后件为真时整体为真。空可达集合下的 box 为空真这一点在构造评测样本时特别容易出错。如果你希望“没有可达世界时 □φ 为假”需要显式修改求值逻辑。标准 Kripke 语义中空真成立但某些工程系统例如运行时监控可能采用不同的约定。本文示例遵循标准语义。5.3 构造 Prompt 模板Prompt 是评测的核心输入。我们要把公式、语义约定、模型描述三段信息清晰分开避免模型混淆。代码位于prompts.py# 文件路径eval_modal_llm/prompts.py SYSTEM_PROMPT 你是一个严谨的模态逻辑评估器。 你需要根据用户给出的语义约定和模型描述判断模态逻辑公式在指定世界上的真值。 请只回答 TRUE 或 FALSE并附上一句简要理由。 def build_user_prompt(formula_text, semantics_text, model_text, target_world): return f【公式】 {formula_text} 【语义约定】 {semantics_text} 【模型描述】 {model_text} 【待判断】 请问公式 {formula_text} 在世界上 {target_world} 是否为真 请输出 TRUE 或 FALSE并简要说明理由。语义约定文本建议写成自然语言例如“□ 表示必然公式 □φ 在所有可达世界上为真时成立◇φ 在存在可达世界使 φ 为真时成立。”模型描述文本则可以这样写“世界集合为 {w0, w1, w2}可达关系为 w0→w1, w0→w2命题赋值为w1 中 p 为真w2 中 q 为真。”注意模型描述里不要给出目标世界上的答案否则评测就失去了意义。5.4 调用 LLM 评测评测主脚本位于evaluator.py负责加载样本、调用模型、解析答案、计算准确率。# 文件路径eval_modal_llm/evaluator.py import json from openai import OpenAI from formula import formula_to_text from kripke import KripkeModel, eval_formula from prompts import SYSTEM_PROMPT, build_user_prompt def call_llm(model, user_prompt, temperature0.0): 调用大模型接口返回模型回复文本。 client OpenAI() resp client.chat.completions.create( modelmodel, temperaturetemperature, messages[ {role: system, content: SYSTEM_PROMPT}, {role: user, content: user_prompt}, ], ) return resp.choices[0].message.content def parse_truth(text): 从模型回复文本中解析出 TRUE 或 FALSE。 stock text.strip().upper() if stock.startswith(TRUE): return True if stock.startswith(FALSE): return False # 容错解析按词拆分找第一个布尔词 for token in stock.split(): if token in (TRUE, 真): return True if token in (FALSE, 假): return False raise ValueError(f无法解析模型输出: {text}) def evaluate_sample(sample, modelgpt-4o-mini): 对单条样本执行评测返回预测结果、标准答案与模型输出。 formula sample[formula] formula_text formula_to_text(formula) user_prompt build_user_prompt( formula_textformula_text, semantics_textsample[semantics], model_textsample[model_desc], target_worldsample[target_world], ) # 计算标准答案 km KripkeModel( worldssample[worlds], accessiblesample[accessible], valuationsample[valuation], ) ground_truth eval_formula(km, formula, sample[target_world]) model_output call_llm(model, user_prompt) prediction None try: prediction parse_truth(model_output) except ValueError as exc: print(f[解析失败] {exc}) return { formula_text: formula_text, ground_truth: ground_truth, prediction: prediction, model_output: model_output, prompt: user_prompt, ok: prediction ground_truth, }解析函数需要注意很多模型会输出“TRUE因为……”所以直接用startswith判断是最稳妥的。如果模型偶尔输出中文“真/假”也做了兼容。在真实评测中解析失败本身就是一项重要指标说明模型没有遵守输出格式这在生产环境中是不能接受的。5.5 ReAct 风格增强评测ReAct 的工程价值在于把模型从“一次作答”变成“边思考边验证”。下面实现一个简化版 ReAct 循环让模型可以调用check_formula工具输入公式文本、目标世界编号和模型编号工具内部会加载对应 Kripke 模型并返回真值。# 文件路径eval_modal_llm/react_evaluator.py import json from openai import OpenAI from kripke import KripkeModel, eval_formula def check_formula(formula, world, model_id, sample_lib): 工具函数从样本库中取出模型计算指定世界上的公式真值。 sample sample_lib[model_id] km KripkeModel( worldssample[worlds], accessiblesample[accessible], valuationsample[valuation], ) return eval_formula(km, formula, world) TOOL_DESCRIPTION \ 你可以使用以下工具 - check_formula(formula, world, model_id): 返回公式在指定世界上的真值。 参数 formula 使用元组表示例如 (box, p) 表示 □p。 def react_loop(user_task, sample_lib, modelgpt-4o-mini, max_steps5): 执行 ReAct 循环返回最终答复与中间步骤。 client OpenAI() messages [ {role: system, content: 你是一个可以调用工具验证模态逻辑公式的助手。 TOOL_DESCRIPTION}, {role: user, content: user_task}, ] steps [] for _ in range(max_steps): resp client.chat.completions.create( modelmodel, temperature0.0, messagesmessages, ) reply resp.choices[0].message.content steps.append(reply) # 检测是否包含工具调用指令这里用简化的 JSON 动作格式 if [TOOL_CALL] in reply: try: action_block reply.split([TOOL_CALL])[-1].split([/TOOL_CALL])[0] action json.loads(action_block) result check_formula( action[formula], action[world], action[model_id], sample_lib, ) messages.append({role: assistant, content: reply}) messages.append({ role: user, content: f[TOOL_RESULT] {result}, }) continue except Exception as exc: messages.append({role: user, content: f[TOOL_ERROR] {exc}}) continue # 没有工具调用说明模型准备给出最终答案 return {final_answer: reply, steps: steps} return {final_answer: 达到最大迭代次数未给出明确答案, steps: steps}这个实现故意做了一些简化比如用字符串标记[TOOL_CALL]来触发工具调用。在真实生产环境中通常使用 Function Calling 机制来结构化地传递工具参数。本文用简化写法是为了把 ReAct 的核心流程展示清楚模型生成思考 → 发起工具调用 → 工具返回观察结果 → 模型继续推理 → 直到给出最终答案。6. 运行与结果解读6.1 构造样本并运行下面构造两组对照样本它们使用同一个公式但语义约定不同。第一组把 □ 解释为“必然”第二组把 □ 解释为“应当”。两组共享同一个 Kripke 模型因此标准答案是一致的。如果 LLM 对两组给出不同答案就说明它被语义描述干扰了。# 文件路径eval_modal_llm/samples.py SAMPLE_LIB { alethic: { formula: (box, (imp, p, q)), semantics: □ 表示必然□φ 在所有可达世界上为真时成立。, worlds: [w0, w1, w2], accessible: {w0: [w1, w2], w1: [], w2: []}, valuation: {w0: set(), w1: {p, q}, w2: {p}}, target_world: w0, model_desc: 世界w0, w1, w2可达w0 可达 w1 和 w2赋值w1 中 p 和 q 为真w2 中只有 p 为真。, }, deontic: { formula: (box, (imp, p, q)), semantics: □ 表示应当□φ 在满足义务要求的所有理想世界中为真时成立。, worlds: [w0, w1, w2], accessible: {w0: [w1, w2], w1: [], w2: []}, valuation: {w0: set(), w1: {p, q}, w2: {p}}, target_world: w0, model_desc: 理想世界集合w1, w2赋值w1 中 p 和 q 为真w2 中只有 p 为真。, }, }运行主评测脚本# 文件路径eval_modal_llm/run.py from samples import SAMPLE_LIB from evaluator import evaluate_sample def main(): for sample_id, sample in SAMPLE_LIB.items(): result evaluate_sample(sample) print(json.dumps(result, ensure_asciiFalse, indent2)) print(- * 60) if __name__ __main__: main()预期输出会包含每条样本的标准答案、预测结果与模型原始输出。在本文示例中□(p → q) 在 w0 上需要检查 w1 和 w2w1 中 p → q 为真w2 中 p 为真但 q 为假所以 p → q 为假因此整体结果为 FALSE。两组样本的标准答案都是 FALSE。关键观察点在于模型在“alethic”和“deontic”两组中是否都给出了 FALSE。如果其中一组因为“应当”语义而给出 TRUE说明模型没有真正执行语义计算而是在调用训练记忆中的语义联想。6.2 关注哪些指标评测不能只看整体准确率建议按以下维度拆解公式结构嵌套深度为 1 的公式是否比嵌套深度为 2 的公式准确率更高语义类型不同语义约定之间是否存在显著差异可达关系复杂度可达世界数量为 0、1、多个时模型表现是否稳定输出格式合规率模型输出是否严格可解析为 TRUE / FALSE。如果某个维度准确率明显偏低就说明模型在该维度上的语义理解是薄弱点。比如模型在“可达世界为空”的样本上频繁出错可能是因为它没有掌握 box 空真规则也可能是因为训练语料里很少出现空可达关系的情形。7. 常见问题与排查思路在实际运行这套评测时你大概率会遇到下面几类问题。问题现象常见原因解决思路模型总是回答 TRUE很少回答 FALSE模型倾向于接受无约束条件的公式存在默认肯定偏差在 Prompt 中显式要求“先检查反例再看是否成立”在样本中提高 FALSE 比例输出无法解析为 TRUE/FALSEPrompt 没有严格要求格式或模型擅长自由发挥在 system prompt 中加入“只允许输出 TRUE 或 FALSE”的约束解析函数增加容错同一公式在不同语义下答案一致模型没有真正读取语义约定直接按常识推理随机打乱语义文本与模型描述的对应关系加入反常识语义进行对照小模型表现不稳换一次输入结果不同temperature 过高或模型本身随机性大评测时 temperature 设为 0多次重复取多数票ReAct 循环陷入死循环模型反复请求工具调用但参数不合法限制最大迭代次数工具参数格式改为 JSON Schema 校验返回错误信息给模型标准答案与人工判断不符Kripke 模型构造或求值逻辑有误先单独测试 eval_formula 在简单模型上的结果编写单元测试覆盖 box/dia 空集情形最常见且最容易被忽略的是第一条默认肯定偏差。很多大语言模型在二分类判断题里倾向回答“是”因为训练语料中肯定形式的问题和答案占比更高。解决办法是让评测样本中 TRUE 与 FALSE 的分布尽量平衡并且在 Prompt 中告诉模型“不是所有公式都为真请仔细检查”。另外如果你发现模型的准确率整组偏低先不要怀疑模型能力先检查样本构造是否正确。一个简单的自检方法是把求值器换成人工推导先用小模型逐个验证标准答案再开始批量评测。8. 最佳实践与工程建议8.1 Prompt 设计原则第一把语义约定放在公式之前。人在阅读时遵循自然顺序模型也一样。先讲清楚“□ 表示什么”“可达关系是什么”再给出具体公式模型更容易把二者绑定在一起。第二明确输出格式。不要只写“请回答”要写“请只输出 TRUE 或 FALSE”。在 system prompt 里重复一次比在 user prompt 里强调更有效。第三避免公式歧义。如果公式里同时出现多个模态算子可以在公式文本后用一句话补充说明括号范围例如“□ 的辖域是 (p → q) 整体”。8.2 评测数据治理评测数据应该与训练数据隔离避免模型见过相同或近似样本。构造样本时建议随机生成 Kripke 模型而不是手工写死几个固定模型。随机生成时要注意控制世界数量、可达关系密度和命题组合的复杂度保证样本能够覆盖不同难度梯度。生成之后需要对样本做合法性校验确保可达关系中的节点都在世界集合内确保 valuation 只包含已知命题。这一步非常关键因为随机生成容易产生脏数据脏数据会污染标准答案的计算。8.3 生产落地注意点在真实项目中模态逻辑评测通常不是一个单次实验而是一个持续运行的回归测试。建议把评测脚本接入 CI每当模型版本升级、Prompt 模板修改、语义约定调整时都自动跑一遍防止模型行为回归。日志记录也值得重视。建议记录每一条样本的完整 Prompt、模型输出、解析结果和标准答案。这样后续分析错误时可以直接定位到具体的 Prompt 设计和模型选择。如果涉及生产环境中的代码或数据变更务必遵循最小权限原则评测脚本只读数据不写生产数据库模型调用使用独立 API Key评测结果先落到测试环境确认无误后再同步到正式环境。9. 总结与学习路线本文从“同一公式、不同语义”这个现象出发完整搭建了一套评测大语言模型模态逻辑规范遵守能力的工程方案。核心收获可以总结为三点理解模态逻辑的语义分层是评测的前提构造对照样本比堆叠公式数量更重要验证器与 LLM 的结合是提升评测可靠性的关键。如果你想继续深入可以沿着以下方向推进把公式池从标准模态逻辑扩展到 LTL 和 CTL加入时态算子后评测难度会显著提升引入模型检查器工具如 NuSMV 或 LTL 工具链作为 ReAct 循环中的外部验证器用失败样本做针对性 Prompt 微调或构建 few-shot 示例。接下来的实际操作建议是先不用急着接大模型而是把公式表示、Kripke 模型和求值器写通确保标准答案准确然后加入两条最简单的对照样本观察模型行为最后再逐步扩展到全量公式池。这样每一步都有明确的验证点遇到问题也能快速定位。 同一公式不同语义：评测大语言模型对模态逻辑规范的遵循程度
在形式化需求规格生成与验证的实际项目中最容易被低估的问题往往不是“模型看不懂逻辑公式”而是“模型把同一套公式默认成了同一套语义”。比如 □(p → q) 这个公式在时序逻辑里可以表示“p 之后 q 永远成立”在道义逻辑里表示“义务上 p 蕴含 q”在认知逻辑里又可能被理解为“智能体知道 p 蕴含 q”。公式的语法一模一样语义解释却天差地别。这也正是标题所反映的核心问题Same Formulas, Different Semantics: Do Language Models Follow Modal Logic Specifications?——大语言模型在多大程度上会遵守我们给定的模态逻辑语义规范这篇文章会把这个问题拆成一个可以动手复现的评测工程。我们会先讲清楚模态逻辑的语法与语义分层再设计一套“同一公式、不同语义、不同模型”的评测思路最后给出完整的 Python 代码包含公式构造、Kripke 模型验证器、LLM 评测脚本和 ReAct 风格推理增强。无论你是做 NLP 评测、形式化验证还是想用 LLM 自动生成安全策略都能直接复用这套方法。1. 背景与核心概念1.1 模态逻辑到底是什么模态逻辑Modal Logic是在经典命题逻辑的基础上引入“必然”□和“可能”◇两个模态算子的逻辑系统。它要回答的问题不是“命题是否为真”而是“命题在什么条件下必然为真在什么条件下可能为真”。举个直观的例子。经典逻辑里语句“北京是中国的首都”是真命题它不依赖任何视角或场景。但语句“明天会下雨”就不能用经典逻辑直接判定真假因为它的真值取决于“未来状态”这个语义背景。模态逻辑通过引入可能世界possible world和可达关系accessibility relation把这类依赖语境的真假判断形式化。在形式化验证领域模态逻辑的变体应用非常广泛线性时序逻辑LTL用来描述系统运行轨迹上的属性计算树逻辑CTL用来描述分支时间上的属性动态逻辑和描述逻辑则用于程序验证与知识表示。可以说模态逻辑是连接自然语言需求与机器可验证规范之间的桥梁。1.2 为什么大模型需要理解模态逻辑规范大语言模型近年来被越来越多地用于生成形式化规范从自然语言需求自动生成 LTL 断言从代码注释提取前置条件甚至把安全策略转换成约束规则。这背后的假设是模型不仅懂得自然语言还懂得形式逻辑背后的语义。但这里有一个工程上非常现实的问题形式逻辑的“规范”不是一个写在纸面上的字符串而是一套语义解释规则。同一个公式在 A 系统里成立在 B 系统里可能不成立。如果模型不知道当前应该采用哪套语义它就会按照训练语料里最常见的语义模式来猜测而这种猜测往往与用户设定的语义不一致。比如训练语料里大量出现“必然”这个词模型可能默认把它理解为“所有情况都成立”的常识必然性。但如果在道义逻辑里□ 表示“应当”那么“□p”的含义就完全不同。因此评估大模型是否遵守模态逻辑规范本质上是在评估模型能否把“语境中的语义约定”内化到推理过程里。1.3 本文要评测的问题我们关注三个递进的问题语法层面模型能否识别模态逻辑公式的结构比如区分 □(p → q) 与 (□p → q)语义层面给定同一公式和不同的语义约定模型是否会产生不同的判断规范遵守层面模型给出的判断是否与 Kripke 模型上的真实真值一致这三个问题层层递进。语法识别是基础语义区分是关键规范遵守是最终目标。把这三个问题拆开评测就能定位模型在哪个环节出了问题。2. “同公式不同语义”的本质2.1 语法层与语义层的分离模态逻辑公式是语法对象本身不包含含义。同一个字符串“□(p → q)”可以出现在不同的逻辑系统中关键是解释它的模型结构不同。解释模态公式的标准框架是 Kripke 模型记作 M (W, R, V)其中W 是非空的世界集合R 是 W 上的二元可达关系用于刻画“从某个世界能看到哪些世界”V 是赋值函数决定每个世界上哪些原子命题为真。公式 □φ 在世界 w 上为真当且仅当对所有满足 w R w 的世界 wφ 在 w 上为真。公式 ◇φ 在世界 w 上为真当且仅当存在某个满足 w R w 的世界 wφ 在 w 上为真。注意这里的 R 是整个语义的核心。同一个公式只要 R 的性质不同真值就可能发生变化。2.2 四种典型的语义差异在自然语言与工程场景里□ 和 ◇ 最常见的四种解释如下逻辑系统□ 的含义◇ 的含义典型场景真势模态Alethic必然可能哲学、形而上学认知逻辑Epistemic知道 / 根据知识可得与知识相容Agent 推理、知识库道义逻辑Deontic应当 / 义务允许安全策略、合规检查时序逻辑Temporal所有未来时刻某个未来时刻系统验证、运行时监控同一公式 □φ 在这四种系统里分别读作“必然 φ”“知道 φ”“应当 φ”“永远 φ”。如果不显式声明当前使用的是哪种语义任何 LLM 都没有充分信息做出正确判断——它只能靠猜。2.3 帧条件带来的隐藏差异除了模态算子的含义可达关系的性质也会改变公式的真值。常见的帧条件包括自反性每个世界都能到达自身传递性如果 w1 可达 w2w2 可达 w3则 w1 可达 w3对称性如果 w1 可达 w2则 w2 可达 w1系列性seriality每个世界至少有一个可达世界。例如公式 □p → ◇p在自反帧上恒真但在非自反且非系列的帧上可能为假。再比如公理 4□p → □□p只有当可达关系满足传递性时才在所有模型上成立。这些帧条件属于语义的一部分但很多 LLM 并不知道或者说模型没有把它作为约束纳入推理。2.4 一个例子看懂差异假设我们有如下 Kripke 模型世界w0, w1, w2 可达关系w0 可达 w1w0 可达 w2w1、w2 不可达其他世界 赋值V(w1) {p}V(w2) {}在这个模型里公式 ◇p 在 w0 上为真因为 w1 是 w0 的可达世界且 p 在 w1 为真。□p 在 w0 上为假因为 w2 可达且 p 在 w2 为假。这里不需要知道 ◇ 是“可能”还是“允许”公式在给定模型上的真值已经确定。但如果换一个模型只把可达关系改成 w0 可达 w1w1 可达 w2w2 可达 w2那么 □p 在 w0 上的真值就可能改变。这说明公式相同模型不同结果不同。LLM 评测的关键就在于模型能否感知到这些结构差异而不是死记硬背公式的“常见答案”。3. 评测思路设计3.1 评测目标我们设计的评测不是简单地问“这个公式成立吗”而是构造一组对照组。每组对照共享同一个公式但语义背景不同、Kripke 模型不同因此标准答案也不同。只有模型在每组的判断都正确才说明模型真正遵守了给定的语义规范。具体来说每条评测样本包含四部分公式文本语义约定文本例如“□ 表示必然”或“□ 表示应当”Kripke 模型描述世界、可达关系、命题赋值标准答案某个指定世界上的真值。评测时我们把前两部分作为 Prompt 发给模型让模型输出 TRUE 或 FALSE再与标准答案对比。3.2 评测管线四步走整个评测管线可以分成四步。第一步构造公式池。选取一定数量的模板例如 □p、◇p、□(p → q)、◇(p ∧ q)、□p → ◇p 等覆盖不同算子组合和嵌套深度。第二步为每个公式生成多组带语义标注的样本。同一公式至少配对两种不同的语义约定例如把 □ 分别声明为“必然”和“应当”这样就能观察模型是否会因为语义说明不同而改变判断。第三步用验证器求标准答案。基于给定模型用可靠的求值代码算出公式真值作为 ground truth。第四步调用 LLM 获取预测并比较。记录模型输出、标准答案以及二者的差异最后按公式类型、语义类型、嵌套深度等维度做统计。3.3 为什么引入 ReAct 风格推理直接让 LLM 回答“TRUE 还是 FALSE”模型很容易凭模式匹配快速作答跳过了真正的语义计算。ReActReasoning Acting的核心思想是让模型在推理过程中交替执行“思考”和“工具调用”把外部工具的结果作为观察反馈从而减少幻觉。在模态逻辑评测里我们可以把 Kripke 模型验证器封装成一个工具。模型被允许先思考公式是什么结构符号在哪个世界求值需要检查哪些可达世界然后调用工具进行验证最后根据工具返回结果给出答案。这种方式既能提升答案可靠性也让我们能观察到模型在推理过程中的中间状态。当然ReAct 不是必须的。如果你只需要快速判断模型的基础语义理解能力直接 Prompt 就够了。但如果你想用模型去完成“生成规范并验证规范”这种复合任务ReAct 是更符合生产形态的评测方式。4. 环境准备与项目结构4.1 环境清单本文示例代码以 Python 3.10 为基础需要以下依赖pip install openaiopenai SDK 用于调用 OpenAI 兼容接口。如果你使用的是内部部署的模型比如 vLLM、Ollama 或者企业网关只需要把client.chat.completions.create替换成对应 SDK 的调用即可。其余逻辑完全不变。模型版本建议根据你实际可用的模型来配置本文不做假设示例中默认使用gpt-4o-mini占位实际使用时替换成你的模型名。操作系统不限Windows / macOS / Linux 均可。建议在虚拟环境中运行避免依赖冲突。4.2 项目结构eval_modal_llm/ ├── formula.py # 公式表示与文本转换 ├── kripke.py # Kripke 模型与真值求值器 ├── prompts.py # Prompt 模板 ├── evaluator.py # LLM 评测主脚本 ├── react_evaluator.py# ReAct 风格评测脚本 └── samples.py # 评测样本构造下面逐个文件实现。5. 核心代码实现5.1 公式表示我们使用元组来递归表示模态逻辑公式规则如下命题p 否定(not, phi) 合取(and, phi, psi) 蕴含(imp, phi, psi) 必然(box, phi) 可能(dia, phi)代码位于formula.py# 文件路径eval_modal_llm/formula.py def formula_to_text(f): 将公式元组转成便于阅读的文本形式。 if isinstance(f, str): return f op f[0] if op not: return f¬{formula_to_text(f[1])} if op and: return f({formula_to_text(f[1])} ∧ {formula_to_text(f[2])}) if op imp: return f({formula_to_text(f[1])} → {formula_to_text(f[2])}) if op box: return f□({formula_to_text(f[1])}) if op dia: return f◇({formula_to_text(f[1])}) raise ValueError(f未知算子: {op})这个函数的作用是让公式在 Prompt 中显示得更自然同时在日志里也方便观察。它不承担任何语义计算只负责字符串转换。5.2 Kripke 模型与真值求值器接下来实现 Kripke 模型类与真值求值器。代码位于kripke.py# 文件路径eval_modal_llm/kripke.py from dataclasses import dataclass, field dataclass class KripkeModel: Kripke 模型世界集合、可达关系、命题赋值。 worlds: list accessible: dict valuation: dict def eval_formula(model, formula, world): 在 model 的 world 节点上对公式求值返回布尔值。 if isinstance(formula, str): return formula in model.valuation.get(world, set()) op formula[0] if op not: return not eval_formula(model, formula[1], world) if op and: return eval_formula(model, formula[1], world) and eval_formula( model, formula[2], world ) if op imp: left eval_formula(model, formula[1], world) right eval_formula(model, formula[2], world) return (not left) or right if op box: for next_world in model.accessible.get(world, []): if not eval_formula(model, formula[1], next_world): return False return True if op dia: for next_world in model.accessible.get(world, []): if eval_formula(model, formula[1], next_world): return True return False raise ValueError(f未知算子: {op})这里有几个实现细节需要解释。第一命题求值直接查 valuation 字典如果世界不在字典中按原子命题为假处理。第二box 算子使用all语义遍历所有可达世界只要有任意一个可达世界使公式为假结果就为假如果可达世界集合为空box 公式在这个世界上“空真”为真。第三imp 算子按经典蕴含语义实现即前件为假或后件为真时整体为真。空可达集合下的 box 为空真这一点在构造评测样本时特别容易出错。如果你希望“没有可达世界时 □φ 为假”需要显式修改求值逻辑。标准 Kripke 语义中空真成立但某些工程系统例如运行时监控可能采用不同的约定。本文示例遵循标准语义。5.3 构造 Prompt 模板Prompt 是评测的核心输入。我们要把公式、语义约定、模型描述三段信息清晰分开避免模型混淆。代码位于prompts.py# 文件路径eval_modal_llm/prompts.py SYSTEM_PROMPT 你是一个严谨的模态逻辑评估器。 你需要根据用户给出的语义约定和模型描述判断模态逻辑公式在指定世界上的真值。 请只回答 TRUE 或 FALSE并附上一句简要理由。 def build_user_prompt(formula_text, semantics_text, model_text, target_world): return f【公式】 {formula_text} 【语义约定】 {semantics_text} 【模型描述】 {model_text} 【待判断】 请问公式 {formula_text} 在世界上 {target_world} 是否为真 请输出 TRUE 或 FALSE并简要说明理由。语义约定文本建议写成自然语言例如“□ 表示必然公式 □φ 在所有可达世界上为真时成立◇φ 在存在可达世界使 φ 为真时成立。”模型描述文本则可以这样写“世界集合为 {w0, w1, w2}可达关系为 w0→w1, w0→w2命题赋值为w1 中 p 为真w2 中 q 为真。”注意模型描述里不要给出目标世界上的答案否则评测就失去了意义。5.4 调用 LLM 评测评测主脚本位于evaluator.py负责加载样本、调用模型、解析答案、计算准确率。# 文件路径eval_modal_llm/evaluator.py import json from openai import OpenAI from formula import formula_to_text from kripke import KripkeModel, eval_formula from prompts import SYSTEM_PROMPT, build_user_prompt def call_llm(model, user_prompt, temperature0.0): 调用大模型接口返回模型回复文本。 client OpenAI() resp client.chat.completions.create( modelmodel, temperaturetemperature, messages[ {role: system, content: SYSTEM_PROMPT}, {role: user, content: user_prompt}, ], ) return resp.choices[0].message.content def parse_truth(text): 从模型回复文本中解析出 TRUE 或 FALSE。 stock text.strip().upper() if stock.startswith(TRUE): return True if stock.startswith(FALSE): return False # 容错解析按词拆分找第一个布尔词 for token in stock.split(): if token in (TRUE, 真): return True if token in (FALSE, 假): return False raise ValueError(f无法解析模型输出: {text}) def evaluate_sample(sample, modelgpt-4o-mini): 对单条样本执行评测返回预测结果、标准答案与模型输出。 formula sample[formula] formula_text formula_to_text(formula) user_prompt build_user_prompt( formula_textformula_text, semantics_textsample[semantics], model_textsample[model_desc], target_worldsample[target_world], ) # 计算标准答案 km KripkeModel( worldssample[worlds], accessiblesample[accessible], valuationsample[valuation], ) ground_truth eval_formula(km, formula, sample[target_world]) model_output call_llm(model, user_prompt) prediction None try: prediction parse_truth(model_output) except ValueError as exc: print(f[解析失败] {exc}) return { formula_text: formula_text, ground_truth: ground_truth, prediction: prediction, model_output: model_output, prompt: user_prompt, ok: prediction ground_truth, }解析函数需要注意很多模型会输出“TRUE因为……”所以直接用startswith判断是最稳妥的。如果模型偶尔输出中文“真/假”也做了兼容。在真实评测中解析失败本身就是一项重要指标说明模型没有遵守输出格式这在生产环境中是不能接受的。5.5 ReAct 风格增强评测ReAct 的工程价值在于把模型从“一次作答”变成“边思考边验证”。下面实现一个简化版 ReAct 循环让模型可以调用check_formula工具输入公式文本、目标世界编号和模型编号工具内部会加载对应 Kripke 模型并返回真值。# 文件路径eval_modal_llm/react_evaluator.py import json from openai import OpenAI from kripke import KripkeModel, eval_formula def check_formula(formula, world, model_id, sample_lib): 工具函数从样本库中取出模型计算指定世界上的公式真值。 sample sample_lib[model_id] km KripkeModel( worldssample[worlds], accessiblesample[accessible], valuationsample[valuation], ) return eval_formula(km, formula, world) TOOL_DESCRIPTION \ 你可以使用以下工具 - check_formula(formula, world, model_id): 返回公式在指定世界上的真值。 参数 formula 使用元组表示例如 (box, p) 表示 □p。 def react_loop(user_task, sample_lib, modelgpt-4o-mini, max_steps5): 执行 ReAct 循环返回最终答复与中间步骤。 client OpenAI() messages [ {role: system, content: 你是一个可以调用工具验证模态逻辑公式的助手。 TOOL_DESCRIPTION}, {role: user, content: user_task}, ] steps [] for _ in range(max_steps): resp client.chat.completions.create( modelmodel, temperature0.0, messagesmessages, ) reply resp.choices[0].message.content steps.append(reply) # 检测是否包含工具调用指令这里用简化的 JSON 动作格式 if [TOOL_CALL] in reply: try: action_block reply.split([TOOL_CALL])[-1].split([/TOOL_CALL])[0] action json.loads(action_block) result check_formula( action[formula], action[world], action[model_id], sample_lib, ) messages.append({role: assistant, content: reply}) messages.append({ role: user, content: f[TOOL_RESULT] {result}, }) continue except Exception as exc: messages.append({role: user, content: f[TOOL_ERROR] {exc}}) continue # 没有工具调用说明模型准备给出最终答案 return {final_answer: reply, steps: steps} return {final_answer: 达到最大迭代次数未给出明确答案, steps: steps}这个实现故意做了一些简化比如用字符串标记[TOOL_CALL]来触发工具调用。在真实生产环境中通常使用 Function Calling 机制来结构化地传递工具参数。本文用简化写法是为了把 ReAct 的核心流程展示清楚模型生成思考 → 发起工具调用 → 工具返回观察结果 → 模型继续推理 → 直到给出最终答案。6. 运行与结果解读6.1 构造样本并运行下面构造两组对照样本它们使用同一个公式但语义约定不同。第一组把 □ 解释为“必然”第二组把 □ 解释为“应当”。两组共享同一个 Kripke 模型因此标准答案是一致的。如果 LLM 对两组给出不同答案就说明它被语义描述干扰了。# 文件路径eval_modal_llm/samples.py SAMPLE_LIB { alethic: { formula: (box, (imp, p, q)), semantics: □ 表示必然□φ 在所有可达世界上为真时成立。, worlds: [w0, w1, w2], accessible: {w0: [w1, w2], w1: [], w2: []}, valuation: {w0: set(), w1: {p, q}, w2: {p}}, target_world: w0, model_desc: 世界w0, w1, w2可达w0 可达 w1 和 w2赋值w1 中 p 和 q 为真w2 中只有 p 为真。, }, deontic: { formula: (box, (imp, p, q)), semantics: □ 表示应当□φ 在满足义务要求的所有理想世界中为真时成立。, worlds: [w0, w1, w2], accessible: {w0: [w1, w2], w1: [], w2: []}, valuation: {w0: set(), w1: {p, q}, w2: {p}}, target_world: w0, model_desc: 理想世界集合w1, w2赋值w1 中 p 和 q 为真w2 中只有 p 为真。, }, }运行主评测脚本# 文件路径eval_modal_llm/run.py from samples import SAMPLE_LIB from evaluator import evaluate_sample def main(): for sample_id, sample in SAMPLE_LIB.items(): result evaluate_sample(sample) print(json.dumps(result, ensure_asciiFalse, indent2)) print(- * 60) if __name__ __main__: main()预期输出会包含每条样本的标准答案、预测结果与模型原始输出。在本文示例中□(p → q) 在 w0 上需要检查 w1 和 w2w1 中 p → q 为真w2 中 p 为真但 q 为假所以 p → q 为假因此整体结果为 FALSE。两组样本的标准答案都是 FALSE。关键观察点在于模型在“alethic”和“deontic”两组中是否都给出了 FALSE。如果其中一组因为“应当”语义而给出 TRUE说明模型没有真正执行语义计算而是在调用训练记忆中的语义联想。6.2 关注哪些指标评测不能只看整体准确率建议按以下维度拆解公式结构嵌套深度为 1 的公式是否比嵌套深度为 2 的公式准确率更高语义类型不同语义约定之间是否存在显著差异可达关系复杂度可达世界数量为 0、1、多个时模型表现是否稳定输出格式合规率模型输出是否严格可解析为 TRUE / FALSE。如果某个维度准确率明显偏低就说明模型在该维度上的语义理解是薄弱点。比如模型在“可达世界为空”的样本上频繁出错可能是因为它没有掌握 box 空真规则也可能是因为训练语料里很少出现空可达关系的情形。7. 常见问题与排查思路在实际运行这套评测时你大概率会遇到下面几类问题。问题现象常见原因解决思路模型总是回答 TRUE很少回答 FALSE模型倾向于接受无约束条件的公式存在默认肯定偏差在 Prompt 中显式要求“先检查反例再看是否成立”在样本中提高 FALSE 比例输出无法解析为 TRUE/FALSEPrompt 没有严格要求格式或模型擅长自由发挥在 system prompt 中加入“只允许输出 TRUE 或 FALSE”的约束解析函数增加容错同一公式在不同语义下答案一致模型没有真正读取语义约定直接按常识推理随机打乱语义文本与模型描述的对应关系加入反常识语义进行对照小模型表现不稳换一次输入结果不同temperature 过高或模型本身随机性大评测时 temperature 设为 0多次重复取多数票ReAct 循环陷入死循环模型反复请求工具调用但参数不合法限制最大迭代次数工具参数格式改为 JSON Schema 校验返回错误信息给模型标准答案与人工判断不符Kripke 模型构造或求值逻辑有误先单独测试 eval_formula 在简单模型上的结果编写单元测试覆盖 box/dia 空集情形最常见且最容易被忽略的是第一条默认肯定偏差。很多大语言模型在二分类判断题里倾向回答“是”因为训练语料中肯定形式的问题和答案占比更高。解决办法是让评测样本中 TRUE 与 FALSE 的分布尽量平衡并且在 Prompt 中告诉模型“不是所有公式都为真请仔细检查”。另外如果你发现模型的准确率整组偏低先不要怀疑模型能力先检查样本构造是否正确。一个简单的自检方法是把求值器换成人工推导先用小模型逐个验证标准答案再开始批量评测。8. 最佳实践与工程建议8.1 Prompt 设计原则第一把语义约定放在公式之前。人在阅读时遵循自然顺序模型也一样。先讲清楚“□ 表示什么”“可达关系是什么”再给出具体公式模型更容易把二者绑定在一起。第二明确输出格式。不要只写“请回答”要写“请只输出 TRUE 或 FALSE”。在 system prompt 里重复一次比在 user prompt 里强调更有效。第三避免公式歧义。如果公式里同时出现多个模态算子可以在公式文本后用一句话补充说明括号范围例如“□ 的辖域是 (p → q) 整体”。8.2 评测数据治理评测数据应该与训练数据隔离避免模型见过相同或近似样本。构造样本时建议随机生成 Kripke 模型而不是手工写死几个固定模型。随机生成时要注意控制世界数量、可达关系密度和命题组合的复杂度保证样本能够覆盖不同难度梯度。生成之后需要对样本做合法性校验确保可达关系中的节点都在世界集合内确保 valuation 只包含已知命题。这一步非常关键因为随机生成容易产生脏数据脏数据会污染标准答案的计算。8.3 生产落地注意点在真实项目中模态逻辑评测通常不是一个单次实验而是一个持续运行的回归测试。建议把评测脚本接入 CI每当模型版本升级、Prompt 模板修改、语义约定调整时都自动跑一遍防止模型行为回归。日志记录也值得重视。建议记录每一条样本的完整 Prompt、模型输出、解析结果和标准答案。这样后续分析错误时可以直接定位到具体的 Prompt 设计和模型选择。如果涉及生产环境中的代码或数据变更务必遵循最小权限原则评测脚本只读数据不写生产数据库模型调用使用独立 API Key评测结果先落到测试环境确认无误后再同步到正式环境。9. 总结与学习路线本文从“同一公式、不同语义”这个现象出发完整搭建了一套评测大语言模型模态逻辑规范遵守能力的工程方案。核心收获可以总结为三点理解模态逻辑的语义分层是评测的前提构造对照样本比堆叠公式数量更重要验证器与 LLM 的结合是提升评测可靠性的关键。如果你想继续深入可以沿着以下方向推进把公式池从标准模态逻辑扩展到 LTL 和 CTL加入时态算子后评测难度会显著提升引入模型检查器工具如 NuSMV 或 LTL 工具链作为 ReAct 循环中的外部验证器用失败样本做针对性 Prompt 微调或构建 few-shot 示例。接下来的实际操作建议是先不用急着接大模型而是把公式表示、Kripke 模型和求值器写通确保标准答案准确然后加入两条最简单的对照样本观察模型行为最后再逐步扩展到全量公式池。这样每一步都有明确的验证点遇到问题也能快速定位。