LASER: Defeasible Certificate Search for Long-Range Protocol Dependencies
Not on the map. Why?
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.
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
20 of 28 references.
References · 20
- 2022ReAct: Synergizing Reasoning and Acting in Language Modelscited by 8,695
- 2023Toolformer: Language Models Can Teach Themselves to Use Toolscited by 4,182
- 2023Lost in the Middle: How Language Models Use Long Contextscited by 3,455
- 2023Self-RAG: Learning to Retrieve, Generate, and Critique through Self-Reflectioncited by 1,839
- 2023LongBench: A Bilingual, Multitask Benchmark for Long Context Understandingcited by 1,417
- 2022Program of Thoughts Prompting: Disentangling Computation from Reasoning for Numerical Reasoning Taskscited by 1,076
- 2022Interleaving Retrieval with Chain-of-Thought Reasoning for Knowledge-Intensive Multi-Step Questionscited by 923
- 2017Selective Classification for Deep Neural Networkscited by 852
- 2024RAPTOR: Recursive Abstractive Processing for Tree-Organized Retrievalcited by 532
- 2024Adaptive-RAG: Learning to Adapt Retrieval-Augmented Large Language Models through Question Complexitycited by 451
- 2023LeanDojo: Theorem Proving with Retrieval-Augmented Language Modelscited by 427
- 2023Logic-LM: Empowering Large Language Models with Symbolic Solvers for Faithful Logical Reasoningcited by 391
8 more
- 2022Selection-Inference: Exploiting Large Language Models for Interpretable Logical Reasoningcited by 334
- 2020ProofWriter: Generating Implications, Proofs, and Abductive Statements over Natural Languagecited by 324
- 2020Transformers as Soft Reasoners over Languagecited by 270
- 2023LINC: A Neurosymbolic Approach for Logical Reasoning by Combining Language Models with First-Order Logic Proverscited by 168
- 2020Answering Complex Open-Domain Questions with Multi-Hop Dense Retrievalcited by 162
- 2021ProoFVer: Natural Logic Theorem Proving for Fact Verificationcited by 53
- 2022Automated Attack Synthesis by Extracting Finite State Machines from Protocol Specification Documentscited by 8
- 2026SecGoal: A Benchmark for Extracting Formalizable Security Goals from Protocol Documentscited by 1
Built on by
Not cited yet.