TorchLean — Lean 4에서 신경망 공식화하기

2026-06-03 · 2026-06-03_torchlean-formalizing-neural-networks-lean.md

#paper #formal-verification #neural-networks #lean #verified-ml #safety-critical

원문 출처

https://arxiv.org/abs/2602.22631

TorchLean: Formalizing Neural Networks in Lean

arXiv: 2602.22631v2 | 2026-05-24 | cs.MS

저자: Robert Joseph George, Jennifer Cruden, Will Adkisson, Xiangru Zhong, Huan Zhang, Anima Anandkumar 소속: Caltech, Washington University in St. Louis, UIUC

한 줄 요약

PyTorch로 학습한 신경망과 검증기가 분석하는 대상이 실제로 같은지 보장할 수 없는 "의미론적 갭(semantic gap)"을 해결하기 위해, 신경망의 정의·실행·검증을 Lean 4 정리 증명기 안에서 통합한 프레임워크.

핵심 내용

1. 해결하려는 문제: "의미론적 갭" 4가지

현재 ML 검증 파이프라인은 PyTorch → Export(ONNX/FX) → Verifier(CROWN 등)로 이어지는데, 각 경계에서 의미론이 달라질 수 있다:

Export drift: 트레이스 기반 export는 제어 흐름을 놓침. ONNX opset 버전마다 의미론 변화
부동소수점: 검증은 실수 산술로 가정하지만, 실제 배포는 IEEE-754 Float32 → 반올림, overflow, NaN
불완전한 인증: PINN 등에서는 함수값뿐만 아니라 미분값까지 검증해야 하는데, 현재 파이프라인은 이를 분리
의미론적 경계 버그: 텐서 shape, broadcasting, padding, attention mask 등 "평범한" 버그가 검증을 무력화

2. TorchLean의 핵심 설계

공유 IR(Shared IR): 모든 프로그램이 operator-tagged SSA/DAG computation graph로 컴파일. 실행, 자동미분, 검증이 모두 동일한 IR을 대상으로 함
PyTorch 스타일 API: Lean 4 안에서 tensor, layer, model, optimizer, training loop 정의 가능
다중 의미론 해석: 같은 IR을 exact real(증명용), Float32(실행용), interval/affine(검증용)로 해석
검증된 자동미분: Theorem 2.1 — backprop이 adjoint Fréchet derivative를 계산함을 Lean 정리로 증명
명시적 FFI 경계: CUDA, PyTorch, Arb/FLINT, Gymnasium 등은 "untrusted producer"로 취급. Lean이 체크하거나 명시적 가정으로 기록

3. 커버리지

지원하는 모델 계열: CNN, GPT-style attention/FlashAttention, Mamba/state-space, diffusion/sampling, FNO/PINN, PPO/RL, MAE/JEPA self-supervised. 36개 정리, 15개 Figure, 12개 Table 포함.

4. 실험 결과

VNN-COMP MNIST-FC: Lean-verified IBP 0/30, CROWN 6/30, α-CROWN(CUDA) 13/30 검증
Certified Robustness: sklearn digits classifier, 318/360 입력에서 ℓ∞ robustness 인증 (체크 시간: 0.032ms 평균)
Neural Controller: Lyapunov 안정성 검증. Lean에서 CROWN enclosure 계산 (1212s, IEEE32Exec)
PINN: viscous Burgers equation의 PDE residual을 Lean에서 검증
Semantic Bug Zoo: broadcasting 오류, causal-mask 누수, log-sum-exp overflow 등 3가지 의미론적 경계 버그 포착

5. 한계

검증된 fragment은 PyTorch/CUDA 전체 표면보다 작음. 새 operator 추가 필요
CUDA FFI는 Lean kernel 밖 → conformance testing에 의존
실행 속도가 PyTorch 대비 느림 (예: neural controller Stage 2에서 1212s vs 0.015s)

커뮤니티 반응 (Hacker News, 104pts, 20 comments)

주요 논의

FFT vs Attention vs 양자(westurner): "FFT가 self-attention을 대체할 수 있다면 Quantum Fourier Transform도 대체할 수 있는가?" → wasabi991011이 반박: "QFT는 양자 컴퓨터에서 실행하는 특별한 분해일 뿐. 고전 컴퓨터에서는 더 빠르지 않으며, LLM을 양자 컴퓨터에서 실행하는 것은 더 비쌈"

