# Governed Deduction: Policy-Grounded Premise Authorization Beyond Relevance

arXiv: https://arxiv.org/abs/2609.31029 · HTML: https://mlsanity.com/paper/2609.31029/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 11 of its 43 references that are in the map.
- First posted on arXiv 25 Sep 2026.

## Builds on (most cited first, 11 of 11)

- [LeanDojo: Theorem Proving with Retrieval-Augmented Language Models](https://mlsanity.com/paper/2306.15626/) (2023)
- [Selection-Inference: Exploiting Large Language Models for Interpretable Logical Reasoning](https://mlsanity.com/paper/2205.09712/) (2022)
- [Transformers as Soft Reasoners over Language](https://mlsanity.com/paper/2002.05867/) (2020)
- [Proof Artifact Co-training for Theorem Proving with Language Models](https://mlsanity.com/paper/2102.06203/) (2021)
- [DeepMath - Deep Sequence Models for Premise Selection](https://mlsanity.com/paper/1606.04442/) (2016)
- [Magnushammer: A Transformer-Based Approach to Premise Selection](https://mlsanity.com/paper/2303.04488/) (2023)
- [Generating Correctness Proofs with Neural Networks](https://mlsanity.com/paper/1907.07794/) (2019)
- [TacticZero: Learning to Prove Theorems from Scratch with Deep Reinforcement Learning](https://mlsanity.com/paper/2102.09756/) (2021)
- [MizAR 40 for Mizar 40](https://mlsanity.com/paper/1310.2805/) (2013)
- [Don't Take the Premise for Granted: Evaluating the Premise Critique Ability of Large Language Models](https://mlsanity.com/paper/2505.23715/) (2025)
- [Pause or Fabricate? Training Language Models for Grounded Reasoning](https://mlsanity.com/paper/2604.19656/) (2026)

## Abstract (arXiv)

Reasoning systems usually treat premise use as a question of relevance: if a fact is available and useful, it may be selected for inference. Authorization imposes a different constraint: a premise may be represented and logically usable but not permitted for a particular local transition. We formalize this distinction as Governed Deduction (GD), with a transition-local admission predicate admit(p, tau, S). From an independently produced RBAC-augmented Spider benchmark, we construct 4,461 matched authorization pairs in which the same query premise and policy state support permitted and denied consuming transitions. An initial joint controller reaches 99.19% held-out accuracy, but a transition-only control reaches 100%, exposing a role-name shortcut. After a frozen, label-independent context-local role permutation removes that shortcut, premise/state-only, transition-only, and joint linear controllers all score exactly 50% on 1,856 held-out edges, while a symbolic policy oracle remains at 100%. The result is a controlled negative finding: the benchmark instantiates policy-grounded authorization beyond relevance, but the frozen linear representation does not recover the relation. Matched one-sided controls and leakage audits are therefore essential for evaluating learned policy-sensitive reasoning.