TorchLean 소개
신경망이 자율주행, 제어, 과학 계산처럼 한 번의 실수가 물리적 또는 사회적 비용으로 이어지는 시스템에 점점 더 깊이 들어가면서, 머신러닝 커뮤니티는 단순한 경험적 정확도(empirical accuracy)를 넘어선 보증(guarantee)을 요구하기 시작했습니다. 입력 섭동에 대한 강건성(robustness), 안전 및 안정성 제약의 충족, 신경망 출력값에 대한 보수적 경계(conservative bound) 같은 것들입니다. 이런 요구는 활발한 검증(verification) 생태계를 낳았지만, 정작 실제로 실행되는 신경망 과 분석 대상이 되는 산출물 이 서로 다른 객체라는 근본적인 문제는 거의 해결되지 못했습니다.
TorchLean 은 lean-dojo 팀(Robert Joseph George, Anima Anandkumar 등)이 공개한, 신경망을 형식화(formalize)하고 실행하며 검증하는 과정을 모두 Lean 4 안에서 하나로 통합한 프레임워크입니다. 이 논문은 "실행되는 모델과 검증되는 모델 사이의 의미적 격차(semantic gap)를 어떻게 없앨 것인가" 라는 문제를, 학습된 모델을 실행 가능한 프로그램 인 동시에 수학적 대상 으로 다루고 계산, 검증, 정리 증명(theorem proving)에 대해 공유된 의미론(shared semantics)을 부여하는 방식으로 풀어냅니다. 관련 논문 TorchLean: Formalizing Neural Networks in Lean (arXiv:2602.22631)은 55쪽 분량으로, 수학 소프트웨어(cs.MS) 분류로 공개되어 있습니다.
검증과 실행이 분리되면 무슨 일이 벌어지는가
문제의 핵심은 검증기의 성능이 아니라, 검증되는 산출물이 무엇을 의미하는가 입니다. 학습된 신경망 하나는 PyTorch nn.Module, 내보내진(export) ONNX 또는 FX 그래프, 컴파일러 IR, CUDA 기반 런타임 연산, 외부 CROWN 증명서(certificate), 논문 속 수학적 대상 등 여러 모습으로 나타납니다. 이들은 익스포터, 그래프 재작성(graph rewrite), 스칼라 의미론, 레이아웃 관례, 런타임 라이브러리로 연결되어 있는데, 이 경계가 명시되지 않으면 어떤 객체에 대해 증명한 속성이 실제 배포된 다른 객체에서는 성립하지 않는 상황이 생깁니다. 논문은 네 가지 구체적인 실패 양상(failure mode)을 지적합니다.
첫째, 내보내기 경계가 의미론적 표류(semantic drift)를 만듭니다. 학습된 모델은 프로그램이지만 검증기는 보통 TorchScript, ONNX, FX 같은 내보내진 대체물(surrogate)을 소비합니다. 트레이스 기반 내보내기는 제어 흐름이나 동적 동작을 놓칠 수 있고, 성공하더라도 특정 실행에서 수행된 연산만 반영한 그래프가 나올 수 있습니다. 게다가 교환 포맷은 연산자 집합(opset)을 버전 관리하므로, 내보내진 신경망의 의미가 도구, 버전, 백엔드 가정과 얽혀 런타임마다 달라질 수 있습니다.
둘째, 부동소수점 의미론이 이상화된 보증을 무효화할 수 있습니다. 대부분의 검증 기법은 실수(real) 산술이나 단순화된 수치 모델 위에서 기술되지만, 실제 배포는 반올림, 오버플로, 언더플로, NaN, 무한대, 부호 있는 0, 혼합 정밀도를 포함하는 IEEE-754 산술을 씁니다. 선행 연구들은 이 수치 오차가 강건성 주장을 반박하는 데 악용될 수 있음 을, 그리고 실수 모델에 대한 이론적 건전성(soundness)이 배포된 부동소수점 신경망의 실용적 건전성을 자동으로 보장하지 않음을 보였습니다.
셋째, 인증이 실제 실행 워크플로까지 도달하지 못하는 경우가 많습니다. 특히 제어와 자율 시스템의 학습 기반 구성요소에서는 검증이 실제 구현된 산출물과 연결되어야 하며, 물리 정보 신경망(Physics-Informed Neural Network, PINN)처럼 자동 미분으로 편미분방정식(PDE) 잔차를 강제하는 경우에는 증명서가 함수값뿐 아니라 도함수까지 포괄해야 합니다.
넷째, 실제 ML 버그는 의미론적 경계에 산다는 점입니다. 딥러닝 버그에 대한 실증 연구들은 많은 실패가 이국적인 증명 코너 케이스가 아니라 잘못된 텐서 형태(shape), 의도치 않은 브로드캐스팅, dtype 변환, 레이아웃 가정, 패딩 관례, 마스킹 실수 같은 평범한 의미론적 경계 오류 임을 보여줍니다. 이런 버그가 위험한 이유는, 표면적 호환성은 유지하면서 실제로 검사되는 속성만 바꿔버리기 때문입니다. "잘못된 패딩 관례에 대한 강건성 증명서도 여전히 증명서이지만, 의도한 계산에 대한 것은 아닙니다."
기존 신경망 검증 접근법과 그 한계
신경망 검증 분야는 크게 두 갈래로 발전해 왔습니다.
접근법 1: 솔버 기반(solver-based) 방법. Reluplex와 Marabou 처럼 검증 질의를 만족성(SMT) 또는 제약 충족 문제로 환원합니다. 조각별 선형(piecewise-linear) 신경망에 강력하지만, 보통 내보내진 산출물(ONNX/TorchScript/맞춤 IR)을 입력으로 받기 때문에 내보내기와 해석 단계에서 추가적인 신뢰 경계(trust boundary)를 떠안습니다.
접근법 2: 추상 해석 및 완화(relaxation) 방법. 구간 경계 전파(Interval Bound Propagation, IBP)나 CROWN/LiRPA, DeepPoly 같은 선형 경계 전파 기법은 경계 전파로 인증된 포위(enclosure)를 계산하여 확장성이 좋습니다. \alpha-CROWN 은 완화 파라미터를 최적화해 경계를 조이고, \beta-CROWN 은 분기 한정(branch-and-bound)을 결합해 더욱 조입니다. 그러나 이들 역시 대개 내보내진 그래프 위에서 동작하므로, 검증된 객체가 실행된 객체와 같다는 보장 은 파이프라인 밖에 남습니다.
이 두 갈래는 VNN-COMP(국제 신경망 검증 대회)에서 표준화되고 검증되어 왔으며, 각 인스턴스가 ONNX 신경망과 VNN-LIB 속성 명세의 쌍으로 포장되는 관례가 자리 잡았습니다. 바로 이 내보내기와 인터페이스 경계 가 문제의 진원지입니다.
TorchLean의 발상 전환: 단일 의미론 목표
기존 파이프라인이 "PyTorch → 내보내기 → ONNX → 검증기" 로 이어지며 각 변환 단계마다 표류 위험을 누적한다면, TorchLean 은 신경망 정의 자체를 유일한 의미론적 기준점(semantic reference point)으로 삼고 실행과 검증이 모두 같은 의미를 가리키게 합니다. 모델은 공유된 연산자 태그 SSA/DAG 계산 그래프 IR(operator-tagged SSA/DAG computation-graph IR)로 낮춰지며(lower), 이 그래프가 (i) 학습 및 추론, (ii) 검증된 역방향 자동 미분, (iii) Lean 기반 경계 전파 및 증명서 검사의 공통 목표가 됩니다.
여기서 외부 검증기는 신뢰받는 권위자가 아니라 선택적 생산자(producer) 입니다. 외부 도구의 출력은 그 자체로 보증으로 인정되지 않고, Lean 이 소비하는 그래프 의미론에 대해 검사되는 증명서 로 해석됩니다. 이 설계가 신뢰 계산 기반(Trusted Computing Base, TCB)을 작게 유지하는 핵심입니다. 마치 "화가가 그림을 그릴 때 여러 장의 스케치를 따로 그리는 대신, 하나의 캔버스 위에서 밑그림과 채색을 모두 진행하는 것" 과 같습니다. 실행하는 그림과 검증하는 그림이 물리적으로 같은 캔버스 위에 있으니, 둘 사이에 격차가 생길 여지가 사라집니다.
핵심 기여
논문이 제시하는 기여는 다음 다섯 가지입니다.
- Lean 안에서의 PyTorch 스타일 신경망 프로그래밍. 텐서, 레이어, 모델, 목적 함수, 옵티마이저, 데이터 로더, 다중 에폭 학습 루프를 정의하는 Lean 기반 API 를 제공합니다. eager 실행과 공유 IR 로 낮추는 컴파일 모드를 모두 지원하며, CUDA 기반 커널은 명시적 FFI 경계를 통해 노출됩니다.
- 실행, 미분, 검증을 위한 공유 IR. 지원되는 프로그램을 연산자 태그 SSA/DAG 계산 그래프로 컴파일하고, 같은 그래프 객체를 실행기, 역방향 자동 미분, IBP/CROWN 경계 전파, 증명서 검사가 함께 사용합니다. 지원 단편(fragment)에 대해 그래프 파라미터적 역방향 미분 정리(graph-parametric reverse-mode theorem)를 증명합니다.
- 명시적 스칼라 및 유한 정밀도 의미론. 같은 정의를 증명용 정확(exact) 실수, 실행용 유한 정밀도 스칼라, 경계용 구간/아핀 도메인에서 동일하게 해석합니다.
- 공유 의미론 위에서의 검증과 증명서 검사. 공유 IR 위에서 IBP, CROWN/LiRPA 아핀 완화, 증명서 검사를 구현합니다. 외부 산출물은 선언만으로 보증으로 받아들여지지 않고 그래프 의미론에 대해 검사됩니다.
- 현대적 ML 워크플로와 의미론적 버그 검사. 비전, GPT 스타일 어텐션, FlashAttention, Mamba/상태공간 모델, 확산 및 샘플링, FNO/PINN 과학 ML, PPO/Gymnasium 롤아웃, 마르코프 결정 과정(MDP), MAE/JEPA 자기지도 목적 함수, PyTorch 왕복, 그리고 의미론적 경계 버그를 모은 bug zoo 까지 포함합니다.
공유 계산 그래프 IR: 모든 것의 의미론적 기준점
현대 ML 시스템은 보통 모델을 계산 그래프(computation graph) 로 표현합니다. 노드는 MatMul, Conv, ReLU 같은 원시 연산이고, 엣지는 그 사이를 흐르는 텐서입니다. TorchLean 의 IR 은 여기에 두 가지 규율을 더합니다. 첫째, 각 노드는 자신이 무엇을 의미하는지 알려주는 명시적 연산자 태그(operator tag) 를 형태 메타데이터와 함께 지닙니다. 따라서 실행과 검증이 외부 프레임워크에서 물려받은 암묵적 관례가 아니라 같은 원시 의미론 으로 노드를 해석합니다. 둘째, 그래프는 정적 단일 할당(Static Single Assignment, SSA) 형태로 저장되어 모든 중간값이 정확히 한 번만 정의됩니다. 이는 데이터 흐름 추론을 단순하게 만들고 노드 리스트에 대한 귀납(induction)을 가능하게 합니다.
수학적으로, 스칼라 의미론 \alpha 와 형태 s 에 대해 \mathrm{Tensor}_{\alpha}(s) 를 형태 s 의 텐서로 쓰면, 각 연산자 태그 \tau 는 타입이 있는 시그니처와 함께 다음과 같은 표시(denotation)를 가집니다.
잘 타입된 SSA/DAG 그래프 G 는 노드를 위상 순서(topological order)로 평가하여 얻어지는 함수 [\![G]\!]_{\alpha} 를 표시하며, 표시는 전역적(total)이고 결정적(deterministic)입니다. 결정적으로, 하나의 동일한 구문(syntax)을 여러 도메인에서 해석할 수 있다는 것이 TorchLean 의 가장 중요한 발상입니다.
즉 같은 모델이 증명을 위한 정확 실수, 실행을 위한 유한 정밀도, 검증을 위한 구간 및 아핀 완화로 해석되더라도 가리키는 수학적 대상은 하나 입니다. 어텐션과 FlashAttention 같은 융합 연산자조차 마스크가 포함된 마스크 스케일드 닷프로덕트 어텐션과의 동치(equivalence)로 명세됩니다.
여기서 마스크 M 은 형식 연산자 의미론의 일부입니다. 즉 "인과 마스크를 깜빡했다" 같은 실수가 비공식 관례가 아니라 타입과 의미론의 문제로 드러납니다.
TorchLean의 구조: 세 계층, 하나의 의미론
TorchLean 은 명세(Specification), 런타임(Runtime), 검증(Verification)의 세 계층으로 이루어지며, 세 계층 모두 위의 단일 IR 을 공유합니다.
명세 계층: 형태를 타입에 새기다
주류 ML 프레임워크는 텐서 형태를 동적으로 다루기 때문에, 형태 불일치가 런타임 예외나 미묘한 의미 버그로 뒤늦게 드러납니다. 실증 연구에 따르면 텐서 형태 결함(tensor shape fault)은 가장 흔한 딥러닝 버그 부류 중 하나입니다. TorchLean 은 형태 제약을 텐서의 타입 의 일부로 만들어, 형태가 맞지 않는 프로그램은 아예 표현 불가능(unrepresentable)하게 합니다. 많은 배관(plumbing) 오류가 테스트 단계가 아니라 타입 검사 단계에서 잡힙니다.
텐서는 스칼라 도메인 \alpha 와 형태 s 로 색인되는 전역 색인 함수(total index function) 로 표현됩니다. 형태는 귀납적 트리이며, 다음과 같은 동일성이 성립합니다.
이 함수적 관점은 증명에 매우 유리합니다. 텐서 연산이 형태에 대한 재귀로 정의되고, 외연적 동등성(extensional equality)이 텐서 동등성을 점별(pointwise) 동등성으로 환원하기 때문입니다. 중요한 점은 브로드캐스팅이 조용한 런타임 관례가 아니라 자체 타이핑과 의미 보조정리를 가진 명시적 형태 변환 이라는 것입니다.
각 레이어는 텐서 공간 사이의 타입 있는 사상(morphism) L : \mathrm{Tensor}_{\alpha}(s_{\mathrm{in}}) \to \mathrm{Tensor}_{\alpha}(s_{\mathrm{out}}) 으로 표현되므로, 신경망 합성은 PyTorch 의 nn.Module 합성과 닮았지만 형태 계약(shape contract)이 타입 검사기에 의해 강제됩니다. 예를 들어 가중치 W 와 편향 b 를 가진 선형 레이어는
로 표시되며, 이 단 하나의 정의 가 증명용 \mathbb{R}, 실행용 Float32, 검증용 구간/아핀 도메인에서 그대로 재사용됩니다. SGD 나 Adam 처럼 반복적 함수 갱신이 긴 클로저 사슬을 만들 수 있으므로, TorchLean 은 같은 외연적 의미를 가지면서 더 빠른 배열 기반 정규형으로 텐서를 재구축하는 물질화(materialization) 를 제공합니다.
런타임 계층: 두 실행 모드, 하나의 의미론적 목표
런타임 계층은 증명 수준 정의를 실제로 돌아가는 학습 및 추론과 연결합니다. 사용자 워크플로는 PyTorch 와 똑같습니다. 모듈을 정의하고, 순전파를 돌리고, backward 를 호출하고, 파라미터를 갱신합니다. 차이는 실행이 검증기 의미론 목표를 중심으로 조직 된다는 점입니다.
open TorchLean
def model := sequential [linear 2 1, relu]
런타임은 고립된 순전파뿐 아니라 CSV/NPY 로더, 미니배치 로더, JSON 학습 로그, 파라미터 import/export, 체크포인트, 그리고 SGD, 모멘텀, Adagrad, RMSProp, Adam, AdamW, Adadelta 옵티마이저를 갖춘 재사용 가능한 ML 인프라를 포함합니다. 학습 루프는 익숙한 수학적 형태 \theta_{t+1} = \mathrm{Opt}(\theta_t, \nabla_\theta L(\theta_t; B_t), s_t) 를 따르되, 같은 파라미터와 손실 그래프, 그래디언트 계산이 나중에 비공식 내보내기 경로를 거치지 않고 검증기 IR 로 그대로 낮춰질 수 있다는 점이 다릅니다.
핵심은 두 실행 모드가 하나의 의미론적 목표를 공유 한다는 것입니다. eager 모드는 연산을 즉시 실행하며 테이프(tape)를 기록하고, 컴파일 모드는 같은 프로그램을 공유 SSA/DAG IR 로 낮춰 그 그래프를 평가합니다. 이 컴파일은 torch.compile 식 커널 최적화가 아니라, 정리와 검사기가 소비할 그래프 객체를 만들어내는 의미론적 역할 을 합니다. 프로그램 p 를 낮추면 그래프 G 와 파라미터 저장소 P_{\theta} 가 나오고, 지원되는 순전파 단편에 대해 \mathrm{eval}_{\mathrm{src}}(p,\theta,x) = [\![G]\!]_{\alpha}(P_{\theta}, x) 가 성립합니다. 이것이 PyTorch 스타일로 개발하면서도 그래프 산출물의 속성을 증명하게 해주는 의미론적 다리 입니다.
역방향 자동 미분은 그래프 수준에서 단 한 번 증명됩니다. 출력 코탄젠트(cotangent) \bar{y} 에 대해 역전파는 수반(adjoint) 도함수를 계산합니다.
연산적으로는 역위상 순회로 구현되며, 값이 여러 다운스트림 노드에 소비되면 코탄젠트를 합산(accumulate) 하는 것이 본질입니다. 그래프 정리는 원시 연산자별 국소 도함수 정확성 보조정리를 합성하여 따라옵니다.
정리 2.1 (역방향 AD 정확성). \mathbb{R} 위의 잘 타입된 SSA/DAG 계산 그래프 G 가 국소 도함수 정확성 가정
GraphFDerivCorrect G를 만족하면, 임의의 입력 x 와 코탄젠트 seed 에 대해 \mathrm{bp}_G(x, seed) = \big(D(\mathrm{evalVec}\,G)(x)\big)^{\top} seed 가 성립한다.
ReLU 의 0 지점처럼 매끄럽지 않은 원시 연산에 대해서는 명시적 부수 조건 아래 점별 변형 GraphFDerivCorrectAt 을 쓰며, 꺾임점(kink)에서의 실행 관례는 결정적입니다. 또한 분류 손실이나 임베딩 모델을 위해, 라벨이나 토큰 ID 같은 비미분 정수 데이터는 별도의 색인 채널로 분리됩니다. 그래디언트는 임베딩 테이블 같은 부동소수점 값으로는 흐르지만 정수 선택자로는 흐르지 않아, 혼합 dtype 미분 그래프를 피하면서도 정수 라벨 교차 엔트로피나 임베딩 조회 같은 패턴을 지원합니다.
성능을 위한 CUDA 경로는 Lean 의 외부 함수 인터페이스(FFI)를 통해 선택적으로 제공됩니다. 중요한 설계 원칙은 CUDA 가 두 번째 의미론이 아니라 실행 백엔드 라는 점입니다. 네이티브 커널은 Lean 정리도 아니고 Lean 의 신뢰 커널의 일부도 아니며, 각 네이티브 호출은 의미가 이미 공유 의미론으로 주어진 연산자 태그 \tau 에 결부됩니다. 의도된 정합성 진술은 형태, dtype, 레이아웃, 반올림 모드, 축약 순서, 결정성에 대한 명시적 사전 조건 아래의 \mathrm{native}_{\tau}(x) \approx [\![\tau]\!]_{\texttt{Float32}}(x) 이며, 이 일치가 증명이 아니라 테스트로 확인될 때는 런타임 정합성 가정(runtime conformance assumption) 으로 기록됩니다. PyTorch state-dict import/export, Gymnasium 브리지, PPO 롤아웃, Arb/FLINT 수치 오라클 같은 상호운용(interop)도 모두 같은 규율을 따릅니다. 외부 도구는 가중치, 트레이스, 후보 경계를 생산 하고, Lean 은 속성을 지닌 산출물을 검사 하거나 명명된 가정으로 기록합니다.
부동소수점 의미론: 신뢰 경계를 일급 시민으로
많은 검증 주장은 반올림, 오버플로/언더플로, NaN/Inf 전파, 부호 있는 0, 비결합성(non-associativity), 혼합 정밀도 같은 미묘한 수치 동작에 좌우됩니다. 그런데 Lean 의 내장 런타임 부동소수점 타입은 커널에 불투명(opaque) 해서, 추가 가정 없이는 커널이 부동소수점 값을 계산하거나 추론할 수 없습니다. 그래서 TorchLean 은 빠른 실행과 증명된 의미론을 분리하고, 신뢰 경계를 명시적으로 드러냅니다. 같은 모델을 역할이 다른 여러 스칼라 도메인에 인스턴스화하는 방식입니다.
| 모드 | 용도 | 의미론과 신뢰 |
|---|---|---|
| \mathbb{R} | 증명, 기준 Autograd | 정확한 실수 산술. 정리 진술의 기준 의미론 |
| Interval / Affine | IBP, CROWN/LiRPA 경계 | 건전한 포위 도메인, 전이 규칙 증명 |
| FP32 / NF | 반올림 인식 정리 | round-on-\mathbb{R} 증명 모델, 합성 가능한 오차 봉투 |
| IEEE32Exec | 실행 가능 Float32 모델 | Lean 정의 binary32 비트 수준 의미론 |
| Arb/FLINT 오라클 | 엄밀한 초월함수 | 외부 검증된 구간 포위, 커널 밖 오라클 경계 |
| Lean Float32 | 빠른 실행 | 커널에 불투명한 런타임 구현. 배포 가정 또는 검증된 백엔드 |
| CUDA/네이티브 FFI | 가속 예제 | 선택적 FFI 실행. 네이티브 원시 일치 계약의 지배를 받음 |
실행용 Float32 로는 부호 있는 0, 비정규수(subnormal), NaN/Inf, 반올림 동작을 포함하는 IEEE-754 binary32 의 비트 수준 모델 IEEE32Exec 를 Lean 으로 정의해 제공합니다. 동시에 각 원시 연산을 "\mathbb{R} 에서 계산한 뒤 반올림" 으로 명세하고 그 오차를 그래프 전체에 걸쳐 경계 짓고 합성하는 보조정리를 갖춘 증명 수준 round-on-\mathbb{R} 모델(FP32/NF)도 함께 둡니다. 이는 Coq 의 Flocq 같은 검증된 부동소수점 라이브러리의 정신을 따른 것입니다. 나아가 NaN/Inf 와 오버플로를 제외한 유한 실행에서 IEEE32Exec 가 FP32/NF 모델로 내부적으로 정제(internal refinement) 됨을 연산자별로 증명합니다.
검증 계층: 검증기는 주장이 아니라 메커니즘이다
검증은 의미론에 대한 진술입니다. 검증 계층은 강건성 마진, 출력 경계, 불변성 및 안전 제약, 랴푸노프(Lyapunov)/배리어 부등식, PINN 잔차 경계, ODE 회랑(corridor) 조건 등의 목표를 컴파일된 그래프의 표시 [\![G]\!] 에 대한 Lean 정리로 표현합니다. 검증기는 주장이 아니라, 중간 경계나 완화, 증인을 생산하는 메커니즘 이며, 그 산출물은 검사된 뒤 [\![G]\!] 의 의미론적 속성을 입증하는 데 쓰입니다.
경계는 구체화 사상(concretization) \gamma 를 가진 추상 도메인 \mathcal{D} 에 살며, 연산자 \tau 의 국소 추상 변환기 \widehat{\tau} 는 다음을 만족할 때 건전합니다.
전체 그래프의 건전성은 [\![G]\!] 를 정의하는 바로 그 위상 노드 순서에 대한 귀납으로 따라옵니다. TorchLean 은 노드별 포위 [l_i, u_i] 를 전진 전파하는 건전한 IBP 코어를 갖추고, 그 위에 구간이 놓치는 상관관계를 잡아 훨씬 조밀한 출력 경계를 주는 CROWN/LiRPA 아핀 전파를 구현합니다. 두 방법 모두 외부 검증기 측 모델이 아니라 같은 IR 표시에 고정 됩니다.
더 강한 조임이 필요할 때 TorchLean 은 증명서/검사기 구조 를 채택합니다. 외부 솔버는 산출물의 생산자 역할을 하고, Lean 은 정리를 결론짓는 데 필요한 유한 데이터만 검사합니다. 의도된 정리 형태는 다음과 같습니다.
이 방식으로 \alpha/\beta-CROWN 증명서 방언(dialect)을 지원합니다. 증명서는 IBP 사전 활성화 박스, 노드별 아핀 경계, 불안정 ReLU 하한 완화를 위한 \alpha 파라미터, 그리고 활성/비활성 제약을 인코딩하는 선택적 \beta 위상 벡터를 공급하며, 검사기는 같은 노드별 단계 의미론을 Lean 에서 재생(replay)하여 제공된 경계가 재계산된 의무와 일치할 때만 받아들입니다. 외부 산출물을 선언만으로 신뢰하지 않고 검사하므로, 신뢰 계산 기반이 Lean 검사기와 IR 표시 라는 작은 핵심으로 줄어듭니다.
TorchLean의 구성 요소와 저장소 구조
TorchLean 은 사람들이 이미 쓰는 소프트웨어와, 그들이 신뢰하고자 하는 증명 산출물 사이에 자리합니다. 모델 코드를 읽기 쉽게 만드는 곳에서는 PyTorch 스타일 표면(surface)을 쓰고, 그 아래에서는 Lean 검사기가 들여다볼 수 있는 형태로 모든 것을 낮춥니다. 저장소는 역할별 디렉토리로 나뉘어 있어 어떤 부분이 명세 이고 어떤 부분이 실행 이며 어떤 부분이 증명 인지 구조 자체로 드러납니다.
- 모델, 텐서, 데이터, 학습 워크플로의 공개 facade 인
NN/API - 수학적 정의를 담은
NN/Spec - 실행 가능한 autograd, 옵티마이저, 학습 루프, CUDA 경계, PyTorch import/export 를 담은
NN/Runtime - 그래프 IR 과 의미론을 담은
NN/IR - 텐서 대수, autograd 정합성, 해석적 도함수 증명을 담은
NN/Proofs - 유한 정밀도 모델과 IEEE 스타일 실행 의미론을 담은
NN/Floats - 증명서 검사기와 CLI 워크플로를 담은
NN/Verification
실험 및 평가 결과
저자들은 TorchLean 을 의미론적 ML 시스템 스택 으로 평가합니다. 목표는 특화된 학습 프레임워크나 솔버 최적화된 검증기를 성능으로 능가하는 것이 아니라, 학습되고 미분되고 경계 지어지고 검사되고 가속되는 대상을 의미론적으로 가시화 하는 것입니다.
현대적 ML 워크플로 커버리지
TorchLean 은 장난감 검증기 신경망이 아니라 알아볼 수 있는 현대적 ML 프로그램을 지원합니다. 예제들은 미니배치 로더, 다중 에폭, 옵티마이저 상태, 저장된 파라미터, 손실 곡선, 샘플링 루프, 롤아웃 텐서, 임포트된 가중치, 생성된 증명서 같은 평범한 ML 구조를 실행합니다. CNN 이나 FNO 예제는 텐서 형태와 합성곱/스펙트럼 연산자, 유한 정밀도 실행을 강조하고, GPT 스타일 모델은 토큰화와 인과 마스킹, 어텐션 의미론을, Mamba/상태공간 예제는 재귀와 스캔 실행, 비예측(non-anticipation)을 강조합니다. 확산과 자기지도 예제는 마스킹, 뷰(view), 스케줄, 잠재 변수를, RL 예제는 롤아웃과 이득(return), 어드밴티지(advantage), 정책/가치 산출물과 시뮬레이터 경계를 다룹니다.
VNN-COMP 스타일 강건성 검증
MNIST-FC 슬라이스에 대한 VNN-COMP 스타일 미니 스위트에서, 완전히 Lean 으로 검사된 결과와 CUDA 기반 생산자 결과를 같은 벤치마크에서 비교합니다. 검사된(Checked) 행은 공유 IR 에 대한 Lean 검증 주장이고, CUDA 행은 NVIDIA A100 의 \alpha-CROWN GPU 생산자가 더 강한 후보 경계를 생성하되, 그 결과는 Lean 검사기가 재생할 때만 신뢰받는 TorchLean 주장이 됩니다.
| 경로 | 방법 | Safe/n | 시간 |
|---|---|---|---|
| Lean | IBP | 0/30 | 6.05s |
| Lean | CROWN-Obj | 6/30 | 22.60s |
| Lean | CROWN+\alpha | 6/30 | 14.21s |
| CPU 생산자 | \alpha-CROWN | 13/30 | 8.39s |
| CUDA 생산자 | \alpha-CROWN | 13/30 | 7.67s |
이 표는 검증의 강도와 신뢰의 위치가 별개 임을 잘 보여줍니다. GPU 생산자가 가장 많은 13/30 을 안전으로 판정하지만, 그 판정이 형식 보증이 되려면 Lean 검사기를 통과해야 합니다.
세 가지 사례 연구: 강건성, 제어, 과학 ML
인증된 강건성. 숫자 분류기(sklearn digits, 8\times8 \to 64 특징, 64 \to 10, \varepsilon = 0.02 )에 대해 \ell_{\infty} 마진 조건을 인증합니다. 모델은 349/360 입력에서 명목상 정확하고, 내보내진 경계 산출물을 재생하며 표준 로짓 마진 부등식을 검증하는 Lean 검사기에 의해 318/360 에서 강건함이 인증됩니다. 검사기는 예제당 평균 0.032 ms 로 가볍지만, 요점은 경쟁력이 아니라 강건성이 검사된 그래프에 결부 된다는 데 있습니다.
신경망 컨트롤러. 외부 학습이 신경 피드백 컨트롤러 u(x) 와 랴푸노프 후보 V(x) 를 제안하면, Lean 이 입력 영역에 대해 랴푸노프 부등식의 CROWN/LiRPA 포위를 검사하여 영역 기반 안전/안정성을 인증하는 2단계 워크플로입니다. 검증된 autograd 로 \nabla V 를 계산해 \dot{V}(x) = \nabla V(x) \cdot f(x, u(x)) 를 영역에서 경계 짓습니다. 흥미로운 비교가 드러나는데, Stage 2 를 PyTorch Float32 로 돌리면 \approx 0.015 초에 9/10 양성 손실 후보가 나오는 반면, TorchLean 이 명시적 IEEE-754 Float32 의미론(IEEE32Exec)으로 돌리면 \approx 1212 초가 걸리고 7/10 양성이 나옵니다. 속도는 크게 느리지만, TorchLean 은 추가로 스칼라 손실에 대한 네이티브 CROWN 포위(예: 상한 \approx 0.1869 )를 계산합니다. 이는 명시적 수치 의미론과 형식 경계를 얻는 대가로 치르는 비용 을 솔직하게 보여줍니다.
PINN 잔차 경계. 점성 버거스 방정식 u_t + u\,u_x - \nu u_{xx} = 0 을 만족하도록 학습된 물리 정보 신경망을 완전히 검증합니다. Python 에서 PINN 을 학습한 뒤 가중치를 JSON 으로 내보내 Lean 에 적재하고, IBP/CROWN 으로 u(x) 의 경계를, 전용 1차/2차 도함수 경계 전파 패스로 u'(x) 와 u''(x) 의 구간 포위를 같은 연산자 태그 그래프 위에서 계산합니다. 이 경계들을 결합해 PDE 잔차 |\mathcal{R}(u_\theta)(x)| 가 검증 지점에서 허용 오차 \varepsilon 안에 있음을 인증합니다.
의미론적 버그 탐지
논문은 세 가지 대표적 의미론 경계 실패를 보여줍니다. 첫째는 형태/브로드캐스팅 버그 입니다. 편향 b \in \mathbb{R}^C 를 로짓 X \in \mathbb{R}^{B \times C} 에 Y_{ij} = X_{ij} + b_j 로 더해야 하지만, 잘못된 브로드캐스트 축은 그럴듯한 텐서를 만들면서도 함수를 조용히 바꿔버립니다. 둘째는 시간적 버그 로, 잘못된 인과 마스크나 오래된 KV 캐시 항목이 미래 토큰 정보를 현재 출력에 흘려보낼 수 있습니다. 셋째는 수치 버그 로, 순진한 log-sum-exp 나 log-softmax 계산이 Float32 에서 오버플로하는 반면 안정적 형식은 유한하게 유지됩니다. 이 예제들은 작게 설계되었지만, 모델이 실행되고 내보내지고 심지어 그럴듯한 다운스트림 산출물을 만들어내는 동안에도 의도한 의미론이 이미 바뀌어 있는 바로 그 종류의 오류를 분리해 보여줍니다.
설치 및 첫 실행
TorchLean 은 lean-toolchain 으로 고정되어 있으며, 공개 시점 기준 leanprover/lean4:v4.29.0 으로 빌드됩니다. 저장소를 받아 빌드한 뒤 예제 데이터로 MLP 를 학습해볼 수 있습니다.
git clone https://github.com/lean-dojo/TorchLean.git
cd TorchLean
lake build
python3 scripts/datasets/download_example_data.py --auto-mpg
lake exe torchlean mlp --cpu --steps 10
lake exe torchlean mlp --steps 10 --dtype float --backend eager
# CUDA 툴킷과 NVIDIA GPU 가 있으면 GPU 경로도 시험할 수 있습니다(스모크 테스트용):
lake build -K cuda=true
lake exe -K cuda=true torchlean mlp --cuda --fast-kernels --steps 1000
첫 번째 MLP 명령은 실행 가능한 IEEE 스타일 Float32 경로를 사용하고, 두 번째는 Lean 내장 Float 런타임 경로를 사용합니다. CUDA 명령은 네이티브 GPU 런타임 경로를 쓰며, 신뢰할 수 있는 증명 경계가 아니라 빠른 스모크 테스트 용도라고 저자들은 명시합니다. TorchLean 을 다른 Lean 프로젝트에서 의존성으로 가져다 쓸 수도 있습니다.
require TorchLean from git "https://github.com/lean-dojo/TorchLean.git" @ "main"
대부분의 다운스트림 모델/학습 파일은 공개 facade 인 import NN.API.Public 에서 시작하고, 명세, IR, 증명, 검증, 예제까지 포함하는 더 넓은 묶음이 필요하면 import NN.Library 를 사용합니다. TorchLean 은 MIT 라이선스로 공개되어 개인 및 상업적 목적으로 자유롭게 쓸 수 있습니다.
한계점 및 향후 방향
저자들은 한계를 솔직하게 밝힙니다.
커버리지와 정합성. 검증된 단편은 PyTorch, CUDA, 현대 ML 라이브러리의 전체 표면보다 필연적으로 작습니다. TorchLean 을 확장하려면 새 원시 연산마다 연산자 의미론, 국소 도함수 규칙, 추상 변환기, 유한 정밀도 모델, 증명서 검사기를 추가해야 합니다.
Float32 신뢰 경계(하드웨어 격차). 실수 기준 의미론, 증명 수준 round-on-\mathbb{R} 모델(FP32/NF), 실행 가능한 비트 수준 Float32 커널(IEEE32Exec)을 분리했지만, 배포된 Float32 툴체인에서 실행 모델로의 표적별 정제 가 남습니다. 즉 반올림 모드, 비정규수 정책, 축약 순서 같은 배포 구성을 고정하고 정합성 인터페이스를 증명 또는 검증으로 해소해야 합니다.
배포와 코드 생성. Lean 안에서는 IR 을 단일 의미론 목표로 삼아 학습과 검증의 격차를 닫았지만, 검증된 모델을 임베디드 타깃에 배포하려면 IR 인터프리터를 기기에서 돌리거나 IR 에서 C/Rust 코드를 생성해 그 동작을 Lean 표시와 다시 연결하는 번역 단계가 필요합니다.
이런 한계는 의도적입니다. 시스템은 암묵적 신뢰보다 명시적 경계 를 택했으며, 형식 보증은 언제나 Lean 검사기가 실제로 검증한 것 에서만 나옵니다.
결론 및 의의
TorchLean 은 검증 가능한 머신러닝(verified machine learning)에 대한 의미론적 접근을 진전시킵니다. 모델은 실행 가능한 신경망 프로그램으로 작성되고, 공유 연산자 태그 SSA/DAG IR 로 낮춰지며, 실행, 자동 미분, 경계 전파, 증명서 검사가 모두 같은 형식 의미론 을 통해 해석됩니다. 이로써 강건성, 제어 지향 안전성, 과학 ML 잔차, VNN 스타일 임포트 산출물, 의미론적 회귀 테스트에 대한 기계 검증된 주장을, 비공식 내보내기 파이프라인에 의존하지 않고 세울 수 있습니다.
이 접근의 더 넓은 가치는 여러 커뮤니티에게 공유할 수 있는 하나의 의미론적 대상 을 준다는 데 있습니다. 검증 연구자는 실행 가능한 모델에 대해 증명서를 검사하고, ML 시스템 연구자는 내보내기와 컴파일, 수치, 백엔드 경계를 형식 계약으로 연구하며, 과학 ML과 제어, 로보틱스 연구자는 학습된 구성요소를 잔차나 안전, 안정성 주장에 연결할 수 있습니다. "검증 가능한 ML 에도 PyTorch 가 경험적 ML 에 제공했던 것과 같은 공유 인프라가 필요합니다." mathlib 이 Lean 에서 수학에 대해 그 역할을 해냈듯, TorchLean 은 신경망 계산과 형식 의미론, 증명서 기반 검증을 하나의 정리 증명 환경 안에서 연결하며 그 방향으로 한 걸음을 내딛습니다.
TorchLean 공식 홈페이지
TorchLean 가이드 문서
TorchLean 논문
TorchLean 프로젝트 GitHub 저장소
이 글은 GPT 모델로 정리한 글을 바탕으로 한 것으로, 원문의 내용 또는 의도와 다르게 정리된 내용이 있을 수 있습니다. 관심있는 내용이시라면 원문도 함께 참고해주세요! 읽으시면서 어색하거나 잘못된 내용을 발견하시면 덧글로 알려주시기를 부탁드립니다. 
파이토치 한국 사용자 모임
이 정리한 이 글이 유용하셨나요? 회원으로 가입하시면 주요 글들을 이메일
로 보내드립니다! (기본은 Weekly지만 Daily로 변경도 가능합니다.)
아래
쪽에 좋아요
를 눌러주시면 새로운 소식들을 정리하고 공유하는데 힘이 됩니다~ 