🤖 AI

Neurosymbolic Auditing of Natural-Language Software Requirements

본 논문은 확률적 형식화 변이를 통해 모호성을 탐지하고 반례 유도 수정을 통해 일관성과 안전성을 검증하기 위해 대규모 언어 모델과 SMT 솔버를 활용하여 자연어 소프트웨어 요구사항을 감사하는 신경 기호 파이프라인인 VERIMED 를 소개하며, 이를 통해 의료기기 안전 요구사항의 정확성을 크게 향상시켰습니다.

원저자: Bethel Hall, William Eiers

게시일 2026-05-14

📖 4 분 읽기☕ 가벼운 읽기

CC BY 4.0

원저자: Bethel Hall, William Eiers

원본 논문은 CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/) 라이선스로 제공됩니다. ✨ 이것은 아래 논문에 대한 AI 생성 설명입니다. 저자가 작성하거나 승인한 것이 아닙니다. 기술적 정확성을 위해서는 원본 논문을 참조하세요. 전체 면책 조항 읽기

생명 구호 기계를 설계한다고 상상해 보세요. 환자의 혈액을 정화하는 투석기 같은 장치입니다. 이 기계가 어떻게 작동해야 하는지에 대한 규칙을 평이한 영어로 적어봅니다: "혈액 흐름이 멈추면 경보를 울려라."

문제는 인간의 언어가 messy(불편하고 복잡)하다는 점입니다. 단어는 모호할 수 있고, 문장은 서로 모순될 수 있으며, 아무도 눈치채지 못한 채 따라야 할 수 없는 규칙이 있을 수도 있습니다. 컴퓨터 프로그램이 이런 messy한 메모를 바탕으로 이 기계를 구축하려 한다면, 종이 위에서는 완벽해 보이지만 실제 생활에서는 실제로 위험한 무언가를 만들어낼 수 있습니다.

이 논문은 이러한 안전 규칙을 위한 슈퍼 감사자 역할을 하도록 설계된 새로운 '뉴로심볼릭'(neurosymbolic) 시스템인 VERIMED를 소개합니다. 이는 창의적인 AI 와 엄격한 논리 로봇이 팀을 이루는 것을 뜻하는 세련된 용어입니다.

다음은 일상적인 비유를 통해 설명한 VERIMED 의 작동 방식입니다:

1. 번역가와 논리 로봇

시스템은 두 부분으로 구성되어 있다고 생각하세요:

번역가 (LLM): 이 창의적인 AI 는 당신의 영어 규칙을 읽고, 컴퓨터가 검증할 수 있는 엄격한 수학적 언어 (SMT) 로 번역하려고 시도합니다.
논리 로봇 (SMT 솔버): 이는 논리적 타당성만 중시하는 강직하고 완고한 기계입니다. 이 로봇은 '감정'이나 '의도'에는 관심이 없으며, 규칙이 논리적으로 타당한지 여부만 중시합니다.

2. 규칙을 위한 '스트레스 테스트'

기계가 구축되기 전에 VERIMED 는 숨겨진 결함을 찾기 위해 번역된 규칙에 대해 네 가지 특정 테스트를 실행합니다:

'일어날 수 있는가?' 테스트 (공허성, Vacuousness): 규칙이 "기계가 물속에 잠기면 전원을 끄라"고 말한다고 가정해 보세요. 만약 기계가 절대 물속에 잠겨서는 안 된다면, 이 규칙은 쓸모없습니다. 논리 로봇은 이렇게 확인합니다: "기계가 실제로 물속에 잠길 수 있는가?" 만약 답이 "아니오"라면, 로봇은 그 규칙을 유령으로 표시합니다. 존재하지만 아무것도 하지 않는 것입니다.
'깨질 수 있는가?' 테스트 (위반 가능성, Violatability): 로봇은 규칙을 깨뜨리려 시도합니다. "규칙을 따르면서도 기계를 위험한 행동을 하게 만들 수 있는가?"라고 묻습니다. 안전을 위반할 방법을 찾으면, 그것은 "반례(counterexample)"로서 어떻게 깨뜨릴 수 있는지 정확히 보여줍니다. 예를 들어, "보라, 다이얼을 50 으로 설정하면 당신이 말했듯이 경보가 울리지 않는다"는 증명입니다.
'이중 장부' 테스트 (중복성, Redundancy): 때로는 정확히 같은 말을 하는 두 가지 규칙을 작성하기도 합니다. 하나는 "압력이 200 을 넘지 않도록 하라"고 하고, 다른 하나는 "압력이 200 을 넘지 않도록 하라"고 말합니다. 로봇은 이러한 중복을 찾아내고 "당신은 자신을 반복하고 있습니다. 둘 다 의도한 것인지, 아니면 그중 하나가 잘못된 것인지 확인해 보세요"라고 말합니다.
'전체적 조화' 테스트 (일관성, Consistency): 로봇이 모든 규칙이 서로 싸우고 있는지 확인합니다. 규칙 A 가 "펌프를 켜라"고 하고 규칙 B 가 "펌프는 꺼져 있어야 한다"고 하며, 둘 다 동시에 발생해야 한다면, 로봇은 "이건 불가능하다!"라고 외칩니다.

