TensorRocq: Rocq 에서의 도식적 추론 활성화에 대한 기술적 요약

이 논문은 TensorRocq이라는 Rocq(구 Coq) 기반의 도구를 소개하며, 대칭 모노이드 범주 (Symmetric Monoidal Categories, SMCs) 에 대한 **도식적 추론 (Diagrammatic Reasoning)**을 검증된 형태로 가능하게 하는 방법을 제시합니다.

1. 문제 정의 (Problem)

대칭 모노이드 범주 (SMC) 는 회로, ZX-계산법, 선형 대수 등 다양한 계산 모델을 표현하는 강력한 프레임워크입니다. 종이 위에서는 **스트링 다이어그램 (String Diagram)**을 사용하여 연산의 병렬 및 직렬 구성을 직관적으로 표현하고, "연결성만 중요하다 (only connectivity matters)"는 원칙 하에 다이어그램을 변형하며 추론합니다.

그러나 Rocq 과 같은 증명 보조기 (Proof Assistant) 에서 SMC 를 다룰 때는 다음과 같은 심각한 문제가 발생합니다:

• 구문적 잡음 (Syntactic Noise): 증명 보조기 내부는 결합법칙 (Associativity) 이 명시적으로 정의된 귀납적 데이터 구조로 SMC 를 표현합니다. 따라서 연결성만 동일한 두 항이더라도 결합 순서가 다르면 구문적으로 다른 것으로 간주됩니다.
• 비효율적인 증명: 사용자는 다이어그램의 연결성을 이해하기 위해 결합법칙 관련 잡음을 수동으로 제거하거나, 원하는 서브다이어그램이 구문적으로 정확히 나타나도록 수많은 구조적 재작성 (Rewriting) 을 수행해야 합니다. 이는 실제 의미 있는 추론을 가리는 지루하고 취약한 과정을 만듭니다.
• 기존 도구의 한계: 기존 도구 (ViCAR, Chyp 등) 는 자동화를 제공하지만, 검증되지 않았거나 (Chyp), 구체적인 의미론 (Semantics) 을 가진 이론에 적용하기 어렵거나, Rocq 내부에서 완전히 통합되지 않았습니다.

2. 방법론 (Methodology)

TensorRocq 는 하이퍼그래프 (Hypergraphs), PROPs, 그리고 텐서 (Tensors) 간의 형식적 연결을 기반으로 합니다. 핵심 아이디어는 SMC 항을 하이퍼그래프로 변환하여 도식적 추론을 수행한 후, 다시 SMC 항으로 변환하는 것입니다.

2.1. 세 가지 핵심 구성 요소

1. 텐서 (Tensors): 하이퍼그래프와 SMC 항에 공통된 의미론적 기반을 제공합니다. 텐서는 선형 대수의 일반화로, 합성 (Contraction) 과 병렬 곱 (Product) 을 통해 SMC 의 직렬 및 병렬 구성을 자연스럽게 인코딩합니다.
2. 인터페이스가 있는 하이퍼그래프 (Hypergraphs with Interfaces): SMC 항을 구체적인 구문적 객체로 표현합니다. Bonchi 등의 연구를 확장하여, 입력/출력 인터페이스를 가진 방향성 하이퍼그래프로 정의합니다.
3. APROP (Autonomous PROPs): TensorRocq 의 구문적 인터페이스입니다. 생성자 (Generators) 와 연산 (합성, 스택, 캡/컵 등) 으로 정의되며, 하이퍼그래프와 텐서 의미론으로 변환 가능합니다.

2.2. 검증된 재작성 엔진 (Verified Rewrite Engine)

TensorRocq 의 핵심 작동 원리는 다음과 같습니다:

1. 변환 (Translation): Rocq 내의 SMC 항 (또는 APROP 항) 을 계산 가능한 하이퍼그래프로 변환합니다.
2. 동형성 검사 (Isomorphism Checking): 하이퍼그래프의 동형성 (Isomorphism) 을 검증된 알고리즘으로 확인합니다. 하이퍼그래프가 동형이면 텐서 의미론상 동일하므로, SMC 항도 동등합니다. 이는 "연결성만 중요하다"는 원칙을 자동화합니다.
3. 이중 푸시아웃 (Double Pushout, DPO) 재작성: 하이퍼그래프 수준에서 서브그래프 매칭을 수행하고, 검증된 규칙에 따라 서브그래프를 치환합니다.
4. 역변환 (Extraction): 재작성된 하이퍼그래프를 다시 APROP 항으로 변환하여 Rocq 증명에 사용합니다.

