Formal Methods Meet LLMs: Auditing, Monitoring, and Intervention for Compliance of Advanced AI Systems

• URL: http://arxiv.org/abs/2605.16198v1
• Date: Fri, 15 May 2026 17:13:27 GMT
• Title: Formal Methods Meet LLMs: Auditing, Monitoring, and Intervention for Compliance of Advanced AI Systems
• Abstract summary: We examine how to monitor and audit AI-enabled products and services throughout the AI development lifecycle.<n>We propose techniques that enable offline auditing and online (runtime) monitoring of product-specific (temporally extended) behavioral constraints.
• Score: 12.360375606177142
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: We examine one particular dimension of AI governance: how to monitor and audit AI-enabled products and services throughout the AI development lifecycle, from pre-deployment testing to post-deployment auditing. Combining principles from formal methods with SoTA machine learning, we propose techniques that enable AI-enabled product and service developers, as well as third party AI developers and evaluators, to perform offline auditing and online (runtime) monitoring of product-specific (temporally extended) behavioral constraints such as safety constraints, norms, rules and regulations with respect to black-box advanced AI systems, notably LLMs. We further provide practical techniques for predictive monitoring, such as sampling-based methods, and we introduce intervening monitors that act at runtime to preempt and potentially mitigate predicted violations. Experimental results show that by exploiting the formal syntax and semantics of Linear Temporal Logic (LTL), our proposed auditing and monitoring techniques are superior to LLM baseline methods in detecting violations of temporally extended behavioral constraints; with our approach, even small-model labelers match or exceed frontier LLM judges. Our predictive and intervening monitors significantly reduce the violation rates of LLM-based agents while largely preserving task performance. We further show through controlled experiments that LLMs' temporal reasoning shows a pronounced degradation in accuracy with increasing event distance, number of constraints, and number of propositions.

Related papers

• Monitoring Data-aware Temporal Properties (Extended Version) [56.386411908764494]
  We consider anticipatory monitoring of linear-time properties enriched with an arbitrary SMT theory over finite traces.<n>Anticipatory monitoring in this setting is highly challenging, as the monitoring state depends on both the trace prefix seen so far and all its possible finite continuations.<n>We present and formally prove the correctness of a novel foundational framework for monitoring properties in an expressive fragment offMT.
  arXiv  Detail & Related papers  (2026-05-14T10:23:11Z)
• On the Paradoxical Interference between Instruction-Following and Task Solving [50.75960598434753]
  Instruction following aims to align Large Language Models (LLMs) with human intent by specifying explicit constraints on how tasks should be performed.<n>We reveal a counterintuitive phenomenon: instruction following can paradoxically interfere with LLMs' task-solving capability.<n>We propose a metric, SUSTAINSCORE, to quantify the interference of instruction following with task solving.
  arXiv  Detail & Related papers  (2026-01-29T17:48:56Z)
• LLM-Assisted Logic Rule Learning: Scaling Human Expertise for Time Series Anomaly Detection [0.9740025522928777]
  Time series anomaly detection is critical for supply chain management to take proactive operations.<n>We propose a framework that leverages large language models (LLMs) to systematically encode human expertise into interpretable, logic-based rules.
  arXiv  Detail & Related papers  (2026-01-27T06:37:37Z)
• SelfAI: Building a Self-Training AI System with LLM Agents [79.10991818561907]
  SelfAI is a general multi-agent platform that combines a User Agent for translating high-level research objectives into standardized experimental configurations.<n>An Experiment Manager orchestrates parallel, fault-tolerant training across heterogeneous hardware while maintaining a structured knowledge base for continuous feedback.<n>Across regression, computer vision, scientific computing, medical imaging, and drug discovery benchmarks, SelfAI consistently achieves strong performance and reduces redundant trials.
  arXiv  Detail & Related papers  (2025-11-29T09:18:39Z)
• Architecting software monitors for control-flow anomaly detection through large language models and conformance checking [4.824526467228295]
  We propose a methodology to develop software monitors for control-flow anomaly detection.<n>The methodology builds on existing software development practices to maintain traditional V&V.<n>We test the methodology on a case-study scenario from the European Railway Traffic Management System / European Train Control System.
  arXiv  Detail & Related papers  (2025-11-14T01:11:26Z)
• Contamination Detection for VLMs using Multi-Modal Semantic Perturbation [73.76465227729818]
  Open-source Vision-Language Models (VLMs) have achieved state-of-the-art performance on benchmark tasks.<n>Pretraining corpora raise a critical concern for both practitioners and users: inflated performance due to test-set leakage.<n>We show that existing detection approaches either fail outright or exhibit inconsistent behavior.<n>We propose a novel simple yet effective detection method based on multi-modal semantic perturbation.
  arXiv  Detail & Related papers  (2025-11-05T18:59:52Z)
• Large language models require a new form of oversight: capability-based monitoring [10.382163755118713]
  Large language models (LLMs) in healthcare have been accompanied by scrutiny of their oversight.<n>We propose a new organizing principle guiding generalist LLM monitoring that is scalable and grounded in how these models are developed and used in practice: capability-based monitoring.<n>We describe considerations for developers, organizational leaders, and professional societies for implementing a capability-based monitoring approach.
  arXiv  Detail & Related papers  (2025-11-05T01:20:28Z)
• Agentic Reinforced Policy Optimization [66.96989268893932]
  Large-scale reinforcement learning with verifiable rewards (RLVR) has demonstrated its effectiveness in harnessing the potential of large language models (LLMs) for single-turn reasoning tasks.<n>Current RL algorithms inadequately balance the models' intrinsic long-horizon reasoning capabilities and their proficiency in multi-turn tool interactions.<n>We propose Agentic Reinforced Policy Optimization (ARPO), a novel agentic RL algorithm tailored for training multi-turn LLM-based agents.
  arXiv  Detail & Related papers  (2025-07-26T07:53:11Z)
• Weakly-supervised VLM-guided Partial Contrastive Learning for Visual Language Navigation [36.17444261325021]
  Visual Language Navigation (VLN) is a fundamental task within the field of Embodied AI, focusing on the ability of agents to navigate complex environments based on natural language instructions.<n>Existing methods rely on pre-trained backbone models for visual perception, which struggle with the dynamic viewpoints in VLN scenarios.<n>We propose Weakly-supervised Partial Contrastive Learning (WPCL), a method that enhances an agent's ability to identify objects from dynamic viewpoints in VLN scenarios without requiring VLM fine-tuning.
  arXiv  Detail & Related papers  (2025-06-18T11:43:50Z)
• Attribute Controlled Fine-tuning for Large Language Models: A Case Study on Detoxification [76.14641982122696]
  We propose a constraint learning schema for fine-tuning Large Language Models (LLMs) with attribute control. We show that our approach leads to an LLM that produces fewer inappropriate responses while achieving competitive performance on benchmarks and a toxicity detection task.
  arXiv  Detail & Related papers  (2024-10-07T23:38:58Z)
• Auditing large language models: a three-layered approach [0.0]
  Large language models (LLMs) represent a major advance in artificial intelligence (AI) research. LLMs are also coupled with significant ethical and social challenges. Previous research has pointed towards auditing as a promising governance mechanism.
  arXiv  Detail & Related papers  (2023-02-16T18:55:21Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.