CoolFace
Modelpublic

AxisMeru/prabhasa-nyaya-step2-sft-arm-c-discrim16

sourceHugging Faceotherupdated 4d agoView on Hugging Face
0likes215downloads
Model Card

prabhasa-nyaya 3B — order + volume + 16 confusable negatives (armcordervol_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.

MeasureResult
Proofs accepted by the Lean checker108 / 377 (28.65%)
False proofs on cases that should not apply4 / 389 (1.03%): under the 2% ceiling
Correct refusals7 / 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() in prabhasa_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.