3. '모호성 탐지기'(마술)

이것이 이 논문의 가장 창의적인 아이디어입니다. 때로는 문장이 너무 모호해서 두 가지 다른 방식으로 해석될 수 있습니다.

비유: 셰프에게 "스테이크가 다 될 때까지 요리하라"고 말한다고 상상해 보세요. 셰프는 '다 됨'을 미디엄 레어로 생각할 수 있지만, 당신은 웰던을 의도했을 수 있습니다.
VERIMED 가 이를 포착하는 방법: AI 에게 규칙을 한 번 번역하라고 요청하는 대신, 같은 규칙을 다섯 번 번역하라고 요청합니다. 마치 다섯 명의 다른 셰프에게 '다 됨'을 해석하라고 요청하는 것과 같습니다.
- 만약 다섯 명의 셰프가 모두 정확히 같은 레시피를 적어내면, 규칙은 명확합니다.
- 만약 한 셰프는 '미디엄 레어'를, 다른 셰프는 '웰던'을 적어내면, 시스템은 이 불일치를 포착합니다. 그리고 인간에게 이렇게 말합니다: "이봐요, 당신의 규칙은 모호합니다! 당신의 문장이 해석될 수 있는 두 가지 다른 방법이 여기 있습니다. 명확히 해 주세요."

4. '수리 공장'

논리 로봇이 실수나 모호성을 발견하면 단순히 "오류"라고만 말하지 않습니다. 그것은 도움이 되는 정비공처럼 행동합니다:

깨진 논리의 경우: 규칙이 실패한 정확한 상황 (반례) 을 AI 에게 보여줍니다. AI 는 그 특정 구멍을 수정하기 위해 규칙을 다시 씁니다.
모호한 언어의 경우: 인간에게 혼란의 특정 지점 (예: "200 도는 포함되는가 제외되는가?") 을 보여줍니다. 인간이 명확히 하면, 시스템은 모두가 동의할 때까지 다시 번역합니다.

그들은 무엇을 발견했는가?

연구자들은 투석기에 대한 64 개의 안전 규칙 세트로 이를 테스트했습니다.

결과: 시스템은 2 개의 규칙이 중복 (복제) 이고 12 개의 규칙이 모호 (여러 방식으로 읽을 수 있음) 함을 발견했습니다.
수정: '반례' 피드백 (AI 에게 정확히 어떻게 실패했는지 보여주는 것) 을 사용했을 때, AI 의 안전 질문에 대한 답변 능력이 약 55% 의 정확도에서 거의 99% 로 급증했습니다.
모호성 수정: 시스템이 모호한 규칙을 표시하고 인간이 이를 명확히 한 후, AI 는 상충되는 번역을 더 이상 생성하지 않았습니다. '모호성'은 제로로 떨어졌습니다.

결론

VERIMED 는 안전망입니다. 이는 창의적인 AI 를 사용하여 인간의 규칙을 수학으로 번역하고, 엄격한 논리 로봇을 사용하여 해당 수학 규칙이 일관성 있고 모호하지 않으며 실제로 안전한지 확인합니다. 이는 코드가 작동하는지 확인하는 것을 넘어, 기계가 구축되기 전에 코드를 위한 지침이 타당한지 확인합니다.

