prabhasa-nyaya 3B — order + volume + 16 confusable negatives (arm_c_ordervol_discrim16)
The best configuration as of 2026-09-22. It adds 16 "looks like section X but isn't" training cases, which bring false proofs under the 2% ceiling.
| Measure | Result |
|---|---|
| Proofs accepted by the Lean checker | 108 / 377 (28.65%) |
| False proofs on cases that should not apply | 4 / 389 (1.03%): under the 2% ceiling |
| Correct refusals | 7 / 389 (1.8%): far below the 90% target |
195 of the 263 malformed outputs declare ELEMENT elN GUNA where NODE elN GUNA belongs. No training row does this; the error arises during training.
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.