기술 요약: 중첩된 데이터 타입을 이용한 자동 추론

1. 문제 정의

SMT-LIB의 데이터 타입 이론은 리스트나 트리와 같은 데이터 구조를 인코딩하는 데 유용한 수단을 제공하며, 이는 소프트웨어 검증에 필수적입니다. 그러나 이 방식은 업데이트 연산자와 무작위 접근(random-access) 기능이 부족하여 표현력에 한계가 있습니다. 이를 해결하기 위해 데이터 타입과 배열 이론을 나이브하게 결합하려는 시도가 자주 이루어집니다.

본 연구에서 식별된 핵심 문제는 이러한 나이브한 결합이 **비표준 모델(non-standard models)**을 도입한다는 점입니다. 구체적으로, 데이터 타입의 값이 자기 자신을 포함할 수 없다는 순환 부재(acyclicity) 원칙이 배열이 관여할 때 우회됩니다. 즉, 데이터 타입 값이 배열의 요소로 나타날 수 있고, 그 배열이 다시 해당 데이터 타입 값의 필드가 되는 구조가 가능해집니다. 이는 사이클을 생성하지만, 표준적인 이론 결합 방식(Nelson-Oppen을 통한)은 이 사이클이 데이터 타입과 배열 구성 요소 사이에 "분리"되어 있기 때문에 이를 감지하지 못합니다. 이러한 비표준 모델은 검증에 사용되는 중첩 데이터 구조의 직관적인 의미론과 일치하지 않으므로 바람직하지 않습니다.

2. 방법론

저자들은 이러한 비표준 모델을 명시적으로 배제하는 중첩된 데이터 타입(nested datatypes) 이론을 제안합니다. 방법론은 이론의 공식적 정의와 환원(reduction)에 기반한 결정 절차라는 두 가지 주요 구성 요소로 이루어집니다.

2.1. 공식적 정의

이 이론은 데이터 타입과 배열의 표준 결합을 제한함으로써 정의됩니다.

• 정칙성(Well-foundedness): 저자들은 배열 소트(sorts)의 존재를 고려하여 정칙 소트(well-founded sorts)에 대한 새로운 정의(정의 10)를 도입합니다. 이는 배열 요소가 포함되더라도 데이터 타입의 재귀적 구조가 정칙성을 유지하도록 보장합니다.
• NDT 관계: 비표준 모델을 배제하기 위해, 저자들은 구조체 상의 관계 $\mathcal{R}_{\mathcal{A}}$를 정의합니다(정의 16). 이 관계는 항(term)을 그 하위 항들과 연결하고, 배열을 그 요소들과 연결합니다. 구조체가 유효한 NDT 구조로 간주되기 위해서는 이 관계가 정칙적이어야 합니다. 이는 데이터 타입 값이 배열을 통해 간접적으로 자기 자신을 참조하는 사이클을 효과적으로 차단합니다.

2.2. 결정 절차

본 논문은 중첩된 데이터 타입의 만족 가능성 문제를 데이터 타입, 배열, 그리고 해석되지 않은 함수(EUF)의 (나이브한) 결합 문제로 환원하는 결정 절차를 제시합니다. 절차는 다음과 같습니다.