중요한 참고 사항: 이 논문은 명시적으로 투석기 및 통증 관리 펌프와 같은 의료 기기 요구 사항에 대해 테스트했다고 밝힙니다. 저자들은 이 시스템이 요구 사항을 검토하기 위한 전문가용 도구일 뿐, 인간 전문가를 대체하는 것이 아니며 독립적인 인간 검토 없이 실제 생활에 사용되어서는 안 된다고 경고합니다.

기술 요약: 자연어 소프트웨어 요구사항의 신경심볼릭 감사

문제 정의

자연어 소프트웨어 요구사항은 특히 의료 기기 같은 안전-중요 분야에서 모호성, 불일치, 미명세로 인해 자주 고통받습니다. 이러한 결함은 형식 모델과 구현으로 전파되어 잘못된 명세의 검증이나 안전하지 않은 행동의 배포로 이어질 수 있으므로 위험합니다. 대규모 언어 모델 (LLM) 이 자연어를 기계 검증 가능 명세로 변환하는 자동형식화 분야를 발전시켰지만, 구문적 유효성만으로는 부족합니다. 잘 구성된 형식 명세라도 전역적 불일치를 포함하거나, 도달 불가능한 트리거 조건 (공허성) 을 포함하거나, 소스 텍스트의 여러 가능한 해석을 허용할 수 있습니다. 진실 형식화가 부재할 경우, LLM 이 종종 통계적으로 가장 일반적인 해석으로 기본화하거나 암묵적 제약을 생략하기 때문에 이러한 의미론적 실패를 감지할 오라클이 없습니다.

방법론: VERIMED 프레임워크

저자들은 자연어 요구사항을 통합된 SMT(이론 만족) 모델로 변환하고 솔버 쿼리를 활용하여 결함을 감지하도록 설계된 신경심볼릭 파이프라인인 VERIMED을 제안합니다. 이 프레임워크는 고정된 타입 상태 변수 (불리언 제어 상태 및 실수 값 매개변수) 와 도메인 제약 조건 스키마를 기반으로 작동합니다.

파이프라인은 네 단계로 구성됩니다:

모호성 해결기: 형식화 전에 각 요구사항이 안정성을 위해 검사됩니다. 시스템은 고온에서 LLM 에서 $N$ 개의 독립적인 형식화를 샘플링합니다. 그런 다음 인코딩 쌍 간에 양방향 SMT 동등성 검사를 수행합니다. 인코딩이 동등하지 않으면 요구사항이 모호성 민감도로 플래그됩니다. 솔버는 인코딩이 불일치하는 구체적인 "증거"(특정 상태) 를 생성하여 LLM 에게 피드백하고 모든 샘플이 단일 인코딩으로 수렴할 때까지 요구사항을 다시 작성하도록 합니다.
자동형식화기: 모호성이 제거된 요구사항은 단일 SMT-LIB 명세로 변환됩니다. 시스템은 솔버 오류 메시지가 LLM 을 안내하여 잘못된 코드를 재생성하여 유효한 모델을 생성할 때까지 유한한 구문 수정 루프를 사용합니다.
속성 검증기: 이 모듈은 조립된 모델 $M$ $M$ 에 대해 네 가지 특정 감사 쿼리를 실행합니다:
- 전역 일관성: $M$ 이 만족 가능한지 확인합니다. 만족 불가능하면 unsat 코어가 충돌하는 요구사항을 식별합니다.
- 공허성: 조건부 요구사항의 경우, 트리거 조건이 도메인 제약 하에서 만족될 수 있는지 확인합니다.
- 위반 가능성: 요구사항이 도메인 내에서 위반될 수 있는지 확인하며, 가능하면 구체적인 위반 할당을 반환합니다.
- 중복성: 요구사항이 명세의 나머지 부분에 의해 이미 강제되는지 확인합니다.
쿼리 검증기: 이 단계는 시나리오 기반 안전 질문을 검증합니다. 제안된 답변이 모델에 의해 함축되는지 확인합니다 ( $M \land s \land \neg a$ 가 만족 불가능한지). 위반이 발견되면 솔버는 반례를 반환합니다. 이 반례와 위반된 요구사항은 LLM 의 답변을 수정하기 위한 수정 루프에 대한 피드백으로 작용합니다.

주요 기여

본 논문은 다음과 같은 기여를 소개합니다:

