7 papers
Cycle-Consistent Neural Explanation of Formal Verification Certificates
Andoni Rodriguez, Alberto Pozanco, Daniel Borrajo
Formal verification produces machine-checkable certificates that attest to the satisfaction or violation of temporal properties, yet these certificates remain opaque to non-special…
Is Your Agent Playing Dead? Deployed LLM Agents Exhibit Constraint-Evasive Fabrication and Thanatosis
Andoni RodrÃguez, Alberto Pozanco, Daniel Borrajo
This paper presents and characterizes a spectrum of previously unreported behaviours we term Constraint-Evasive Fabrication (CEF): when an LLM agent operates under irreconcilable c…
Explanations for Unrealizability of Infinite-State Safety Shields
Andoni Rodriguez, Irfansha Shaik, Davide Corsi +2
Safe Reinforcement Learning focuses on developing optimal policies while ensuring safety. A popular method to address such task is shielding, in which a correct-by-construction saf…
Efficient Dynamic Shielding for Parametric Safety Specifications
Davide Corsi, Kaushik Mallik, Andoni Rodriguez +1
Shielding has emerged as a promising approach for ensuring safety of AI-controlled autonomous systems. The algorithmic goal is to compute a shield, which is a runtime safety enforc…
Research Vision: Multi-Agent Path Planning for Cops And Robbers Via Reactive Synthesis
William Fishell, Andoni Rodriguez, Mark Santolucito
We propose the problem of multi-agent path planning for a generalization of the classic Cops and Robbers game via reactive synthesis. Specifically, through the application of LTLt…
Shield Synthesis for LTL Modulo Theories
Andoni Rodriguez, Guy Amir, Davide Corsi +2
In recent years, Machine Learning (ML) models have achieved remarkable success in various domains. However, these models also tend to demonstrate unsafe behaviors, precluding their…