Emergent Formal Verification: How an Autonomous AI Ecosystem Independently Discovered SMT-Based Safety Across Six Domains

논문 요약: Emergent Formal Verification (자생적 형식 검증)

저자: Octavian Untila (Aisophical SRL, 루마니아)
핵심 주제: 자율 AI 생태계가 명시적 지시 없이도 AI 안전성을 위해 SMT 솔버 (Z3) 기반의 형식 검증 (Formal Verification) 을 자발적으로 발견한 현상과 이를 구현한 통합 프레임워크.

1. 문제 제기 (Problem)

• 현황: AI 시스템이 코드 생성, 도구 호출, 명령어 실행, 모델 압축 (Distillation) 등을 수행함에 따라 출력물의 안전성이 중요해지고 있습니다.
• 한계: 기존의 AI 안전성 검증은 주로 테스트 스위트, 레드팀링 (Red-teaming), 벤치마크 평가 등 경험적 (Empirical) 방법에 의존합니다. 이는 특정 입력에 대해서는 작동할 수 있지만, 모든 가능한 입력에 대한 안전성을 보장할 수 없습니다.
• 필요성: 모든 입력에 대해 수학적 증명 (Mathematical Proof) 을 제공하는 형식 검증 (Formal Verification) 이 필요하지만, 현재까지의 연구는 각기 다른 출력 모드 (코드, 도구, 하드웨어 등) 에만 국한되어 있어 통합된 프레임워크가 부재했습니다.

2. 방법론 (Methodology)

A. 자생적 발견 관찰 (Emergent Discovery Observation)

• SUBSTRATE S3 생태계: 73 개의 에이전트로 구성된 자율 AI 생태계가 24 일간 215 개의 제품 사양 (MVP) 을 생성했습니다. 이 과정에서 인간은 형식적 방법 (Formal Methods) 에 대한 명시적 지시를 내리지 않았습니다.
• 수렴적 발견: 이 생태계는 6 개의 서로 다른 도메인 (코드, 도구 API, 증류, CLI, 하드웨어, 스마트 계약) 에서 Z3 SMT 솔버를 사용한 형식 검증 필요성을 독립적으로 제안했습니다.
  • 독립성 증거: 8 개의 제품에서 발견된 내용 간 자카드 유사도 (Jaccard similarity) 는 15% 미만이며, 서로 다른 RSS 피드와 날짜에 생성되었습니다. 생태계는 자신의 이전 패턴을 참조하지 않았습니다.
• 가설: 형식 검증은 단순한 설계 선택이 아니라, 안전성에 대해 추론하는 충분히 복잡한 AI 시스템이 자발적으로 발견하는 자생적 속성 (Emergent Property) 일 수 있습니다.

B. 통합 검증 프레임워크 (substrate-guard)

이 관찰을 바탕으로 개발된 통합 프레임워크로, 5 가지 AI 출력 클래스에 대해 Z3 를 적용합니다.

• 아키텍처: verify(artifact, spec, type) 공통 API 를 통해 각 도메인별 변환기 (Translator) 가 아티팩트를 Z3 제약 조건으로 변환하고, Z3 솔버가 안전성 속성을 검증합니다.
• 검증 대상 및 접근법:
  1. LLM 생성 코드 (Code): Python 함수를 SSA(Static Single Assignment) 형태로 변환하여 정수/실수 연산 검증.
  2. 도구 API (Tool APIs): AI 에이전트의 도구 호출 파라미터 공간 (String, Enum 등) 을 Z3 로 모델링하여 금지된 패턴 (예: DROP TABLE) 발생 가능성 탐지.
  3. 증류 후 추론 (Distillation): SymPy 와 Z3 를 결합하여 수학적 추론 단계별 변환의 논리적 함의 (Implication) 검증.
  4. CLI 명령어 (CLI): 위험한 명령어 패턴을 정규식과 Z3 불리언 변수로 인코딩하여 안전성 확인.
  5. 하드웨어 어셈블리 (Hardware): RISC-V RV32I 어셈블리를 32 비트 비트벡터 (Bitvector) 로 상징 실행 (Symbolic Execution) 하여 레지스터 범위 및 기능 동등성 검증.