신경심볼릭 프레임워크: VERIMED 은 자연어 요구사항을 단일 SMT 모델로 변환하고, 다운스트림 검토를 위한 주요 신호로 솔버 출력을 활용합니다.
요구사항 수준 SMT 감사: 저자들은 일관성, 공허성, 위반 가능성, 중복성이라는 네 가지 감사를 수립하여 확립된 품질 기준을 운영화합니다.
확률성을 통한 모호성 감지: 본 논문은 LLM 의 확률적 성질을 이용하여 모호성을 감지하는 방법을 소개합니다. 여러 형식화를 샘플링하고 양방향 SMT 부동등성을 검사함으로써 시스템은 여러 가능한 해석을 허용하는 요구사항을 플래그합니다. 솔버가 생성한 증거는 자연어 명확화를 주도합니다.
반례 유도 수정 (CEGR): 연구는 심볼릭 피드백의 세분성이 수정 효과에 상당한 영향을 미친다는 것을 보여줍니다.

실험 결과

이 프레임워크는 혈액 투석기 명세에서 추출한 64 개의 자연어 안전 요구사항 코퍼스에 대해 평가되었으며, PCA 펌프 명세에 대해 2 차 평가가 수행되었습니다.

자동형식화 및 감사: 시스템은 모든 64 개 요구사항에 대해 솔버 검사 가능한 SMT 모델을 성공적으로 생성했습니다. 모델은 전역적으로 일관성이 있으며 공허한 요구사항이 포함되지 않았습니다. 감사는 2 개의 요구사항 (3.1%) 을 중복으로 플래그했습니다. 순환 의미 동등성 (SMT 를 텍스트로 변환하고 다시 형식화) 은 100% 의 요구사항에서 달성되었으며, 원본과 재구성된 텍스트 간의 평균 코사인 유사도는 96.2% 였습니다.
변이 감지: 파이프라인은 네 가지 결함 카테고리 전반에 걸쳐 256 개의 변이된 요구사항 (오경보 억제 및 한계 위반과 같은 결함 표현) 의 97.3% 를 감지했습니다.
반례 유도 수정: 질문-답변 작업에서 구체적인 SMT 반례를 피드백 (CEGR) 으로 사용한 결과, 검증된 정확도가 기준선 (피드백 없음) 인 55.4% 에서 **98.5%**로 상승했습니다. 구체적인 반례 없이 위반된 요구사항만 제공하는 경우 정확도는 80.0% 였으며, 이는 구체적인 증거 상태가 수정을 위한 결정적 동인임을 보여줍니다.
모호성 해결: 모호성 해결기는 64 개 요구사항 중 12 개 (18.8%) 가 여러 다른 인코딩을 생성하는 것으로 플래그했습니다. SMT 유도 명확화 후, 플래그된 모든 요구사항은 단일 인코딩으로 수렴하여 (100% 쌍별 합의) 요구사항당 평균 다른 인코딩 수를 1.59 에서 1.00 으로 줄였습니다.

중요성 및 주장

본 논문은 VERIMED 가 SMT 기반 쿼리를 통해 소프트웨어 요구사항 감사를 성공적으로 운영화하여 자동형식화에서 의미론적 결함의 "보이지 않는" 특성을 해결했다고 주장합니다. 저자들은 다음과 같은 점을 강조합니다:

확률적 변이는 신호이다: 독립적인 형식화 간의 불일치는 소스 텍스트의 모호성에 대한 신뢰할 수 있는 지표입니다.
세분성이 중요하다: 심볼릭 피드백의 유용성은 그 구체성에 크게 의존합니다. 구체적인 반례는 추상적 요구사항 목록보다 수정에 훨씬 더 효과적입니다.
일관성만으로는 부족하다: 형식 모델의 내부 일관성은 결함 부재를 보장하지 않습니다. 행동 보존과 모호성 감지가 필수적인 보완책입니다.

저자들은 범위를 겸손하게 유지하며, 연구 결과가 주입 관련 의료 기기에 구체적이며 의도 충실도의 직접적 측정 대신 대리 신호 (일관성, 변이 민감도 등) 에 의존한다고 명시합니다. 또한 결과는 독립적인 전문가 검토 없이 안전-중요 응용 프로그램에 사용되어서는 안 되며, 현재 구현은 완전한 시간 논리를 지원하지 않고 현재 상태 조건을 통해 시간 요구사항을 근사화한다고 명시합니다.