Open Math Harnessとは？
Open Math Harnessは、Open Math OSの基盤となるオープンソースのランタイムです。第1世代はNucleusと名付けられ、Rustで記述されており、プラットフォームが使用するカーネル、サービス、エージェントを含みます。
このランタイムは、数学研究の協働作業向けに設計されています。オープンウェイトモデル上で動作するエージェント、Ultramathによる並列問題探索、Leanで検証された証明探索、プロジェクトメモリ、各種ツール、保護された操作に対する人間の承認をサポートできます。
現在の制限：完全なランタイムはOpen Math OSのデプロイ環境に依存します。リポジトリはソースからビルドでき、小規模な自己完結型の例も含まれていますが、インタラクティブエージェント、Ultramath、メモリ、証明探索のためのスタンドアロンのローカル環境はまだ提供していません。
中核設計と機能
能力ベースの隔離
Open Math Harnessは、能力ベースのマイクロカーネルを使用します。各プロセスには、その構成によって付与された権限だけが与えられ、起動したプロセスにも、親が委譲できる以上の権限は与えられません。これはエージェントだけでなく、他のプログラムにも適用されます。
モデルの応答、ツールの結果、リポジトリのファイル、その他のテキストは、信頼できない入力として扱われます。テキストによって権限を付与したり、保護された操作を承認したり、証明が有効かどうかを決定したりすることはできません。認証情報は、モデル、トランスクリプト、ログに公開されるのではなく、権限を厳しく制限したプロバイダー内に保持されます。
エージェントと研究ツール
- オープンモデルエージェント：セッションでは、ストリーミング応答、ツール、サブエージェント、永続的な履歴を備えたオープンウェイトモデルを使用できます。
- Ultramath：複数のエージェントが難しい問題に対する異なるアプローチを非同期に調査し、知見を共有して、調整役のエージェントにレポートを提出します。
- 証明探索：ワーカーは、Lean証明候補の木構造にある分岐を探索します。候補が成功するのは、Leanが元の命題に対して検証した場合だけです。
- プロジェクトツール：エージェントは、リポジトリのファイル、シェル、Webおよび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仮想マシン向けです。パーソナルコンピューター用のスタンドアロンインストーラーではありません。
自己完結型スライス例を実行する
リポジトリには、examples/slice/以下にスクリプト化された例が含まれています。この例では、エージェント、ワーカー、ファイルシステムサービスを起動し、能力のチェックと委譲を示します。
この例はモデルプロバイダーに接続せず、モデルの認証情報やOpen Math OSのデプロイメントも必要としません。また、インタラクティブチャット、Ultramath、メモリ、証明探索も起動しません。ただし、Linuxと機能するbubblewrapによる隔離は引き続き必要です。
ステップ1：例を起動する
リポジトリのルートから次を実行します。
cargo run --locked --manifest-path cli/Cargo.toml -- run examples/slice/config.jsonステップ2：デモンストレーションを理解する
実行中、スクリプト化されたエージェントは、次の3種類の重要な処理を行います。
- 付与された能力によってアクセスを許可されたファイルを読み取ります。
- より小さなディレクトリへのアクセスをワーカーに委譲します。
- 自身の権限を超えるため、カーネルが拒否する操作を試みます。
これにより、スライス例はプロジェクトの中心的なルール、つまりプロセスは実際に保有する能力だけを使用および委譲できるということを、簡潔に示します。
ステップ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 を使用してください。これにより、依存関係の解決がリポジトリのロックファイルと一致し、環境間で予期しない差異が生じにくくなります。
早い段階で隔離を検証する
起動に失敗した場合は、上位レベルのサービスをデバッグする前に bubblewrap を確認してください。bwrap が PATH 上にあり、ホストのセキュリティポリシーで非特権ユーザー名前空間が許可されていることを確認します。ランタイムは、必要な隔離機能がなければ意図的に処理を続行しません。
証明検証の境界を理解する
完全なアーキテクチャでは、エージェントの確信だけで定理が証明されたことにはなりません。候補証明は期限付きの隔離ワークスペースで評価され、合格したかどうかは Lean が判定します。探索記録には候補作業が保存されるため、後続ラウンドでは以前の分岐から続行できます。
コントリビューションのチェック項目に従う
変更を提案する前に、CONTRIBUTING.md とリポジトリの CI ワークフローを確認してください。コントリビューションガイドには、テスト、AI レビュー、プルリクエストで求められる情報について説明されています。
まとめ
Open Math Harness は、Open Math OS のセキュリティ重視ランタイム基盤を提供します。完全な対話型環境をスタンドアロンのローカル環境として利用できる状態にはまだありませんが、Nucleus ワークスペースをビルドし、自己完結型の slice 例を実行し、機能の強制適用を調べ、デフォルトテストを実行できます。これらの手順を通じて、ランタイムの中核原則を実践的に理解できます。エージェントは明示された権限の範囲内で提案と操作を行い、人間と信頼できる検証者が制御を保持します。