자연어 소프트웨어 요구사항의 뉴로심볼릭 감사 (Neurosymbolic Auditing)

자연어 소프트웨어 요구사항은 종종 모호하고, 일관성이 없으며, 명세가 불충분합니다. 안전이 중요한 (safety-critical) 도메인에서 이러한 결함은 잘못된 명세를 검증하는 형식 모델 (formal models)로 전파되며, 안전하지 않은 동작을 배포하는 구현체로 이어집니다. 우리는 SMT solver가 장착된 대규모 언어 모델 (LLM)이 이러한 요구사항을 감사할 수 있음을 보여줍니다. 즉, 요구사항을 형식 논리 (formal logic)로 번역하고, 생성된 형식화 과정에서의 확률적 변동 (stochastic variation)을 통해 모호성을 탐지하며, 결과물인 명세에 대한 solver 쿼리를 통해 불일치, 공허함 (vacuousness), 그리고 안전 위반을 드러내는 방식입니다. 우리는 의료 기기 소프트웨어 요구사항을 위해 이 아이디어를 실행 가능한 형태로 구현한 뉴로심볼릭 (neurosymbolic) 파이프라인인 VERIMED를 제시하고 두 가지 발견 사항을 보고합니다. 첫째, 독립적인 형식화 과정 전반에 걸친 확률적 변동은 모호성의 신호입니다. 여러 가지 그럴듯한 해석을 허용하는 요구사항은 SMT적으로 동등하지 않은 (SMT-inequivalent) 형식화를 생성하며, 양방향 SMT 동등성 검사 (bidirectional SMT equivalence checking)는 이러한 불일치를 solver로 확인 가능한 테스트로 전환합니다. 둘째, 심볼릭 피드백 (symbolic feedback)의 유용성은 그 입도 (granularity)에 달려 있습니다. 혈액 투석 질의응답 벤치마크에서의 반례 유도 수정 (counterexample-guided repair)에서, 구체적인 SMT 반례 (counterexamples)는 검증된 정확도를 55.4%에서 98.5%로 높였습니다. 오픈 소스 혈액 투석 안전 요구사항에 대한 광범위한 실험적 평가를 통해, 우리는 VERIMED의 LLM 기반 접근 방식이 모호성에 민감한 요구사항을 성공적으로 줄이고 SMT 기반 쿼리를 통해 소프트웨어 요구사항의 엄격한 감사를 가능하게 함을 보여줍니다.