Xây dựng và chạy Open Math Harness: Hướng dẫn thực hành về Nucleus

Open Math Harness là gì?

Open Math Harness là runtime mã nguồn mở đứng sau Open Math OS. Thế hệ đầu tiên có tên Nucleus, được viết bằng Rust và chứa kernel, các dịch vụ cùng những agent được nền tảng sử dụng.

Runtime này được thiết kế cho nghiên cứu toán học cộng tác. Nó có thể hỗ trợ các agent chạy trên mô hình có trọng số mở, khám phá bài toán song song qua Ultramath, tìm kiếm chứng minh được Lean xác minh, bộ nhớ dự án, các công cụ và sự phê duyệt của con người đối với những hành động được bảo vệ.

Giới hạn hiện tại: runtime hoàn chỉnh phụ thuộc vào môi trường triển khai Open Math OS. Kho mã có thể được build từ mã nguồn và bao gồm một ví dụ nhỏ tự chứa, nhưng hiện chưa cung cấp môi trường cục bộ độc lập cho agent tương tác, Ultramath, bộ nhớ hoặc tìm kiếm chứng minh.

Thiết kế và tính năng cốt lõi

Giới hạn dựa trên capability

Open Math Harness sử dụng microkernel dựa trên capability. Mỗi tiến trình chỉ nhận quyền hạn được cấp bởi cấu hình của nó, và mọi tiến trình do nó khởi chạy không nhận nhiều quyền hơn mức tiến trình cha có thể ủy quyền. Điều này áp dụng cho cả agent và các chương trình khác.

Phản hồi của mô hình, kết quả công cụ, tệp trong kho mã và các văn bản khác đều được xem là đầu vào không đáng tin cậy. Văn bản không thể cấp quyền, phê duyệt hành động được bảo vệ hoặc xác định một chứng minh có hợp lệ hay không. Thông tin xác thực được giữ trong các provider có đặc quyền hẹp, thay vì để lộ cho mô hình, bản ghi phiên hoặc nhật ký.

Agent và công cụ nghiên cứu

• Agent dùng mô hình mở: Các phiên có thể sử dụng mô hình có trọng số mở với phản hồi dạng luồng, công cụ, agent con và lịch sử lâu dài.
• Ultramath: Nhiều agent sẽ bất đồng bộ khảo sát các hướng tiếp cận khác nhau cho một bài toán khó, chia sẻ phát hiện và gửi báo cáo cho agent điều phối.
• Tìm kiếm chứng minh: Các worker khám phá các nhánh trong cây chứng minh Lean tiềm năng. Một ứng viên chỉ thành công khi Lean xác minh được ứng viên đó với mệnh đề ban đầu.
• Công cụ dự án: Agent có thể làm việc với các tệp trong kho mã, shell, công cụ web và PDF, kỹ năng dự án, máy chủ MCP và plugin.
• Kiểm soát của con người: Các hành động được bảo vệ sẽ chờ phê duyệt, trong khi bản ghi phiên được quét tìm thông tin bí mật trước khi hiển thị.

Bộ nhớ dự án

Bộ nhớ được duy trì riêng cho từng dự án. Sau khi một phiên trở nên yên ắng, dịch vụ bộ nhớ có thể trích xuất nội dung hữu ích từ lịch sử và hợp nhất thông tin được chọn vào MEMORY.md. Các phiên sau sẽ nhận bộ nhớ này làm ngữ cảnh và trích dẫn nội dung mà chúng sử dụng.

Bộ nhớ chỉ cung cấp ngữ cảnh. Nó không thể cấp quyền hoặc ghi đè chỉ dẫn hiện tại của người dùng.

Điều kiện tiên quyết

Trước khi build Open Math Harness, hãy chuẩn bị một môi trường Linux được hỗ trợ với các phần phụ thuộc sau:

• Linux: Windows và macOS không được hỗ trợ làm máy chủ runtime gốc.
• Công cụ build gốc: Cài đặt trình biên dịch C và linker cho các phần phụ thuộc gốc.
• Rust qua rustup: Tệp rust-toolchain.toml của kho mã ghim toolchain bắt buộc và bao gồm các thành phần định dạng cùng lint.
• bubblewrap: Cài đặt bwrap, đặt nó trên PATH và bảo đảm máy chủ cho phép user namespace không đặc quyền.

