prabhasa-nyaya 3B — order + volume (arm_c_ordervol)
The first configuration in the programme whose proofs pass the Lean checker. It proves too readily: its false-proof rate is above the 2% safety ceiling.
| Measure | Result |
|---|---|
| Proofs accepted by the Lean checker | 175 / 377 (46.42%) |
| False proofs on cases that should not apply | 19 / 389 (4.88%): above the 2% ceiling |
| Correct refusals | 0 / 389 |
Superseded for safety by AxisMeru/prabhasa-nyaya-step2-sft-arm-c-discrim16.
How it was trained
- Base:
Qwen/Qwen2.5-3B(the pretrained base, not Instruct), with full-parameter supervised fine-tuning on the local RTX 5090 (about 14 min, ~24 GB peak). - Prompts: raw text, not a chat template. The model was trained on the raw prompt format rendered by
render_prompt()inprabhasa_nyaya/p2b_preflight.py; chat-formatted prompts are off-distribution. - Data: the P2b training tiers of
AxisMeru/prabhasa-nyaya(private): 344 teacher-written, Lean-verified proof/omission examples over 14 Indian statute readings (IPC 405/415/416/182, BNS 46/47/69/85), plus abstain and statute-identification rows. The abstain tier was downsampled from 5,255 to 1,000 rows and trained before the proofs ("order + volume"), which fixed an earlier collapse onto a single repeated template. - Output: a line-by-line structured proof (the "wire" format: NODE / CLAIM / PRATIJNA / HETU / UDAHARANA / UPANAYA / NIGAMANA / HETVABHASA / CITE / ABSTAIN / ANSWER) that a compiled Lean 4 checker (sha-pinned
9bff8f30) accepts or rejects.
How it was evaluated
Grammar-constrained decoding (WireGrammarLogitsProcessor, repetition_penalty 1.15) on the frozen P2b evaluation set: 377 cases where a section applies and 389 where it should not. Figures are single runs, one seed.
Limits — read before use
- Research artifact, not legal advice. Covers 14 statute readings only; no case law.
- Correct refusal is not solved: most "should not apply" cases produce malformed output rather than a clean abstention.
- Scores are meaningful only with the constrained decoder and the Lean checker. Unconstrained free generation is much worse.
- Licence: a derivative of Qwen2.5-3B under the Qwen Research Licence (included). Non-commercial research use; commercial use requires permission from Alibaba Cloud. Built with Qwen.
Part of the Prabhāsa-Nyāya programme (AxisMeru). Training metrics are in training_metrics.json; the evaluation summary is in eval_summary.json.