# LASER: Defeasible Certificate Search for Long-Range Protocol Dependencies

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

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 20 of its 28 references that are in the map.
- First posted on arXiv 10 Oct 2026.

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

- [ReAct: Synergizing Reasoning and Acting in Language Models](https://mlsanity.com/paper/2210.03629/) (2022)
- [Toolformer: Language Models Can Teach Themselves to Use Tools](https://mlsanity.com/paper/2302.04761/) (2023)
- [Lost in the Middle: How Language Models Use Long Contexts](https://mlsanity.com/paper/2307.03172/) (2023)
- [Self-RAG: Learning to Retrieve, Generate, and Critique through Self-Reflection](https://mlsanity.com/paper/2310.11511/) (2023)
- [LongBench: A Bilingual, Multitask Benchmark for Long Context Understanding](https://mlsanity.com/paper/2308.14508/) (2023)
- [Program of Thoughts Prompting: Disentangling Computation from Reasoning for Numerical Reasoning Tasks](https://mlsanity.com/paper/2211.12588/) (2022)
- [Interleaving Retrieval with Chain-of-Thought Reasoning for Knowledge-Intensive Multi-Step Questions](https://mlsanity.com/paper/2212.10509/) (2022)
- [Selective Classification for Deep Neural Networks](https://mlsanity.com/paper/1705.08500/) (2017)
- [RAPTOR: Recursive Abstractive Processing for Tree-Organized Retrieval](https://mlsanity.com/paper/2401.18059/) (2024)
- [Adaptive-RAG: Learning to Adapt Retrieval-Augmented Large Language Models through Question Complexity](https://mlsanity.com/paper/2403.14403/) (2024)
- [LeanDojo: Theorem Proving with Retrieval-Augmented Language Models](https://mlsanity.com/paper/2306.15626/) (2023)
- [Logic-LM: Empowering Large Language Models with Symbolic Solvers for Faithful Logical Reasoning](https://mlsanity.com/paper/2305.12295/) (2023)
- [Selection-Inference: Exploiting Large Language Models for Interpretable Logical Reasoning](https://mlsanity.com/paper/2205.09712/) (2022)
- [ProofWriter: Generating Implications, Proofs, and Abductive Statements over Natural Language](https://mlsanity.com/paper/2012.13048/) (2020)
- [Transformers as Soft Reasoners over Language](https://mlsanity.com/paper/2002.05867/) (2020)
- [LINC: A Neurosymbolic Approach for Logical Reasoning by Combining Language Models with First-Order Logic Provers](https://mlsanity.com/paper/2310.15164/) (2023)
- [Answering Complex Open-Domain Questions with Multi-Hop Dense Retrieval](https://mlsanity.com/paper/2009.12756/) (2020)
- [ProoFVer: Natural Logic Theorem Proving for Fact Verification](https://mlsanity.com/paper/2108.11357/) (2021)
- [Automated Attack Synthesis by Extracting Finite State Machines from Protocol Specification Documents](https://mlsanity.com/paper/2202.09470/) (2022)
- [SecGoal: A Benchmark for Extracting Formalizable Security Goals from Protocol Documents](https://mlsanity.com/paper/2604.27601/) (2026)

## Abstract (arXiv)

Protocol specifications rarely justify executable behavior in one place: a transition may inherit its source state from a remote control block, name its events only by number, and remain subject to a later correction. Recovering the nearby clause is therefore insufficient; the system must assemble a source-linked certificate and determine whether any stronger rule applies. We introduce LASER, a proof-carrying search method for sparse, defeasible protocol evidence. LASER represents missing support and unresolved corrections as explicit obligations, searches typed evidence routes, and lets an occurrence-aware symbolic checker alone decide whether a certificate warrants, refutes, or leaves a behavior unresolved. On 91 BehaviorCheck families under a matched 2K budget, LASER improves Joint Edge+Proof over the strongest local reader on two model families (Delta=+.132, p=.017; Delta=+.198, p<.001) while cutting false discoveries by 2--3×. Controlled replays attribute the gain and its limits: neither reference routing nor deterministic citation expansion alone exceeds the local baseline; whole-document reading (29--65K tokens), two-round iterative retrieval, and even oracle minimal-certificate evidence all fail to reach LASER, localizing the bottleneck in typed obligation closure rather than evidence access. An authority-corruption replay shows source-link errors only cause abstention, while the only unsafe-warrant mechanism is mis-recording a Held erratum as Verified, confined to that erratum's family. LASER thus improves long-range dependency recovery while converting incomplete evidence and uncertain authority into explicit residual obligations rather than unsupported behavior.