LLM 파이프라인을 위한 증명 전달 인증서: 신뢰 경계 아키텍처

우리는 대규모 언어 모델 (LLM) 자체보다는 모델을 둘러싼 결정론적 구조적 계산 (deterministic structured computations)을 검증하기 위한 프레임워크를 제시하며, Lean 4 신뢰 경계 아키텍처 (trust-boundary architecture)를 현대적 LLM 파이프라인의 일반적인 인터페이스로 확장합니다. 인증서의 유효성은 Lean 4 커널 타입 체크 (kernel type-check)와 신뢰할 수 있는 집합 {propext, Classical.choice, Quot.sound}에 대한 'sorry'가 없는 전이적 공리 감사 (sorry-free transitive axiom audit)로 이루어집니다. 기타 가정들은 계층별(수학적 플레이스홀더, 암호학적 가정, ML/인간 오라클)로 선언되고 분할됩니다. 기술적 기여는 세 가지 로컬 인증서 제품군과 두 가지 연산자로 구성됩니다. 제품군은 충돌 인식 비라티스 그라운딩 (conflict-aware bilattice grounding, 방출 게이트 건전성 보조 정리 포함), 임베딩 민감도 및 패러프레이즈 안정성 (embedding sensitivity and paraphrase stability), 그리고 호어 스타일 에이전트 동작 (Hoare-style agent action)입니다. 연산자는 기권(abstention)을 감사 로그가 남은 드롭된 주장(dropped claims)을 포함하는 최대 가중 인증 가능 잔차 (Maximal Certifiable Residue)로 변환하는 연산자와, 레이어별 이득 및 마진으로부터 파이프라인 전체의 폐쇄형 섭동 예산 (closed-form pipeline-wide perturbation budget)을 산출하는 합성 안정성 (Compositional Stability) 정리입니다. 이 세 가지 제품군과 범용 보증 카드 통합기 (Universal Assurance Card consolidator)는 특허 및 법률 검색, 규제 금융, 임상 의사 결정 지원, 그리고 되돌릴 수 없는 부작용이 있는 에이전트 시스템과 같은 고위험 배포를 위한 호출당 산출물을 형성합니다. 컴파일된 Lean 4 참조 아티팩트 (Lean v4.30.0-rc2, Mathlib)는 22개의 모든 인증서 유형을 다루며, 46개의 커널 감사 선언 중 17개는 공리가 없고, 나머지는 신뢰 집합과 선언된 가정에만 의존하며, sorryAx 또는 Lean.ofReduceBool의 사용은 전혀 없습니다. 세 가지 제품군은 네 가지 등록된 파일럿을 통해 경험적으로 테스트되었습니다: 적대적으로 섭동된 HotpotQA에서의 비라티스 그라운딩, 단문 및 장문 설정에서의 임베딩 민감도, 그리고 적대적 프롬프트 주입 (adversarial prompt injection)이 있는 파일 시스템 샌드박스에서의 호어 스타일 에이전트 동작입니다.