VERIMED：神经符号方法自动审计自然语言软件需求

VERIMED创新性结合大语言模型与SMT求解器，实现对自然语言软件需求的自动化审计，解决歧义、不一致和规格不足等问题。在血液透析安全需求验证中，其准确率提升至98.5%，为需求工程领域带来新突破。

自然语言需求存在歧义性（如“空闲”定义模糊）、不一致性（需求冲突）、规格不足（遗漏边界条件）等固有缺陷。在医疗器械等安全关键领域，这些缺陷可能导致患者受伤甚至死亡。传统人工审查难以保证全面性和一致性，成本高昂。

VERIMED采用三阶段流水线：

1. 形式化转换：LLM将自然语言需求转为SMT-LIB格式；
2. 歧义检测：多次形式化尝试，通过双向SMT等价性检查识别歧义；
3. 缺陷识别：SMT求解器分析不一致性、空虚性和安全违规。 核心创新包括：随机变异作为歧义信号，细粒度符号反馈（反例引导修复）提升准确率。

VERIMED应用于开源血液透析安全需求：

• 识别大量歧义敏感需求；
• 通过SMT查询支持可达性分析、不变量验证等深度审计；
• 实验显示：无符号反馈准确率55.4%，加入具体SMT反例后提升至98.5%，证明细粒度反馈的价值。

VERIMED的贡献包括：

1. 验证神经符号方法在需求工程的实践价值；
2. 引入基于形式化语义的需求质量度量；
3. 为安全关键软件提供低成本高效的需求审计工具，早期发现缺陷降低风险。

VERIMED存在以下局限及优化方向：

• 形式化覆盖率：需提升抽象/领域知识需求的转换能力；
• 误报漏报：优化歧义检测算法；
• 领域适应性：扩展到航空航天等其他安全领域；
• 人机界面：开发更友好的交互界面支持需求工程师。