Cơ chế giới hạn là bắt buộc. Nếu bubblewrap không thể tạo sandbox do chính sách bảo mật của máy chủ, runtime sẽ lỗi khi khởi động.

Build Open Math Harness từ mã nguồn

Clone kho mã, đi vào thư mục của kho và build toàn bộ workspace Rust:

git clone https://github.com/openmathmodel/open-math-harness.git
cd open-math-harness
cargo build --locked --workspace

Tùy chọn --locked yêu cầu Cargo sử dụng các phiên bản phụ thuộc được ghi trong lockfile. Sau khi build thành công, các binary launcher và dịch vụ có trong target/debug/.

Các tệp trong deploy/vm/ dành cho máy ảo Open Math OS được quản lý. Chúng không phải là trình cài đặt độc lập cho máy tính cá nhân.

Chạy ví dụ lát cắt tự chứa

Kho mã bao gồm một ví dụ dạng script trong examples/slice/. Ví dụ này khởi chạy một agent, một worker và một dịch vụ hệ thống tệp để minh họa việc kiểm tra capability và ủy quyền.

Ví dụ này không kết nối với provider mô hình và không yêu cầu thông tin xác thực mô hình hay một bản triển khai Open Math OS. Nó cũng không khởi chạy trò chuyện tương tác, Ultramath, bộ nhớ hoặc tìm kiếm chứng minh. Linux và cơ chế giới hạn bubblewrap hoạt động bình thường vẫn là yêu cầu bắt buộc.

Bước 1: Khởi động ví dụ

Từ thư mục gốc của kho mã, chạy:

cargo run --locked --manifest-path cli/Cargo.toml -- run examples/slice/config.json

Bước 2: Tìm hiểu phần minh họa

Trong quá trình chạy, agent dạng script thực hiện ba loại hoạt động quan trọng:

1. Đọc các tệp mà capability được cấp cho phép truy cập.
2. Ủy quyền quyền truy cập vào một thư mục con cho worker.
3. Thử thực hiện các thao tác bị kernel từ chối vì vượt quá quyền hạn.

Điều này biến ví dụ lát cắt thành phần minh họa ngắn gọn cho quy tắc trung tâm của dự án: một tiến trình chỉ có thể sử dụng và ủy quyền những capability mà nó thực sự nắm giữ.

Bước 3: Kiểm tra kết quả

Sau khi chạy xong, hãy kiểm tra bản ghi của agent và worker:

examples/slice/out/agent/transcript.jsonl
examples/slice/out/agent/worker/transcript.jsonl

Dịch vụ hệ thống tệp ghi riêng các lệnh gọi mà nó nhận được:

examples/slice/log/access.jsonl

Ví dụ này cũng tạo báo cáo sau:

examples/slice/data/work/report.txt

Hãy đối chiếu các bản ghi với nhật ký truy cập hệ thống tệp để xem những thao tác nào đã được yêu cầu, ủy quyền, chấp nhận hoặc từ chối.

Chạy lại ví dụ

Tệp report.txt được tạo ra sẽ ảnh hưởng đến các lần chạy lặp lại. Hãy xóa tệp này trước khi chạy lại ví dụ nếu bạn muốn việc tạo báo cáo thành công lần nữa:

rm examples/slice/data/work/report.txt
cargo run --locked --manifest-path cli/Cargo.toml -- run examples/slice/config.json

Việc giữ lại các tệp bản ghi và nhật ký cũ vẫn có thể hữu ích khi so sánh hành vi giữa các lần chạy, vì vậy hãy xem xét các thư mục đầu ra trước khi xóa thêm các tệp khác.

Chạy bộ kiểm thử

Sau khi xây dựng workspace, hãy chạy các bài kiểm thử Rust mặc định từ thư mục gốc của kho lưu trữ:

cargo test --workspace