이 과정에서 반사 (Reflection) 기법을 사용하여, 검증된 알고리즘이 증명 생성을 담당하도록 하여 성능과 확장성을 확보했습니다.

2.3. 확장성: 인스턴스화 (Instantiation)

TensorRocq 는 새로운 SMC 이론을 정의하는 것뿐만 아니라, 기존 프로젝트 (예: VyZX) 에도 적용할 수 있도록 Typeclass 시스템을 제공합니다. 사용자는 대상 이론의 생성자와 의미론을 정의하고, APROP 과의 변환 (Quoting/Denoting) 을 구현하기만 하면, TensorRocq 의 재작성 전술 (Tactics) 을 해당 이론에 바로 적용할 수 있습니다.

3. 주요 기여 (Key Contributions)

• 검증된 도식적 재작성: Rocq 내에서 SMC 항에 대해 결합법칙을 자동으로 무시하고 연결성 기반으로 재작성할 수 있는 검증된 전술 (Tactics) 을 제공합니다.
• 하이퍼그래프 기반 의미론: 하이퍼그래프와 텐서를 연결하여, 도식적 추론의 정확성을 수학적으로 검증할 수 있는 프레임워크를 구축했습니다.
• Chyp 와 유사한 추상 이론 정의: 생성자와 관계 (Rules) 로 SMC 이론을 정의할 수 있는 Signature 구조를 제공하며, 이는 Chyp 와 유사한 추상적 추론을 Rocq 내에서 검증 가능하게 만듭니다.
• 기존 프로젝트 통합: VyZX (ZX-계산법 구현) 와 같은 기존 Rocq 라이브러리에 TensorRocq 전술을 통합하여, 기존 증명의 길이를 획기적으로 줄이고 가독성을 높였습니다.
• 성능 최적화: 하이퍼그래프 동형성 검사를 통해 대규모 목표에 대해서도 효율적으로 작동하도록 설계되었습니다.

4. 결과 (Results)

• 증명 길이 단축: VyZX 프로젝트의 CNOT 게이트와 스왑 연산에 대한 증명 사례에서, 기존 Rocq 증명은 결합법칙 처리를 위해 45 줄의 코드가 필요했으나, TensorRocq 를 사용하면 17 줄로 단축되었습니다.
• 가독성 및 견고성 향상: 증명 과정이 결합법칙의 잡음에서 벗어나 다이어그램의 구조적 변화에 집중하게 되어 가독성이 크게 향상되었습니다. 또한, 정의의 미세한 변경에 덜 민감해졌습니다.
• 성능: 실제 실험에서 하이퍼그래프 동형성 검사는 수백 개의 엣지를 가진 목표에서도 1 초 이내에 완료되어 실용성을 입증했습니다.

5. 의의 (Significance)

TensorRocq 는 종이 위 증명과 형식적 검증 사이의 간극을 해소합니다.

• 직관적 추론의 형식화: 연구자들이 종이 위와 마찬가지로 다이어그램을 변형하며 추론할 수 있게 하여, SMC 기반의 복잡한 시스템 (양자 컴퓨팅, 회로 설계 등) 에 대한 형식적 검증을 접근 가능하게 만듭니다.
• 검증된 자동화: 단순히 자동화 도구를 제공하는 것을 넘어, 그 자동화 과정 자체가 텐서 의미론을 통해 검증되므로, 어떤 이론에 적용하더라도 안전성이 보장됩니다.
• 생태계 확장: 선형 대수, 양자 컴퓨팅 등 다양한 분야에서 SMC 를 사용하는 프로젝트에 적용 가능한 범용 프레임워크를 제공함으로써, 형식적 방법론의 확산을 촉진합니다.

결론적으로, TensorRocq 는 Rocq 생태계에서 SMC 기반의 도식적 추론을 가능하게 하는 첫 번째 검증된 도구로서, 복잡한 수학적 구조에 대한 형식적 증명의 생산성과 신뢰성을 동시에 높이는 중요한 기여를 합니다.