양자화 지원(measurablefunc): "다음 단계는 quantized arithmetic 지원" → woctordho: "SageAttention(int8 quantized attention)이 일부 모델에서는 작동하지만 다른 모델에서는 overflow로 검은 이미지 생성. formal verification으로 overflow 범위를 확인할 수 있으면 좋겠다"

관련 프로젝트(austinvhuang): "Junji Hashimoto의 Lean 기반 GPU 프로그래밍 라이브러리 Hesper도 흥미로움. WebGPU + 양자화된 transformer inference 포함"

수학 연구의 가치(godelski): "수학 연구가 무용하다는 믿음이 있음. 하지만 black box에 자부심만 가질 것이 아니라 더 깊은 질문이 있음"

총체적 느낌

학계/폼벌 메소드 커뮤니티에서는 긍정적 반응. "의미론적 갭" 문제 자체는 널리 인정받음. CUDA 검증 한계와 확장성은 현실적인 지적.

새로운 시각

1. "검증의 검증" 문제

이 논문의 가장 중요한 통찰은 "검증기가 검증하는 대상이 실제로 배포되는 모델과 같은가"라는 메타-문제 자체를 제기한다는 점. 기존 검증 연구는 verifier의 tightness나 확장성에 집중했지만, TorchLean은 "무엇을 검증하는가"라는 더 근본적인 질문으로 돌아감. 이는 의료 AI 검증에도 직접적으로 적용 가능한 관점 — 모델 export 과정에서 의미론이 달라진다면, 인증 받은 모델과 실제 임상에서 돌아가는 모델이 다를 수 있음.

2. Lean의 "PyTorch화" 시도

논문 마지막에서 "Verified ML도 PyTorch가 empirical ML에 제공한 것과 같은 공유 인프라가 필요하다"고 명시. Lean ecosystem(mathlib, CSLib)이 수학/CS에 제공한 것을 ML 검증에도 확장하겠다는 비전. 이는 단순한 도구 개발을 넘어 "폼벌 ML의 표준 라이브러리"를 만들겠다는 선언.

3. 의료 AI 검증 파이프라인에의 시사점

의료 AI(특히 영상 진단)는 이미 ONNX export → 검증 → 인증의 파이프라인을 따르는데, 이 논문은 그 파이프라인의 각 경계가 "의미론적 드리프트"를 유발할 수 있음을 체계적으로 보여줌. 의료 AI의 경우:

전처리(pixels → tensor)의 의미론이 export에서 달라질 수 있음
Float32 → Float16/bfloat16 변환이 검증 결과를 무효화할 수 있음
attention mask, padding convention이 진단 모델에서 "평범한" 버그가 치명적일 수 있음

자녀/미래 영향

아인, 석현, 은한에게 관련될 분야

AI 안전성/검증 엔지니어: 이 분야가 성장하면 "모델을 학습하는 사람"과 "모델이 안전함을 증명하는 사람"이 분리되는 직무가 생김. 수학+CS 배경이 필요한 하이브리드 역할

의료 AI 규제: FDA/EMA가 AI 의료기기를 승인할 때 "formal verification certificate"를 요구할 가능성. 이 논문이 그 인프라의 일부가 될 수 있음 — 부모님이 일하는 내시경 AI도 언젠가 이런 검증 파이프라인을 통과해야 할 것

양자 컴퓨팅 vs 고전 ML: HN 댓글에서 논의된 QFT vs attention 문제는 아직 실험 단계. 하지만 "양자 ML"이 실제 영향력을 발휘하려면 formal semantics가 먼저 정의되어야 함 — TorchLean이 그 기반이 될 수 있음

교육적 관점: "수학이 무용하다"는 인식을 깨는 사례. Lean + mathlib 생태계가 성장하면, 고등학교/대학에서 "증명 보조기"를 수학 교육의 일부로 다룰 가능성도 있음

평가

장점:

명확한 문제 정의 (의미론적 갭의 4가지 실패 모드)
포괄적인 범위 (vision → transformer → diffusion → RL → scientific ML)
Lean theorem prover의 신뢰성 있는 검증
실제 실험 + semantic bug zoo로 실용성 입증
저자 라인업 (Anima Anandkumar 등)이 학계 영향력 보장

주의점:

아직 "연구용 프레임워크" — production ML 파이프라인에 바로 적용하기에는 early stage
CUDA 검증이 FFI 경계 밖 → 완전한 formal guarantee 아님
실행 속도가 PyTorch 대비 느림