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.

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.

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.

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 for the complete contract and decisions.