Bộ kiểm thử mặc định không yêu cầu API mô hình trả phí hoặc thông tin xác thực môi trường production. Một số bài kiểm thử tích hợp khởi chạy các tiến trình con thực và sử dụng bubblewrap, nên các yêu cầu cô lập Linux tương tự vẫn được áp dụng.

Các bài kiểm thử yêu cầu nhà cung cấp mô hình bên ngoài hoặc cài đặt Lean được bật riêng theo tùy chọn. Quy trình CI của kho lưu trữ cũng xác định các kiểm tra về định dạng, Clippy, công cụ Python và tích hợp MCP của Node.js.

Cách sử dụng nâng cao và mẹo phát triển

Sử dụng nhật ký để nghiên cứu ranh giới quyền năng

Ví dụ slice hữu ích nhất khi các tệp JSON Lines của nó được xem như một dấu vết kiểm toán. Hãy xem đồng thời bản ghi của agent, bản ghi của worker và nhật ký truy cập hệ thống tệp. Điều này cho thấy quyền truy cập được ủy quyền trở nên hạn chế hơn như thế nào và kernel từ chối các thao tác nằm ngoài thẩm quyền được giao ra sao.

Tách biệt các yêu cầu triển khai

Việc xây dựng workspace không tự động tạo ra một cài đặt Open Math OS cục bộ hoàn chỉnh. Các agent tương tác còn yêu cầu cấu hình dịch vụ, thông tin xác thực của nhà cung cấp mô hình và một client. Việc tìm kiếm chứng minh cũng yêu cầu môi trường Lean và Mathlib đã được cấu hình.

Tránh xem cấu hình máy ảo được quản lý trong deploy/vm/ như một tập lệnh cài đặt đa mục đích. Hiện tại, kho lưu trữ chỉ tài liệu hóa ví dụ slice như bản trình diễn cục bộ khép kín được hỗ trợ.

Duy trì việc phân giải Cargo có thể tái lập

Hãy sử dụng --locked với các lệnh xây dựng và chạy đã được tài liệu hóa. Điều này giữ cho việc phân giải phụ thuộc phù hợp với tệp khóa của kho lưu trữ và giảm các khác biệt không mong muốn giữa các môi trường.

Kiểm tra cơ chế cô lập sớm

Nếu quá trình khởi động thất bại, hãy kiểm tra bubblewrap trước khi gỡ lỗi các dịch vụ cấp cao hơn. Xác nhận rằng bwrap có trong PATH và chính sách bảo mật của máy chủ cho phép các user namespace không đặc quyền. Runtime cố ý không tiếp tục nếu thiếu cơ chế cô lập bắt buộc.

Hiểu ranh giới xác minh chứng minh

Trong kiến trúc đầy đủ, sự tin tưởng của agent không chứng minh rằng một định lý đã được chứng minh. Các chứng minh ứng viên được đánh giá trong những workspace bị cô lập với thời hạn, và Lean quyết định chúng có đạt hay không. Các bản ghi tìm kiếm lưu lại công việc ứng viên để những vòng sau có thể tiếp tục từ các nhánh trước đó.

Tuân thủ các kiểm tra đóng góp

Trước khi đề xuất thay đổi, hãy xem CONTRIBUTING.md và quy trình CI của kho lưu trữ. Hướng dẫn đóng góp mô tả việc kiểm thử, đánh giá AI và những thông tin cần có trong các pull request.

Kết luận

Open Math Harness cung cấp nền tảng runtime chú trọng bảo mật cho Open Math OS. Mặc dù môi trường tương tác hoàn chỉnh hiện chưa có dưới dạng một thiết lập cục bộ độc lập, bạn vẫn có thể xây dựng workspace Nucleus, chạy ví dụ slice khép kín, kiểm tra việc thực thi quyền năng và chạy các bài kiểm thử mặc định. Những bước này mang đến phần giới thiệu thực tế về nguyên tắc cốt lõi của runtime: các agent đề xuất và hoạt động trong phạm vi thẩm quyền rõ ràng, còn con người và các bộ xác minh đáng tin cậy vẫn duy trì quyền kiểm soát.