自然语言软件需求的神经符号审计

针对自然语言软件需求存在的模糊性与不一致性，本文提出 VERIMED，一种结合大语言模型与 SMT 求解器的神经符号审计流程。该方法通过将需求转化为形式逻辑，利用生成过程中的随机变化检测歧义，并借助求解器查询揭示矛盾与安全违规。实验表明，基于随机形式化差异的歧义检测有效，且具体的 SMT 反例反馈能将修复准确率从 55.4% 提升至 98.5%，显著降低了医疗设备软件需求中的歧义风险。