1. 시그니처 변환(Signature Translation): 새로운 시그니처 $\Sigma_{\varphi}$를 구축합니다.

   • 배열 소트는 두 가지 구성 요소로 분리됩니다: 사이클 체크를 위한 데이터 타입 소트($\sigma^*$)와 표준 배열 추론을 위한 배열 소트($\sigma'$)입니다.
   • 데이터 타입 생성자들은 새로운 소트들을 대상으로 동작하도록 복사됩니다.
   • 배열을 유한한 튜플로 나타내기 위한 특수 생성자들이 도입되며, 이는 입력 공식에 존재하는 인덱스들에 의해 접근되는 요소들을 포착합니다.
   • 배열 소트 표현($\sigma'$)과 데이터 타입 소트 표현($\sigma^*$)을 연결하기 위해 해석되지 않은 함수($f_A, g_A$)가 추가됩니다.

2. 공식 변환(Formula Translation): 입력 공식 $\varphi$는 $\text{trFormula}(\varphi)$로 변환됩니다.

   • 표준 리터럴(예: $x = \text{select}(a, i)$)은 새로운 시그니처의 대응하는 항으로 매핑됩니다.
   • 보조 정리(Lemmas): 결정적으로, 변환 과정에는 원래 공식의 배열 연산과 새로운 시그니처의 튜플 기반 표현 사이의 대응 관계를 강제하는 보조 정리 세트 $L(\varphi)$가 추가됩니다. 이 보조 정리들은 "숨겨진 사이클"이 변환된 공식에서 드러나도록 보장합니다.

3. 해결(Solving): 결과물인 $\text{trFormula}(\varphi)$는 기존의 데이터 타입, 배열, EUF 결합을 처리할 수 있는 SMT 솔버(예: Nelson-Oppen 방식 활용)를 사용하여 만족 가능성을 확인합니다.

2.3. 정당성 및 결정 가능성

본 논문은 데이터 타입 이론이 공유된 소트들에 대해 안정적으로 무한하다는 가정하에, 변환이 만족 가능성을 보존함을 증명합니다(정리 31). 결과적으로, 중첩된 데이터 타입 이론은 결정 가능합니다(정리 32).

3. 주요 기여

본 논문은 세 가지 주요 기여를 합니다:

1. 이론 정의: 데이터 타입과 배열의 상호작용에서 발생하는 비표준 순환 모델을 방지하는 정밀한 중첩 데이터 타입 이론을 도입했습니다.
2. 결정 절차: 중첩된 데이터 타입 문제를 해석되지 않은 함수가 추가된 표준 이론 결합 문제로 변환하는 환원 기반 결정 절차를 제시했습니다.
3. 구현 및 평가: cvc5 SMT 솔버 내의 프로토타입 구현과 접근 방식의 효과성을 입증하는 경험적 평가를 수행했습니다.

4. 실험 결과

저자들은 두 가지 벤치마크 스위트를 통해 구현을 평가했습니다:

• 합성 벤치마크(Synthetic Benchmarks): 데이터 타입과 배열 사이의 다양한 크기의 사이클을 생성하도록 체계적으로 설계된 공식들입니다.
  • 불만족(unsatisfiable) 인스턴스(사이클 존재)의 경우, cvc5는 500개의 벤치마크를 모두 해결하여 Z3(평균 299.8개를 해결했으나, 표에 따르면 Z3가 해결한 총 인스턴스 수는 더 적음)를 능가했습니다.
  • 만족(satisfiable) 인스턴스(사이클 파괴)의 경우, cvc5는 50개 중 25개를 해결한 반면, Z3는 단 1개만을 해결했습니다.
• 실제 세계 벤치마크(Real-World Benchmarks): 스마트 계약의 지속성 데이터 구조를 모델링하기 위해 Move Prover 검증 도구를 사용하여 도출된 공식들입니다.
  • 두 솔버 모두 Move Prover 벤치마크를 빠르게 해결했습니다.
  • 만족 인스턴스에 대해 cvc5는 Z3와 대등하거나 약간 더 빠른 성능을 보였습니다.

5. 의의 및 주장

본 논문은 제안된 이론과 결정 절차가 데이터 타입과 배열의 결합에서 발생하는 비표준 모델 문제를 성공적으로 해결한다고 주장합니다. 이는 기존 솔버(예: Z3)가 암묵적으로 처리할 수는 있지만, 순환 부재에 대한 정밀한 이론적 정의나 보장된 정확성을 갖추지 못한 문제입니다.

저자들은 자신들의 접근 방식이 "유망함(promising)"을 밝히며, 실제 세계의 벤치마크에서 기존 솔루션들과 경쟁력이 있고, 사이클 탐지를 테스트하기 위해 설계된 합성 벤치마크에서는 더 우수함을 보여주었습니다. 저자들은 이 연구가 중첩된 데이터 구조가 흔히 사용되는 Move Prover의 요구사항에 의해 동기 부여되었음을 강조합니다.

논문은 현재의 작업이 배열의 특정 사례를 해결하고 있지만, 탐지되지 않은 사이클의 광범위한 문제는 다른 데이터 구조(시퀀스, 집합 등)에도 존재한다는 점을 언급하며 겸허하게 결론을 맺습니다. 저자들은 배열에 대한 자신들의 해결책이 나이브한 이론 결합 문제에 대한 더 일반적인 해결책의 기초가 될 수 있다고 제안합니다. 향후 과제로 증분형 해결(incremental solving) 및 한정사(quantifiers) 지원 확장을 꼽았습니다.