본 논문은 신경망을 명시적 알고리즘으로 역설계하려는 메커니즘 해석 가능성과 재훈련 없이 특정 동작을 수정하려는 모델 편집을 다룬다. BlockCert라는 프레임워크를 통해 변환기 메커니즘의 인증된 블록별 추출을 소개하고, 가벼운 확장을 통해 인증된 로컬 편집을 지원하는 방법을 설명한다. 사전 훈련된 변환기와 프롬프트 분포를 기반으로 BlockCert는 잔여 블록에 대한 구조화된 대리 구현을 추출하고, 근사 오차를 제한하고, 커버리지 지표를 기록하며, 기본 아티팩트를 해싱하는 기계 확인 가능 인증서를 제공한다. Lean 4에서 간단한 Lipschitz 기반 구성 정리를 공식화하여 이러한 로컬 보장을 글로벌 편차 경계로 끌어올린다. GPT-2 small, TinyLlama-1.1B-Chat, Llama-3.2-3B 모델에 적용하여 높은 블록별 커버리지와 작은 잔여 오차를 얻었으며, TinyLlama에서 완전하게 스티치된 모델이 스트레스 프롬프트에서 기본 난이도와 약 6e-5 내로 일치함을 보여주었다.
