VERIMED: Neural-Symbolic Approach for Automated Auditing of Natural Language Software Requirements

VERIMED innovatively combines large language models (LLMs) with SMT solvers to realize automated auditing of natural language software requirements, addressing issues such as ambiguity, inconsistency, and insufficient specifications. In the verification of hemodialysis safety requirements, its accuracy has been raised to 98.5%, bringing a new breakthrough to the field of requirements engineering.

Natural language requirements have inherent defects such as ambiguity (e.g., vague definition of "idle"), inconsistency (conflicting requirements), and insufficient specifications (missing boundary conditions). In safety-critical fields like medical devices, these defects may lead to patient injury or even death. Traditional manual reviews struggle to ensure comprehensiveness and consistency, and are costly.

VERIMED uses a three-stage pipeline:

1. Formal Transformation: LLMs convert natural language requirements into SMT-LIB format;
2. Ambiguity Detection: Multiple formalization attempts, identifying ambiguity via bidirectional SMT equivalence checks;
3. Defect Identification: SMT solvers analyze inconsistencies, vacuity, and safety violations. Core innovations include: using random mutations as ambiguity signals, and fine-grained symbolic feedback (counterexample-guided repair) to improve accuracy.

VERIMED was applied to open-source hemodialysis safety requirements:

• Identified a large number of ambiguity-sensitive requirements;
• Supported in-depth auditing such as reachability analysis and invariant verification via SMT queries;
• Experiments showed: accuracy was 55.4% without symbolic feedback, and increased to 98.5% after adding specific SMT counterexamples, proving the value of fine-grained feedback.

VERIMED's contributions include:

1. Verifying the practical value of neural-symbolic methods in requirements engineering;
2. Introducing requirements quality metrics based on formal semantics;
3. Providing a low-cost and efficient requirement auditing tool for safety-critical software, enabling early defect detection to reduce risks.

VERIMED has the following limitations and optimization directions:

• Formal Coverage: Need to improve the conversion capability for abstract/domain knowledge requirements;
• False Positives and Negatives: Optimize ambiguity detection algorithms;
• Domain Adaptability: Expand to other safety-critical fields such as aerospace;
• Human-Machine Interface: Develop more user-friendly interactive interfaces to support requirements engineers.