Open Math Harness란?
Open Math Harness는 Open Math OS를 구동하는 오픈 소스 런타임입니다. Nucleus라는 이름의 1세대 런타임은 Rust로 작성되었으며 플랫폼에서 사용하는 커널, 서비스, 에이전트를 포함합니다.
이 런타임은 협업 수학 연구를 위해 설계되었습니다. 오픈 웨이트 모델에서 실행되는 에이전트, Ultramath를 통한 병렬 문제 탐색, Lean 검증 증명 검색, 프로젝트 메모리, 도구, 보호된 작업에 대한 사람의 승인을 지원할 수 있습니다.
현재 제한 사항: 전체 런타임은 Open Math OS 배포 환경에 의존합니다. 저장소는 소스에서 빌드할 수 있고 소규모 독립 실행형 예제를 포함하지만, 대화형 에이전트, Ultramath, 메모리 또는 증명 검색을 위한 독립적인 로컬 환경은 아직 제공하지 않습니다.
핵심 설계 및 기능
권한 기반 격리
Open Math Harness는 권한 기반 마이크로커널을 사용합니다. 각 프로세스는 구성에 따라 부여된 권한만 받으며, 해당 프로세스가 시작하는 프로세스는 부모가 위임할 수 있는 권한보다 더 많은 권한을 받지 않습니다. 이는 에이전트뿐 아니라 다른 프로그램에도 적용됩니다.
모델 응답, 도구 결과, 저장소 파일 및 기타 텍스트는 신뢰할 수 없는 입력으로 처리됩니다. 텍스트는 권한을 부여하거나, 보호된 작업을 승인하거나, 증명의 유효성을 결정할 수 없습니다. 자격 증명은 모델, 대화 기록 또는 로그에 노출되지 않고 제한된 권한을 가진 제공자 내부에 보관됩니다.
에이전트 및 연구 도구
- 오픈 모델 에이전트: 세션은 스트리밍 응답, 도구, 하위 에이전트 및 영구 기록을 지원하는 오픈 웨이트 모델을 사용할 수 있습니다.
- Ultramath: 여러 에이전트가 어려운 문제에 대해 서로 다른 접근법을 비동기적으로 조사하고, 결과를 공유하며, 조정 에이전트에 보고서를 제출합니다.
- 증명 검색: 작업자들이 후보 Lean 증명 트리의 여러 분기를 탐색합니다. 후보 증명은 Lean이 원래 명제에 대해 검증한 경우에만 성공합니다.
- 프로젝트 도구: 에이전트는 저장소 파일, 셸, 웹 및 PDF 도구, 프로젝트 스킬, MCP 서버, 플러그인을 사용할 수 있습니다.
- 사람의 통제: 보호된 작업은 승인을 기다리며, 세션 기록은 표시되기 전에 비밀 정보가 있는지 검사됩니다.
프로젝트 메모리
메모리는 프로젝트별로 별도로 관리됩니다. 세션이 조용해지면 메모리 서비스가 기록에서 유용한 자료를 추출하고, 선택한 정보를 MEMORY.md에 통합할 수 있습니다. 이후 세션은 이 메모리를 컨텍스트로 받고 사용한 자료를 인용합니다.
메모리는 컨텍스트만 제공합니다. 권한을 부여하거나 사용자의 현재 지시를 무시할 수 없습니다.
사전 요구 사항
Open Math Harness를 빌드하기 전에 다음 종속성이 설치된 지원되는 Linux 환경을 준비하세요:
- Linux: Windows와 macOS는 네이티브 런타임 호스트로 지원되지 않습니다.
- 네이티브 빌드 도구: 네이티브 종속성을 위해 C 컴파일러와 링커를 설치하세요.
- rustup을 통한 Rust: 저장소의
rust-toolchain.toml이 필요한 툴체인을 고정하며 포매팅 및 린팅 구성 요소를 포함합니다. - bubblewrap:
bwrap을 설치하고PATH에 추가한 다음, 호스트가 권한 없는 사용자 네임스페이스를 허용하는지 확인하세요.
격리는 필수입니다. 호스트의 보안 정책으로 인해 bubblewrap이 샌드박스를 생성하지 못하면 런타임이 시작 중에 실패합니다.
소스에서 Open Math Harness 빌드
저장소를 복제하고 해당 디렉터리로 이동한 다음 전체 Rust 워크스페이스를 빌드하세요:
git clone https://github.com/openmathmodel/open-math-harness.git
cd open-math-harness
cargo build --locked --workspace--locked 옵션을 사용하면 Cargo가 잠금 파일에 기록된 종속성 버전을 사용합니다. 빌드가 성공하면 런처와 서비스 바이너리를 target/debug/에서 사용할 수 있습니다.
deploy/vm/아래의 파일은 관리형 Open Math OS 가상 머신을 대상으로 합니다. 개인용 컴퓨터에 설치하는 독립 실행형 설치 프로그램이 아닙니다.
독립 실행형 Slice 예제 실행
저장소에는 examples/slice/ 아래에 스크립트로 실행되는 예제가 포함되어 있습니다. 이 예제는 에이전트, 작업자, 파일 시스템 서비스를 시작하여 권한 확인과 위임을 보여 줍니다.
이 예제는 모델 제공자에 연결하지 않으며 모델 자격 증명이나 Open Math OS 배포가 필요하지 않습니다. 또한 대화형 채팅, Ultramath, 메모리 또는 증명 검색을 시작하지 않습니다. Linux와 정상적으로 작동하는 bubblewrap 격리는 여전히 필요합니다.
1단계: 예제 시작
저장소 루트에서 다음을 실행하세요:
cargo run --locked --manifest-path cli/Cargo.toml -- run examples/slice/config.json2단계: 시연 내용 이해
실행 중 스크립트로 작성된 에이전트는 다음 세 가지 중요한 작업을 수행합니다:
- 부여받은 권한으로 접근할 수 있는 파일을 읽습니다.
- 더 작은 디렉터리에 대한 접근 권한을 작업자에게 위임합니다.
- 자신의 권한을 초과하기 때문에 커널이 거부하는 작업을 시도합니다.
이를 통해 Slice 예제는 프로젝트의 핵심 규칙을 간결하게 보여 줍니다. 프로세스는 실제로 보유한 권한만 사용하고 위임할 수 있습니다.
3단계: 결과 확인
실행이 끝나면 에이전트와 작업자의 대화 기록을 확인하세요:
examples/slice/out/agent/transcript.jsonl
examples/slice/out/agent/worker/transcript.jsonl파일 시스템 서비스는 수신한 호출을 별도로 기록합니다:
examples/slice/log/access.jsonl이 예제는 다음 보고서도 생성합니다:
examples/slice/data/work/report.txt어떤 작업이 요청되었고, 위임되었으며, 허용되거나 거부되었는지 확인하려면 트랜스크립트와 파일 시스템 액세스 로그를 비교하세요.
예제 다시 실행하기
생성된 report.txt는 반복 실행에 영향을 줍니다. 예제를 다시 실행하여 보고서 생성을 성공시키려면 먼저 이 파일을 삭제하세요:
rm examples/slice/data/work/report.txt
cargo run --locked --manifest-path cli/Cargo.toml -- run examples/slice/config.json이전 트랜스크립트와 로그 파일은 실행 간 동작을 비교할 때 여전히 유용할 수 있으므로, 추가 아티팩트를 삭제하기 전에 출력 디렉터리를 확인하세요.
테스트 모음 실행하기
워크스페이스를 빌드한 후 저장소 루트에서 기본 Rust 테스트를 실행하세요:
cargo test --workspace기본 테스트 모음에는 유료 모델 API나 프로덕션 자격 증명이 필요하지 않습니다. 일부 통합 테스트는 실제 자식 프로세스를 실행하고 bubblewrap을 사용하므로 동일한 Linux 격리 요구 사항이 적용됩니다.
외부 모델 제공자나 Lean 설치가 필요한 테스트는 명시적으로 선택해야 실행됩니다. 저장소의 CI 워크플로에는 포매팅, Clippy, Python 도구, Node.js MCP 통합 검사도 정의되어 있습니다.
고급 사용법 및 개발 팁
로그로 기능 경계 연구하기
slice 예제는 JSON Lines 파일을 감사 추적 기록으로 활용할 때 가장 유용합니다. 에이전트 트랜스크립트, 워커 트랜스크립트, 파일 시스템 액세스 로그를 함께 검토하세요. 이를 통해 위임된 액세스가 어떻게 더 제한적으로 바뀌는지, 그리고 커널이 할당된 권한 범위를 벗어난 작업을 어떻게 거부하는지 확인할 수 있습니다.
배포 요구 사항 분리하기
워크스페이스를 빌드해도 완전한 로컬 Open Math OS 설치 환경이 자동으로 생성되지는 않습니다. 대화형 에이전트에는 추가로 서비스 구성, 모델 제공자 자격 증명, 클라이언트가 필요합니다. 증명 검색에는 구성된 Lean 및 Mathlib 환경도 필요합니다.
deploy/vm/의 관리형 VM 구성을 범용 설치 스크립트로 취급하지 마세요. 현재 저장소에서는 slice 예제를 지원되는 독립형 로컬 데모로 문서화하고 있습니다.
재현 가능한 Cargo 의존성 해결 유지하기
문서화된 빌드 및 실행 명령에 --locked를 사용하세요. 이렇게 하면 의존성 해결이 저장소의 lockfile과 일치하고 환경 간 예기치 않은 차이를 줄일 수 있습니다.
격리를 조기에 확인하기
시작에 실패하면 상위 수준 서비스를 디버깅하기 전에 bubblewrap을 확인하세요. bwrap이 PATH에 포함되어 있고 호스트 보안 정책이 권한 없는 사용자 네임스페이스를 허용하는지 확인하세요. 런타임은 필요한 격리 기능 없이는 의도적으로 계속 실행되지 않습니다.
증명 검증 경계 이해하기
전체 아키텍처에서 에이전트의 확신만으로는 정리가 증명되었다고 할 수 없습니다. 후보 증명은 기한이 설정된 격리된 작업 공간에서 평가되며, 통과 여부는 Lean이 결정합니다. 검색 기록은 후보 작업을 보존하므로 이후 라운드에서 이전 분기부터 계속 진행할 수 있습니다.
기여 검사 따르기
변경 사항을 제안하기 전에 CONTRIBUTING.md와 저장소의 CI 워크플로를 검토하세요. 기여 가이드에는 테스트, AI 검토, 풀 리퀘스트에 포함해야 할 정보가 설명되어 있습니다.
결론
Open Math Harness는 Open Math OS를 위한 보안 중심 런타임 기반을 제공합니다. 완전한 대화형 환경을 독립형 로컬 설정으로 아직 사용할 수는 없지만, Nucleus 워크스페이스를 빌드하고 독립형 slice 예제를 실행하며 기능 권한 적용을 검사하고 기본 테스트를 실행할 수 있습니다. 이러한 단계는 런타임의 핵심 원칙을 실질적으로 소개합니다. 에이전트는 명시적인 권한 범위 안에서 제안하고 작업하며, 사람과 신뢰할 수 있는 검증자는 통제권을 유지합니다.