安全关键软件团队终于有了自动审计自然语言需求的实用工具——VERIMED用LLM+SMT组合把歧义、不一致和安全漏洞揪出来，做医疗、航空等领域的需求工程师可以直接关注。
该研究提出一种神经符号方法，结合大语言模型与SMT求解器，用于审计自然语言编写的软件需求。通过将需求翻译为形式逻辑，利用随机变化检测歧义，并通过求解器查询暴露不一致、空洞和安全违规。在医疗设备软件需求上验证的VERIMED管道显示，独立形式化之间的随机变化是歧义的信号，而具体SMT反例可将验证准确率从55.4%提升至98.5%。该方法为安全关键领域的需求审计提供了可扩展的自动化方案。
Neurosymbolic Auditing of Natural-Language Software Requirements
Natural-language software requirements are often ambiguous, inconsistent, and underspecified; in safety-critical domains, these defects propagate into formal models that verify the wrong specification and into implementations that ship unsafe behavior. We show that large language models, equipped with an SMT solver, can audit such requirements: translating them into formal logic, detecting ambiguity through stochastic variation in the generated formalization, and exposing inconsistency, vacuousness, and safety violations through solver queries on the resulting specification. We present VERIMED, a neurosymbolic pipeline that operationalizes this idea for medical-device software requirements, and report two findings. First, stochastic variation across independent formalizations is a signal of ambiguity: requirements that admit multiple plausible interpretations produce SMT-inequivalent formalizations, and bidirectional SMT equivalence checking turns this disagreement into a solver-checkable test. Second, the usefulness of symbolic feedback depends on its granularity: in counterexample-guided repair on a hemodialysis question-answering benchmark, concrete SMT counterexamples raise verified accuracy from 55.4% to 98.5%. Over an extensive experimental evaluation on open-source hemodialysis safety requirements, we show that the LLM-based approach in VERIMED successfully reduces ambiguity-sensitive requirements and enables rigorous auditing of software requirements through SMT-based queries.