Learning to Check LTL Satisfiability and to Generate Traces via Differentiable Trace Checking
This program is tentative and subject to change.
Due to the high complexity of linear temporal logic (LTL) satisfiability checking (PSPACE-complete), its applications in downstream testing tasks are limited. Neural networks are promising to approximately check LTL satisfiability in polynomial time. However, there is a lack of effective neural-network-based approaches to SAT-verifiably check LTL satisfiability, where if a formula is satisfiable, approaches generate its satisfiable trace as evidence.
In this paper, we tackle SAT-verifiable LTL satisfiability checking via bridging LTL trace checking to neural network inference. Our key theoretical contribution is to show that a well-designed neural network inference, called neural trace checking, can simulate LTL trace checking. We design a neural-network-based approach, VSCNet, which benefits from differentiable neural trace checking such that it is able to effectively jointly learn to check satisfiability and generate traces via gradient descent. Experimental results confirm the effectiveness of our theoretical contribution and show that VSCNet significantly improves the state-of-the-art performance on trace generation (at least up to $35.79%$ accuracy improvements on in-distribution datasets). Besides, in the best case, VSCNet can achieve $186$X speedup than the state-of-the-art logic-based approach nuXmv on large-scale datasets.
This program is tentative and subject to change.
Wed 18 SepDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
15:30 - 17:10 | |||
15:30 20mTalk | Learning to Check LTL Satisfiability and to Generate Traces via Differentiable Trace Checking Technical Papers Weilin Luo Sun Yat-Sen University, Pingjia Liang Sun Yat-Sen University, Qiu Junming SUN YAT-SEN UNIVERSITY, Polong Chen Sun Yat-Sen University, Hai Wan School of Data and Computer Science, Sun Yat-sen University, Jianfeng Du Guangdong University of Foreign Studies, Weiyuan Fang SUN YAT-SEN UNIVERSITY | ||
15:50 20mTalk | Interprocedural Path Complexity Analysis Technical Papers Mira Kaniyur Harvey Mudd College, Ana Cavalcante-Studart Harvey Mudd College, Yihan Yang Harvey Mudd College, Sangeon Park Harvey Mudd College, David Chen Harvey Mudd College, Duy Lam Harvey Mudd College, Lucas Bang Harvey Mudd College DOI | ||
16:10 20mTalk | VRDSynth: Synthesizing Programs for Multilingual Visually Rich Document Information Extraction Technical Papers Thanh-Dat Nguyen University of Melbourne, Tung Do-Viet Cinnamon AI, Hung Nguyen-Duy Independent Researcher, Tuan-Hai Luu Cinnamon AI, Hung Le Deakin University, Xuan-Bach D. Le University of Melbourne, Patanamon Thongtanunam University of Melbourne Pre-print | ||
16:30 20mTalk | Characterizing and Detecting Program Representation Faults of Static Analysis Frameworks Technical Papers Huaien Zhang The Hong Kong Polytechnic Universituy, Yu Pei The Hong Kong Polytechnic University, Shuyun Liang Southern University of Science and Technology, Zezhong Xing Southern University of Science and Technology, Shin Hwei Tan Concordia University | ||
16:50 20mTalk | API Misuse Detection via Probabilistic Graphical Model Technical Papers Yunlong Ma Beihang University, Wentong Tian Beihang University, Xiang Gao Beihang University, Hailong Sun Beihang University, Li Li Beihang University DOI |