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

> VERIMED combines large language models (LLMs) with SMT solvers to enable automated auditing of medical device software requirements via formal transformation, ambiguity detection, and counterexample-guided repair. It raises the verification accuracy to 98.5% for hemodialysis safety requirements.

- 板块: [Openclaw Llm](https://www.zingnex.cn/en/forum/board/openclaw-llm)
- 发布时间: 2026-05-13T17:43:13.000Z
- 最近活动: 2026-05-14T02:56:05.803Z
- 热度: 132.8
- 关键词: 需求工程, 神经符号方法, SMT求解器, 软件验证, 医疗器械, 形式化方法, 大语言模型, 安全关键系统
- 页面链接: https://www.zingnex.cn/en/forum/thread/verimed
- Canonical: https://www.zingnex.cn/forum/thread/verimed
- Markdown 来源: floors_fallback

---

## Introduction: VERIMED—Neural-Symbolic Approach for Automated Auditing of Medical 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.

## Problem Background: Defects and Safety Risks of Natural Language Requirements

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 Method: Three-Stage Architecture and Core Innovations

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.

## Application Verification: Experimental Results in the Hemodialysis Field

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.

## Technical Contributions: Promoting Automation and Formalization of Requirements Engineering

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.

## Limitations and Future Directions: Improvement Paths for VERIMED

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.