
什么是 Open Math Harness?
Open Math Harness 是 Open Math OS 背后的开源运行时。其第一代版本名为 Nucleus,使用 Rust 编写,包含该平台所使用的内核、服务和代理。
该运行时专为协作式数学研究而设计。它支持运行在开放权重模型上的代理、通过 Ultramath 进行并行问题探索、经 Lean 验证的证明搜索、项目记忆、工具,以及对受保护操作进行人工批准。
当前限制:完整运行时依赖 Open Math OS 部署环境。该仓库可以从源代码构建,并包含一个小型自包含示例,但目前尚未提供用于交互式代理、Ultramath、记忆或证明搜索的独立本地环境。
核心设计与功能
基于能力的隔离
Open Math Harness 使用基于能力的微内核。每个进程只能获得其组合所授予的权限,而它启动的任何进程所获得的权限不会超过父进程能够委派的范围。这一规则同样适用于代理和其他程序。
模型响应、工具结果、仓库文件和其他文本均被视为不可信输入。文本不能授予权限、批准受保护操作或决定证明是否有效。凭据保留在权限严格受限的提供程序中,不会暴露给模型、记录内容或日志。
代理与研究工具
- 开放模型代理:会话可以使用开放权重模型,并支持流式响应、工具、子代理和持久化历史记录。
- Ultramath:多个代理异步研究困难问题的不同解法,分享发现,并向协调代理提交报告。
- 证明搜索:工作进程在候选 Lean 证明树中探索不同分支。只有经过 Lean 针对原始命题验证的候选证明才会成功。
- 项目工具:代理可以使用仓库文件、shell、Web 和 PDF 工具、项目技能、MCP 服务器及插件。
- 人工控制:受保护操作必须等待批准,同时会话记录在显示前会经过机密信息扫描。
项目记忆
每个项目分别维护记忆。当会话变得安静后,记忆服务可以从其历史记录中提取有用材料,并将选定信息整合到 MEMORY.md 中。后续会话会将这些记忆作为上下文接收,并引用所使用的材料。
记忆仅提供上下文,不能授予权限,也不能覆盖用户当前的指令。
前置条件
在构建 Open Math Harness 之前,请准备好受支持的 Linux 环境及以下依赖:
- Linux:不支持将 Windows 和 macOS 作为原生运行时主机。
- 原生构建工具:安装用于原生依赖的 C 编译器和链接器。
- 通过 rustup 安装 Rust:仓库中的
rust-toolchain.toml固定了所需工具链,并包含格式化和 lint 组件。 - 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.json步骤 2:了解演示内容
运行期间,脚本化代理会执行三类重要操作:
- 读取其获授能力允许访问的文件。
- 将一个更小目录的访问权限委派给其工作进程。
- 尝试执行超出自身权限、因而被内核拒绝的操作。
这使得 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 集成检查。
高级用法与开发提示
使用日志研究能力边界
将 JSON Lines 文件作为审计记录时,切片示例最为有用。请结合查看代理记录、工作进程记录和文件系统访问日志。这样可以了解委派的访问权限如何进一步收窄,以及内核如何拒绝超出分配权限范围的操作。
分离部署要求
构建工作区不会自动生成完整的本地 Open Math OS 安装。交互式代理还需要服务配置、模型提供商凭据和客户端。证明搜索还需要配置好的 Lean 和 Mathlib 环境。
不要将 deploy/vm/ 中的受管理虚拟机配置视为通用安装脚本。目前,仓库将切片示例记录为受支持的自包含本地演示。
保持可复现的 Cargo 依赖解析
请在文档所述的构建和运行命令中使用 --locked。这样可以使依赖解析与仓库的锁定文件保持一致,并减少环境之间出现意外差异。
尽早验证隔离机制
如果启动失败,请先检查 bubblewrap,再调试更高层的服务。确认 bwrap 位于 PATH 中,并确认主机安全策略允许非特权用户命名空间。运行时在缺少必要隔离机制时会有意停止继续运行。
理解证明验证边界
在完整架构中,代理的信心并不能证明定理已经得到证明。候选证明会在具有限时的受隔离工作区中进行评估,并由 Lean 判定其是否通过。搜索记录会保留候选工作,以便后续轮次能够从之前的分支继续。
遵循贡献检查
在提交更改之前,请查看 CONTRIBUTING.md 和仓库的 CI 工作流。贡献指南说明了测试、AI 审查以及拉取请求中应提供的信息。
结语
Open Math Harness 为 Open Math OS 提供了面向安全的运行时基础。尽管完整的交互式环境尚未作为独立的本地设置提供,但你可以构建 Nucleus 工作区、运行其自包含的切片示例、检查能力强制机制,并执行默认测试。这些步骤为了解运行时的核心原则提供了切实的入门:代理在明确的权限范围内提出建议并执行操作,而人员和受信任的验证器保留控制权。
