Hesper

Lean 4로 GPU 프로그램을 작성하고, 그 정확성을 증명하며, WebGPU 또는 CUDA에서 실행하세요.

[!IMPORTANT]
Alpha 소프트웨어입니다. API, 검증 기능 및 컴파일러는 활발히 개발 중이며 변경될 수 있습니다. 현재 초점: BitNet, Gemma 4, 그리고 verified-AD 레이어입니다.

Hesper는 검증된 GPU 프로그래밍 프레임워크입니다. Lean 4에서 타입 안전한 셰이더와 고수준 텐서 코드를 작성하고, 동일한 언어로 정확성을 증명하며, 그 결과를 WebGPU (Metal / Vulkan / D3D12) 또는 CUDA PTX에서 실행할 수 있습니다.

import Hesper.WGSL.DSL

-- Lean의 elaboration 시간(시간)에 검사되는 타입 안전한 셰이더 표현식:
...

Hesper 방식 (The Hesper Way)

IP 카탈로그 (IP Catalog)

| 모델 / IP | 백엔드 | 상태 | 진입점 | |
|---|---|---|---|
| BitNet b1.58 (2 B) | WebGPU | ✅ M4 Max에서 125 TPS | lake exe bitnet-complete |
| ... | |

릴리스 타임라인은 docs/CHANGELOG.md를 참조하세요.

빠른 시작 (Quick Start)

옵션 1 — 튜토리얼 Docker 이미지 (권장)

Lean 4, xeus-lean, Jupyter Lab 및 모든 12개 튜토리얼 챕터를 실행 가능한 노트북으로 포함하는 사전 구축된 이미지:

docker run --rm -p 8888:8888 ghcr.io/verilean/hesper-tutorial:latest
# → 브라우저에서 http://localhost:8888 열기

옵션 2 — 로컬 빌드

git clone https://github.com/Verilean/hesper.git
cd hesper
lake build Hesper             # 네이티브 의존성(Dawn, Highway)을 필요에 따라 빌드
...

사전 요구 사항: Lean 4 (elan를 통해), C++17 툴체인, CMake ≥ 3.16. CUDA에서 Gemma 4 사용 시: NVIDIA 드라이버 + CUDA Toolkit. 전체 설정 지침: docs/tutorial/md/Ch00_Setup.md.

문서 (Documentation)

튜토리얼이 표준 진입점입니다. 각 챕터는 Markdown 마스터이며, xeus-lean을 통해 실행 가능한 Jupyter 노트북으로도 렌더링됩니다.

다른 사용자 대상 문서:

• docs/LORA_FINETUNING.md — BitNet LoRA 훈련 가이드
• docs/VERIFIED_AD.md — Verified-AD 설계 노트
• docs/circuit-dsl-tutorial.md — 커널-융합 DSL 심층 분석
• docs/research/ — 보관된 내부 R&D 노트 (유지되지 않음)

작동 방식

┌──────────────────────────────────────────────────────────────┐
│  Lean 4 코드                                                  │
│  ─ 타입 안전 셰이더 DSL  ─ 텐서 연산(Tensor ops)  ─ 형식 증명        │
... 

동일한 DSL은 두 가지 표면 언어(surface languages)를 방출합니다. 컴파일 시간에 백엔드를 선택하세요 (-Kgpu=cuda는 CUDA 실행 파일용, 그 외 기본값은 WebGPU).

예시

lake exe bitnet-complete             # BitNet b1.58 추론 end-to-end
lake exe gemma4-cuda data/...gguf "Hello"   # CUDA를 사용한 Gemma 4
lake exe tetris                      # 인터랙티브 WebGPU 게임
... 

Examples/ 디렉터리에는 주제별로 분류된 약 90개의 실행 가능한 데모가 있습니다 (DSL/, Compute/, Graphics/, MachineLearning/, …).

프로젝트 구조

Hesper/
├── Hesper/             # 핵심 라이브러리 (DSL, WebGPU, CUDA, 레이어(Layers), 모델(Models))
├── Examples/           # 약 90개의 실행 가능한 데모
... 

테스트

lake build test-all && ./.lake/build/bin/test-all

동일한 테스트 스위트가 Linux + Vulkan, macOS + Metal, Windows + D3D12, 그리고 CPU 전용 폴백 경로에서 CI를 통해 실행됩니다.

기여하기(Contributing)

CONTRIBUTING.md를 참조하세요. 요약하자면: 포크(fork)하고, 브랜치(branch)를 만들고, 테스트 스위트를 실행한 다음, PR을 여세요. 버그 보고 및 설계 논의는 GitHub Issues / Discussions로 보내주세요.

라이선스

Apache-2.0. LICENSE를 참조하세요.

감사의 말(Acknowledgments)

• Lean 4 — 우리가 기반으로 구축한 언어입니다.
• Google Dawn — WebGPU 네이티브 런타임입니다.
• Google Highway — 이식 가능한 SIMD(Single Instruction, Multiple Data)입니다.
• Verilean / sparkle — 하드웨어 기술 언어 설명에 동일한 검증 아이디어를 가져오는 자매 프로젝트입니다.

커뮤니티

• Discord: https://discord.gg/94Xueve8WD — 설계 토론, 주간 진행 상황 스레드, 초보자 Q&A를 진행합니다.