TorchLean은 Lean에서 텐서 연산과 신경망 학습을 수행하고, 같은 언어로 수학적 성질을 증명할 수 있는 프레임워크다. 신경망 검증을 다루거나 정밀도를 조절한 수치 계산을 Lean 코드와 함께 사용하려는 사람이 대상이다. GPU 실행은 LibTorch 등을 이용하며, 외부 GPU 구현은 Lean 증명과 별도의 신뢰 경계로 남는다.
설치는 저장소를 복제한 뒤 캐시를 받고 빌드하는 방식이다.
git clone https://github.com/lean-dojo/TorchLean.git
cd TorchLean
scripts/lake.sh exe cache get
scripts/lake.sh build
설치 안내에는 Linux, macOS, Windows/WSL, CUDA와 LibTorch 설정이 나와 있다. CPU에서 간단한 학습 예제를 실행하는 명령은 다음과 같다.
scripts/lake.sh exe torchlean quickstart_mlp --device cpu --steps 10 --arithmetic ieee
scripts/lake.sh exe torchlean quickstart_mlp --device cpu --steps 10
첫 번째 명령은 FloatLib의 binary32 연산을 사용하고, 두 번째는 Lean의 기본 Float32를 쓴다. CUDA 실행에는 CUDA를 지원하는 LibTorch SDK와 호환되는 툴킷, NVIDIA GPU가 필요하다. CUDA를 사용할 수 없으면 명령은 오류를 반환한다.
TorchLean은 차원을 타입에 담은 텐서를 제공해 연산을 구성할 때 모양을 검사한다. 사용자는 자체 텐서 계산을 작성하거나 모델을 만들고 학습시킬 수 있다. FloatLib를 이용하면 binary32, binary128 또는 사용자 정의 이진 형식으로 CPU 텐서와 타입 지정 모델을 계산할 수 있으며, 반올림과 수치 오차의 상한을 명시적 가정 아래 증명할 수 있다. 자세한 내용은 정밀도 안내와 텐서 안내에서 확인할 수 있다.
자동 미분은 TorchLean이 관리한다. GPU에서는 LibTorch의 ATen 연산으로 텐서 값과 국소 기울기를 계산하며, GPU 테이프는 Float32에 binary32, Float에 binary64를 유지한다. 설정된 이진 연산도 GPU 테이프에 기록할 수 있지만, 기본 모델 연산자와 옵티마이저 체크포인트는 여전히 기본 데이터 형식을 요구한다. 십진 형식과 posit 형식은 CPU에서 실행된다. 사용자 정의 계산의 지원 연산과 GPU 실행 경계는 사용자 정의 연산 안내에서 설명한다.
검증 기능은 입력 영역에서 분류기의 예측이 유지되는지와 같은 속성을 다룬다. 외부 도구가 만든 인증서를 검사할 수도 있지만, 검사기가 인증서를 받아들였다는 사실만으로 의미적 보장이 성립하지는 않는다. 의미적 보장에는 검사기의 건전성 정리와 그 가정이 필요하며, Lean 증명에는 커널이 검사한 승인 증거가 필요하다. 인증서를 만든 프로그램 자체가 검증되는 것은 아니다. CPU 명령, CUDA 커널, cuBLAS, LibTorch, PyTorch와 같은 외부 시스템도 런타임 제공자로 남는다. 자세한 신뢰 경계는 문서를 참고할 수 있다.
다른 Lean 프로젝트에서는 저장소를 Lake 패키지로 추가해 사용할 수 있다. 모델·데이터·학습 코드에는 NN.API를, 증명이나 백엔드 인프라까지 필요한 경우에는 NN을 가져오도록 안내한다. TorchLean은 MIT License로 배포된다. 프로젝트 저장소는 GitHub, 논문은 arXiv에서 확인할 수 있다.
댓글 (0)
로그인하면 이 기사에 내 생각을 남길 수 있어요