Mathagentic Knowledge Bundle
Bundle OKF 0.2 · 3 conceitos · schneiderkamplab/mathagentic
Open source Repository Open in the app JSON README (API)
About
# Mathagentic Knowledge Bundle
Operational and technical knowledge for executable arithmetic tool-use SFT
construction.
## Start Here
- [OKF Maintenance](schema.md) - Authoring and validation rules.
- [Knowledge Pages](pages/) - Architecture, data contracts, and operations.
- [Bundle Log](log.md) - Substantial documentation and decision updates.
Details
- Kind
- OKF bundles
- Topic
- No topic detected
- Publisher
- schneiderkamplab
- Origin
- okf_github
- Category
- dados
- Version
- 0.2
- Last push
- 2026-09-08T11:35:02Z
- Repository state
- ativo
- Language
- Python
- License
- Apache-2.0
- Added
- 2026-09-10 02:06:41
- Updated
- 2026-09-10 02:06:41
- Origin id
schneiderkamplab/mathagentic:wiki/index.md
README
# Mathagentic
Mathagentic converts executable arithmetic programs into complete agentic SFT
trajectories for HRM-Text. It currently supports:
- `TinyGSM/TinyGSM`: restricted Python programs normalized to `solve()`;
- `niklasm222/gsm8k-prolog-prover`: SWI-Prolog programs defining `solve/1`,
checked against `openai/gsm8k` train answers.
Each output row contains one native tool definition, a user problem, an
assistant tool call, a precomputed tool result, and a terminal assistant target
containing only `\boxed{...}`. The bundled template renders this OpenAI-shaped
structure into Mimir's Gemma 4 native tool syntax. No executor is needed during
training, although real inference still needs an orchestrator that executes
model-requested tools.
## Install
```bash
conda env create -f environment.yml
conda activate mathagentic
uv pip install -e '.[test]'
```
The Conda environment supplies Python 3.12 and SWI-Prolog 10.0. Python source
is accepted only after strict AST validation and is executed in a
resource-limited isolated interpreter process.
## Build
```bash
mathagentic download --output data/raw --workers 64
mathagentic convert-prolog \
--source data/raw/gsm8k-prolog-prover \
--gsm8k data/raw/gsm8k \
--output data/converted/gsm8k-prolog \
--mismatch-verdicts verdicts/gsm8k-prolog-gold-overrides.jsonl \
--program-repairs verdicts/gsm8k-prolog-program-repairs.jsonl \
--workers 64
# Build execution-verified candidates. Production admission should additionally
# pass --semantic-verdicts and --require-semantic-verdict.
mathagentic convert-tinygsm \
--source data/raw/tinygsm \
--output data/converted/tinygsm \
--max-rows 500000 \
--sample-modulus 20 \
--workers 64
# Semantically audit candidates using existing OpenAI-compatible servers.
mathagentic audit-tinygsm \
--source data/converted/tinygsm \
--output data/audits/tinygsm/verdicts.jsonl \
--failures data/audits/tinygsm/failures.jsonl \
--endpoint http://127.0.0.1:8100 \
--endpoint http://127.0.0.1:8101 \
--endpoint http://127.0.0.1:8102 \
--endpoint http://127.0.0.1:8103 \
--concurrency 512 \
--max-output-tokens 64
# Rebuild after auditing, admitting only positive semantic verdicts.
mathagentic convert-tinygsm \
--source data/raw/tinygsm \
--output data/converted/tinygsm-semantic \
--max-rows 500000 \
--sample-modulus 20 \
--semantic-verdicts data/audits/tinygsm/verdicts.jsonl \
--require-semantic-verdict \
--workers 64
mathagentic validate --source data/converted
mathagentic tokenize \
--source data/converted \
--output data/tokenized \
--tokenizer /work/mimir/brainsurgery/models/gemma4_31b/tokenizer.json \
--max-seq-len 4096 \
--workers 5
```
`data/tokenized` uses HRM-Text's task array contract:
`tokens.npy`, `inst_start.npy`, `inst_len.npy`, `resp_start.npy`, and
`resp_len.npy`. Tokenization accepts plain or gzip-compressed JSONL shards and
atomically commits one task directory per input shard. Every source trajectory
yields two supervised examples. Tool definitions and prior messages are prompt
tokens; only the current assistant call or terminal boxed answer is a response
target. Train this source only with HRM-Text `data.target_only=true`; disabling
target-only masking would also supervise the rendered prompt and tool-result
tokens.
The tokenized task tree is intended to be merged into DFM11's tokenized union
and sampled with `data_io/sample_tokenized.py`. HRM-Text itself reads the
sampler's aggregate `tokens.npy`, `metadata.json`, and `epoch_N` indices, not a
raw JSONL or unsampled task tree.
## Quality boundary
Prolog rows are retained only when execution exactly matches the corresponding
GSM8K-train answer. TinyGSM has no authoritative answer field. Its deterministic
conversion rejects malformed, multi-question, unsafe, non-scalar, and
non-executable rows, but execution alone does not establish semantic
correctness. A production DFM11 build must use independent row-level verdicts
and `--require-semantic-verdict`.
See the [knowledge bundle](wiki/index.md) for the complete contract and
decisions.