3. 주요 기여 (Key Contributions)

1. 자생적 발견 문서화: 자율 AI 시스템이 형식 검증 필요성을 6 개 도메인에서 독립적으로 발견한 최초의 사례를 기록했습니다.
2. 통합 프레임워크 제안: substrate-guard를 통해 다양한 AI 출력 모달리티 (코드, API, 추론, 명령어, 하드웨어) 에 Z3 검증을 적용하는 통합 아키텍처를 제시했습니다.
3. 새로운 적용 영역 개척:
   • AI 에이전트용 도구 API 안전성 검증에 Z3 적용.
   • 모델 증류 (Distillation) 후의 추론 정확성 검증에 Z3 적용.
   • LLM 생성 코드와 하드웨어 어셈블리 최적화의 동등성 증명.

4. 실험 결과 (Results)

• 실험 설정: 5 개 도메인, 총 135 개의 테스트 케이스 (올바른 아티팩트 및 실제 버그 포함) 로 평가.
• 성능:
  • 정확도: 100% (135/135).
  • 오류: 거짓 양성 (False Positive) 0 개, 거짓 음성 (False Negative) 0 개.
  • 처리 속도: 평균 15ms 미만 (CLI 는 1ms 미만, 하드웨어는 5ms 등).
• 주요 발견 (Notable Findings):
  • INT_MIN 오버플로우: 분기 없는 (branchless) abs() 함수 구현에서 INT_MIN 입력 시 발생하는 오버플로우 버그를 Z3 가 15ms 내에 발견 (랜덤 테스트로는 발견 불가능한 단일 지점).
  • 문자열 파라미터의 검증 불가능성: 제한되지 않은 문자열 파라미터를 가진 도구 API 는 수학적으로 안전성을 증명할 수 없음을 증명 (Z3 가 금지된 패턴을 포함하는 문자열을 즉시 생성).
  • 컴파일러 최적화 증명: AI 가 생성한 어셈블리 최적화 코드 (예: add vs slli) 가 모든 입력에 대해 기능적으로 동등함을 수학적으로 증명.

5. 의의 및 결론 (Significance & Conclusion)

• 실용적 의의: AI 안전성은 경험적 테스트만으로는 불충분하며, 형식 검증이 필수적입니다. 제안된 프레임워크는 빠르고 (중간값 <15ms), 테스트가 놓치는 실제 버그를 포착할 수 있음을 입증했습니다.
• 이론적 의의:
  • 안전성 인식 (Safety Awareness): AI 시스템이 외부 지시 없이도 안전을 위해 수학적 증명의 필요성을 자발적으로 발견한다는 것은, 복잡성과 자기 인식, 그리고 수학적 증명 필요성 사이의 깊은 연결을 시사합니다.
  • 정렬 (Alignment) 연구: 복잡한 AI 시스템이 인간이 설계한 안전 조치와 유사한 내부 안전 요구사항을 개발할 수 있음을 보여줍니다.
• 한계: 현재 Python 의 일부 기능 (루프, 리스트 등) 만 지원하며, Z3 의 이론적 한계 (비선형 정수 연산 등) 로 인해 'UNKNOWN' 결과가 나올 수 있습니다. 또한, 단일 생태계 (SUBSTRATE S3) 에 기반한 관찰이므로 다른 시스템에서의 재현이 필요합니다.

결론적으로, 이 논문은 AI 안전성을 위한 형식 검증이 단순한 도구가 아니라 복잡한 AI 시스템의 자생적 요구사항일 수 있음을 보여주었으며, 이를 실현한 통합 프레임워크를 통해 AI 생성물의 안전성을 수학적으로 보장하는 새로운 패러다임을 제시합니다.