Scalable Neural Learning for Verifiable Consistency with Temporal Specifications
Formal verification of machine learning models has attracted attention recently, and significant progress has been made on proving simple properties like robustness to small perturbations of the input features. In this context, it has also been observed that folding the verification procedure into training makes it easier to train verifiably robust models. In this paper, we extend the applicability of verified training by extending it to (1) recurrent neural network architectures and (2) complex specifications that go beyond simple adversarial robustness, particularly specifications that capture temporal properties like requiring that a robot periodically visits a charging station or that a language model always produces sentences of bounded length. Experiments show that while models trained using standard training often violate desired specifications, our verified training method produces models that both perform well (in terms of test error or reward) and can be shown to be provably consistent with specifications.
Code (0)
등록된 구현이 없습니다.
Tasks
Adversarial RobustnessLanguage ModelingLanguage ModellingSimilar Papers 제목 키워드 기반
NL2SpaTiaL: Generating Geometric Spatio-Temporal Logic Specifications from Natural Language for Manipulation Tasks
While Temporal Logic provides a rigorous verification framework for robotics, it typically operates on trajectory-level signals and does not natively represent the object-centric geometric relations that are central to m…
Spatial ReasoningSemantic ParsingLinear Temporal Logic Translation via Human-Inspired Self-Constrained Reasoning for Robot Task Specification
Many robotic tasks are temporally extended and demand precise specifications of subgoals, constraints, and their temporal ordering. Yet human operators typically communicate such tasks in natural language, which is inher…
VeriEquivBench: An Equivalence Score for Ground-Truth-Free Evaluation of Formally Verifiable Code
Formal verification is the next frontier for ensuring the correctness of code generated by Large Language Models (LLMs). While methods that co-generate code and formal specifications in formal languages, like Dafny, can,…
Code GenerationVerifiable Natural Language to Linear Temporal Logic Translation: A Benchmark Dataset and Evaluation Suite
Empirical evaluation of state-of-the-art natural-language (NL) to temporal-logic (TL) translation systems reveals near-perfect performance on existing benchmarks. However, current studies measure only the accuracy of the…
Measuring Inconsistency in Declarative Process Specifications
We address the problem of measuring inconsistency in declarative process specifications, with an emphasis on linear temporal logic on fixed traces (LTLff). As we will show, existing inconsistency measures for classical l…