Sheaf-Guarded Updates: Streaming Structural Verification for Evolving Agent State

Motivation

• Known: Sheaf neural network 및 sheaf-theoretic 방법들은 고정된 그래프 위에서 H0 기반 신호(예: Cheeger-type inequality, connection Laplacian)를 주로 활용해왔으며, Borkar의 stochastic approximation 프레임워크는 고정 토폴로지의 학습 시스템에 Lyapunov 안정성 분석을 적용해왔다.
• Gap: 기존 연구는 H1 이상의 고차 cohomology를 운용적 신호로 사용하지 않았고, 그래프 토폴로지 자체가 진화하는 상황에서의 Lyapunov 안정성 분석이나 update-time 구조 검증 비용을 로컬 편집 수로 억제하는 방법이 부재했으며, self-evolving agent의 최종 산출물이 아닌 내부 mutable state 자체의 coherence 검증도 다뤄지지 않았다.
• Why: 자율적으로 스스로를 수정하는 과학 에이전트가 대규모로 운영되려면, 각 local update가 전체 상태의 정합성을 깨뜨리는지 총 누적 상태 크기가 아니라 업데이트 지역성에 비례하는 비용으로 실시간 검증해야 하며, 이는 neural generation이 더 이상 병목이 아니고 state maintenance가 병목인 시대의 핵심 인프라 문제이다.
• Approach: 에이전트 상태를 cellular sheaf가 부착된 growing graph로 모델링하고, coboundary operator·H1 obstruction·Dirichlet energy·Laplacian spectral gap을 이용한 pre-commit 검증 계층과 density-aware governor, cellular decomposition 기반의 O(1) amortized 재계산 메커니즘을 결합한다.

Achievement

Coboundary norm distributions for 490 valid generaliza-

1. 조건부 Lyapunov 안정성 증명: edge-vertex ratio와 Laplacian spectral gap에 대해 Borkar stochastic approximation을 이용한 두 개의 conditional Lyapunov stability theorem과, near-identity sheaf에 대한 restricted stability corollary를 제시했다.
2. O(1) amortized 검증: bounded-cell 분해와 cached-assembly 가정 하에 cellular decomposition을 통해 편집당 재계산 비용을 O(1) amortized로 낮추고, V=5M vertex, 35 µs median per-edit latency, zero assembled-cohomology drift를 단일 상용 머신에서 달성했다.
3. ProofDAG 벤치마크에서 완전 분리: exact representation 하에서 F1=1.000, 14% relative noise 하에서도 F1≥0.94의 coboundary 기반 판별 성능을 보였다.
4. structural aliasing 규명: 990개 lemma·10개 수학 도메인에 걸친 live LLM 제안 연구를 통해 자연어 loading의 조악함이 valid/contradictory coboundary 분포를 겹치게 만드는 structural aliasing을 유발함을 보이고, loader fidelity가 자율 커밋 결정의 binding constraint임을 규명했다.
5. Lean/mathlib 검증: 507개 declaration, 954개 kernel-certified dependency edge, 6개 namespace group에서 exact-loader 경로가 zero clean residual(max 2.61×10⁻¹⁶)과 62개 controlled corruption 전량 탐지를 달성했다.

How

• 각 vertex에 stalk space F(v)=R^d(d=8)를 부여하고, 인접 edge에 restriction map ρ_{u→e}를 정의하여 coboundary operator δ0와 sheaf Laplacian L_F=δ0^⊤δ0를 구성
• Dirichlet energy E[s]=s^⊤ L_F s와 spectral gap λ2(L_F)를 이용해 restriction map 불일치를 정량화
• 모든 restriction map에 대해 σmax(ρ)≤ρmax인 bounded-gain 조건을 deterministic rescaling으로 강제하여 near-identity regime 확보
• density-aware governor가 edge-vertex ratio r(t)에 대한 penalty(w·max(0,(r−r)/r))로 restorative drift를 공급하고 Purity Gate가 CM<0인 경우 업데이트를 차단
• H1 obstruction, coboundary norm 등 구조적 신호를 이용해 실패를 국소화하고 commit/block/decompose를 결정하는 governor loop(Fig 1) 구성
• bounded-cell 가정 하에 cellular decomposition으로 cohomology 재계산을 국소화하여 O(1) amortized per-edit cost 달성
• ProofDAG(합성 controlled test), 990-lemma live LLM proposal study, Lean/mathlib 실제 커널 검증 데이터셋 세 가지로 실증 평가

Originality

• 기존 sheaf ML 연구가 고정 그래프의 H0 신호에 국한된 것과 달리, growing graph 위에서 H1 obstruction을 1차 피드백 신호로 사용한 최초의 시도
• 그래프 토폴로지 자체가 진화하는 상황에 Borkar stochastic approximation 기반 Lyapunov 분석을 확장 적용
• First & Kaufman(2024)의 arbitrary sheaf에 대한 no-universal-Cheeger 결과와 양립하는 near-identity regime에서의 restricted positive stability corollary 도출
• 최종 산출물(증명, 정리)이 아니라 에이전트의 mutable internal state 자체를 검증 대상으로 삼는 pre-commit layer라는 문제 설정 자체의 참신성
• structural aliasing 현상(자연어 loading에 의한 valid/contradictory 분포 중첩)을 실증적으로 규명하여 loader fidelity를 자율 커밋의 binding constraint로 명시

Limitation & Further Study

• 검증기는 represented structural coherence만 보장하며 semantic truth를 보장하지 않아, false statement가 이웃과 호환적으로 표현되면 zero coboundary로 통과할 수 있음
• 안정성 결과가 조건부(conditional) Lyapunov theorem으로, 명시된 update-policy 가정과 bounded-cell·cached-assembly 가정 하에서만 성립하여 일반성이 제한적
• 자연어 기반 loader의 구조적 정합성이 낮아 실제 LLM 제안 환경에서는 structural aliasing이 발생, exact-loader(Lean/mathlib) 환경에서만 완전한 성능이 확인됨 → 강건한 semantic loader 개발이 향후 과제
• 단일 상용 머신에서의 실험으로 분산/다중 에이전트 환경에서의 확장성 및 동시성 문제는 다루지 않음
• d=8 고정 stalk 차원, 특정 노이즈 모델(14% relative noise) 등 실험 설계의 일반화 가능성에 대한 추가 검증 필요

Evaluation

총평: Sheaf 이론을 growing graph 기반 에이전트 상태 검증에 창의적으로 결합하고 이론적 안정성 증명과 대규모 실증(5M vertex, Lean/mathlib 실증)을 모두 갖춘 견고한 연구이나, semantic truth와 structural coherence의 간극 및 loader fidelity 문제라는 실질적 한계를 스스로 명확히 드러낸 균형 잡힌 워크숍 논문이다.