arXiv Science⌕ Search
Home/Archive/arXiv

arXiv · 2610.19701

Runtime Monitoring of Supermartingale Certificates

Mirco Giacobbe·Thomas A. Henzinger·Konstantin Kueffner·Emily Yu·Đorđe Žikelić
View original source ↗Read source document ↗Export metadata ↓

Abstract

Supermartingale certificates formally guarantee temporal properties of discrete and continuous-time stochastic dynamical systems. However, these guarantees rely on a mathematical model of the world, leaving a sim-to-real gap that can invalidate them for the deployed system. We formulate the runtime monitoring problem for supermartingale certificates, in which a monitor observes a single system trajectory and raises an alarm when there is sufficient statistical evidence that the supermartingale certificate has been violated during execution. We present an algorithm to automatically construct a monitor using betting-based sequential tests that bound the probability of ever raising a false alarm at a user-specified level. Within this betting framework, we formulate strategies that allow the monitor to exploit spatial regularity to improve detection power while preserving this statistical guarantee. We demonstrate the efficacy of our approach on supermartingale certificate benchmarks from the literature.

Explore related subjects

cs.AIcs.SYeess.SY

Keep this discovery

Explore connections, maps & timelines

BibTeXRIS

Mirco Giacobbe, Thomas A. Henzinger, Konstantin Kueffner, Emily Yu, Đorđe Žikelić. 2026-10-14. Runtime Monitoring of Supermartingale Certificates. https://arxiv.org/abs/2610.19701

Cite the original work for its findings. Save a collection to share your selection of sources.

KEEP EXPLORING

Related papers

arXiv2026

SEDM: Selective Self-Evolving Distributed Memory for Agents

Agents in a society can reuse each other's experience, but indiscriminate memory use increases processing cost and can reduce task success. We present SEDM (Selective Self-Evolving Distributed Memory), a framework that selects both what agents share and when recipients use it. On the sender side, SEDM admits memories through paired execution tests, ranks them by relevance and measured utility, and abstracts them for cross-domain reuse. On the recipient side, Calibrated Memory Gating (CMG) predicts success with and without memory in a single forward pass, learning from paired outcomes including ties. It injects memory only when the calibrated success gain outweighs a context-cost penalty. SEDM exceeds the strongest evaluated baseline on LoCoMo open-domain questions by 15.1 F1 points and outperforms G-Memory on FEVER and HotpotQA with 16-32% fewer prompt tokens. In a controlled HotpotQA study, CMG achieves success comparable to always using memory with 18% fewer agent input tokens. Within the full SEDM pipeline on LoCoMo, CMG outperforms both always-use and no-memory policies for two SEDM memories while using 19-31% fewer input tokens than always-use. These results show that selective use can recover value from shared memories that hurt performance when injected indiscriminately.

cs.AI↗
arXiv2026

Toward Agents That Reason About Their Computation

While reinforcement learning agents can achieve superhuman performance in many complex tasks, they typically do not become more computationally efficient as they improve. In contrast, humans gradually require less cognitive effort as they become more proficient at a task. If agents could reason about their compute as they learn, could they similarly reduce their computation footprint? If they could, we could have more energy efficient agents or free up compute cycles for other processes like planning. In this paper, we experiment with showing agents the cost of their computation and giving them the ability to control when they use compute. We conduct our experiments on the Arcade Learning Environment, and our results demonstrate that with the same training compute budget, agents that reason about their compute perform better on 75% of games. Furthermore, these agents use three times less compute on average. We analyze individual games and show where agents gain these efficiencies. An interactive version of this paper is available at https://adrianorenstein.com/paper/toward-compute.

cs.AI↗
arXiv2026

LingLanMedBench: A Unified Benchmark for Evaluating Large Language Models in Traditional Chinese Medicine

Reliable evaluation of large language models in traditional Chinese medicine remains limited because existing benchmarks mainly focus on examination-style question answering or isolated generative tasks. We developed LingLanMedBench, a unified benchmark comprising 25,620 expert-verified items across 13 subtasks and five domains, covering knowledge, language understanding, information extraction, and diagnostic-therapeutic decision-making. LingLanMedBench standardizes task formats and evaluation metrics and further incorporates synonym-tolerant clinical-label matching, empirically derived hard subsets, and decision-recognition reformulations of open-ended clinical tasks. Fourteen open-source and proprietary models were evaluated under a standardized zero-shot protocol. Performance varied substantially across domains, model families, task formulations, and difficulty levels. The leading overall score decreased from 51.1 on the full benchmark to 31.9 on the hard subsets. Prescription performance also differed markedly between open-ended generation, with F1 scores of 32.7 and 20.3, and decision recognition, with accuracies of 90.6 and 56.8 on the full and hard subsets, respectively. These findings reveal a substantial gap between knowledge-oriented performance and clinically faithful reasoning. LingLanMedBench provides a standardized and reproducible framework for characterizing current capabilities, identifying systematic limitations, and tracking meaningful progress in large language models for traditional Chinese medicine.

cs.AI↗