paper-with-me

홈 › Papers

Scalable Neural Learning for Verifiable Consistency with Temporal Specifications

2019-09-25 · Sumanth Dathathri, Johannes Welbl, Krishnamurthy (Dj) Dvijotham, Ramana Kumar, Aditya Kanade, Jonathan Uesato, Sven Gowal, Po-Sen Huang, Pushmeet Kohli

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.

📄 PDF Abstract BibTeX

Code (0)

등록된 구현이 없습니다.

Tasks

Adversarial RobustnessLanguage ModelingLanguage Modelling

Similar Papers 제목 키워드 기반

NL2SpaTiaL: Generating Geometric Spatio-Temporal Logic Specifications from Natural Language for Manipulation Tasks

2025-12-15 · Licheng Luo, Kaier Liang, Yu Xia, Mingyu Cai arxiv

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 Parsing

Linear Temporal Logic Translation via Human-Inspired Self-Constrained Reasoning for Robot Task Specification

2026-08-28 · Haofei Hou, Fanxu Meng, Shunyi Zhao, Kairui Yang 외 arxiv

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

2025-10-07 · Lingfei Zeng, Fengdi Che, Xuhan Huang, Fei Ye 외 arxiv

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 Generation

Verifiable Natural Language to Linear Temporal Logic Translation: A Benchmark Dataset and Evaluation Suite

2025-07-01 · William H English, Chase Walker, Dominic Simon, Sumit Kumar Jha 외 arxiv

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

2022-06-14 · Carl Corea, John Grant, Matthias Thimm

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…