Timezone: »
A fundamental problem in program verification concerns inferring loop invariants. The problem is undecidable and even practical instances are challenging. Inspired by how human experts construct loop invariants, we propose a reasoning framework Code2Inv that constructs the solution by multi-step decision making and querying an external program graph memory block. By training with reinforcement learning, Code2Inv captures rich program features and avoids the need for ground truth solutions as supervision. Compared to previous learning tasks in domains with graph-structured data, it addresses unique challenges, such as a binary objective function and an extremely sparse reward that is given by an automated theorem prover only after the complete loop invariant is proposed. We evaluate Code2Inv on a suite of 133 benchmark problems and compare it to three state-of-the-art systems. It solves 106 problems compared to 73 by a stochastic search-based system, 77 by a heuristic search-based system, and 100 by a decision tree learning-based system. Moreover, the strategy learned can be generalized to new programs: compared to solving new instances from scratch, the pre-trained agent is more sample efficient in finding solutions.
Author Information
Xujie Si (University of Pennsylvania)
Hanjun Dai (Georgia Tech)
Mukund Raghothaman (University of Pennsylvania)
Mayur Naik (University of Pennsylvania)
Le Song (Ant Financial & Georgia Institute of Technology)
Related Events (a corresponding poster, oral, or spotlight)
-
2018 Poster: Learning Loop Invariants for Program Verification »
Thu. Dec 6th through Fri the 7th Room Room 210 #23
More from the Same Authors
-
2021 : Scallop: From Probabilistic Deductive Databases to Scalable Differentiable Reasoning »
Jiani Huang · Ziyang Li · Binghong Chen · Karan Samel · Mayur Naik · Le Song · Xujie Si -
2021 : Large Scale Coordination Transfer for Cooperative Multi-Agent Reinforcement Learning »
Ethan Wang · Binghong Chen · Le Song -
2022 Poster: Uncovering the Structural Fairness in Graph Contrastive Learning »
Ruijia Wang · Xiao Wang · Chuan Shi · Le Song -
2021 : Numerical Reasoning over Legal Contracts via Relational Database »
Jiani Huang · Ziyang Li · Ilias Fountalis · Mayur Naik -
2021 Poster: A Biased Graph Neural Network Sampler with Near-Optimal Regret »
Qingru Zhang · David Wipf · Quan Gan · Le Song -
2021 Poster: Locality Sensitive Teaching »
Zhaozhuo Xu · Beidi Chen · Chaojian Li · Weiyang Liu · Le Song · Yingyan Lin · Anshumali Shrivastava -
2021 Poster: Multi-task Learning of Order-Consistent Causal Graphs »
Xinshi Chen · Haoran Sun · Caleb Ellington · Eric Xing · Le Song -
2021 Poster: RoMA: Robust Model Adaptation for Offline Model-based Optimization »
Sihyun Yu · Sungsoo Ahn · Le Song · Jinwoo Shin -
2021 Poster: Scallop: From Probabilistic Deductive Databases to Scalable Differentiable Reasoning »
Jiani Huang · Ziyang Li · Binghong Chen · Karan Samel · Mayur Naik · Le Song · Xujie Si -
2020 Poster: Understanding Deep Architecture with Reasoning Layer »
Xinshi Chen · Yufei Zhang · Christoph Reisinger · Le Song -
2020 Poster: The Devil is in the Detail: A Framework for Macroscopic Prediction via Microscopic Models »
Yingxiang Yang · Negar Kiyavash · Le Song · Niao He -
2020 Spotlight: The Devil is in the Detail: A Framework for Macroscopic Prediction via Microscopic Models »
Yingxiang Yang · Negar Kiyavash · Le Song · Niao He -
2019 Workshop: Learning with Temporal Point Processes »
Manuel Rodriguez · Le Song · Isabel Valera · Yan Liu · Abir De · Hongyuan Zha -
2019 Poster: Learning Transferable Graph Exploration »
Hanjun Dai · Yujia Li · Chenglong Wang · Rishabh Singh · Po-Sen Huang · Pushmeet Kohli -
2019 Poster: Neural Similarity Learning »
Weiyang Liu · Zhen Liu · James Rehg · Le Song -
2019 Poster: Meta Architecture Search »
Albert Shaw · Wei Wei · Weiyang Liu · Le Song · Bo Dai -
2019 Poster: Exponential Family Estimation via Adversarial Dynamics Embedding »
Bo Dai · Zhen Liu · Hanjun Dai · Niao He · Arthur Gretton · Le Song · Dale Schuurmans -
2019 Poster: Retrosynthesis Prediction with Conditional Graph Logic Network »
Hanjun Dai · Chengtao Li · Connor Coley · Bo Dai · Le Song -
2018 Poster: Cooperative neural networks (CoNN): Exploiting prior independence structure for improved classification »
Harsh Shrivastava · Eugene Bart · Bob Price · Hanjun Dai · Bo Dai · Srinivas Aluru -
2018 Poster: Coupled Variational Bayes via Optimization Embedding »
Bo Dai · Hanjun Dai · Niao He · Weiyang Liu · Zhen Liu · Jianshu Chen · Lin Xiao · Le Song -
2018 Poster: Learning Temporal Point Processes via Reinforcement Learning »
Shuang Li · Shuai Xiao · Shixiang Zhu · Nan Du · Yao Xie · Le Song -
2018 Spotlight: Learning Temporal Point Processes via Reinforcement Learning »
Shuang Li · Shuai Xiao · Shixiang Zhu · Nan Du · Yao Xie · Le Song -
2018 Poster: Learning towards Minimum Hyperspherical Energy »
Weiyang Liu · Rongmei Lin · Zhen Liu · Lixin Liu · Zhiding Yu · Bo Dai · Le Song -
2017 : Learning from Conditional Distributions via Dual Embeddings (poster). »
Le Song -
2017 Poster: Predicting User Activity Level In Point Processes With Mass Transport Equation »
Yichen Wang · Xiaojing Ye · Hongyuan Zha · Le Song -
2017 Poster: Learning Combinatorial Optimization Algorithms over Graphs »
Elias Khalil · Hanjun Dai · Yuyu Zhang · Bistra Dilkina · Le Song -
2017 Spotlight: Learning Combinatorial Optimization Algorithms over Graphs »
Elias Khalil · Hanjun Dai · Yuyu Zhang · Bistra Dilkina · Le Song -
2017 Poster: Deep Hyperspherical Learning »
Weiyang Liu · Yan-Ming Zhang · Xingguo Li · Zhiding Yu · Bo Dai · Tuo Zhao · Le Song -
2017 Poster: On the Complexity of Learning Neural Networks »
Le Song · Santosh Vempala · John Wilmes · Bo Xie -
2017 Spotlight: Deep Hyperspherical Learning »
Weiyang Liu · Yan-Ming Zhang · Xingguo Li · Zhiding Yu · Bo Dai · Tuo Zhao · Le Song -
2017 Spotlight: On the Complexity of Learning Neural Networks »
Le Song · Santosh Vempala · John Wilmes · Bo Xie -
2017 Poster: Wasserstein Learning of Deep Generative Point Process Models »
Shuai Xiao · Mehrdad Farajtabar · Xiaojing Ye · Junchi Yan · Xiaokang Yang · Le Song · Hongyuan Zha -
2016 Poster: Multistage Campaigning in Social Networks »
Mehrdad Farajtabar · Xiaojing Ye · Sahar Harati · Le Song · Hongyuan Zha -
2016 Poster: Coevolutionary Latent Feature Processes for Continuous-Time User-Item Interactions »
Yichen Wang · Nan Du · Rakshit Trivedi · Le Song -
2015 Poster: Time-Sensitive Recommendation From Recurrent User Activities »
Nan Du · Yichen Wang · Niao He · Jimeng Sun · Le Song -
2015 Poster: Scale Up Nonlinear Component Analysis with Doubly Stochastic Gradients »
Bo Xie · Yingyu Liang · Le Song -
2015 Poster: Efficient Learning of Continuous-Time Hidden Markov Models for Disease Progression »
Yu-Ying Liu · Shuang Li · Fuxin Li · Le Song · James Rehg -
2015 Poster: COEVOLVE: A Joint Point Process Model for Information Diffusion and Network Co-evolution »
Mehrdad Farajtabar · Yichen Wang · Manuel Rodriguez · Shuang Li · Hongyuan Zha · Le Song -
2015 Oral: COEVOLVE: A Joint Point Process Model for Information Diffusion and Network Co-evolution »
Mehrdad Farajtabar · Yichen Wang · Manuel Rodriguez · Shuang Li · Hongyuan Zha · Le Song -
2015 Poster: M-Statistic for Kernel Change-Point Detection »
Shuang Li · Yao Xie · Hanjun Dai · Le Song -
2014 Poster: Active Learning and Best-Response Dynamics »
Maria-Florina F Balcan · Christopher Berlind · Avrim Blum · Emma Cohen · Kaushik Patnaik · Le Song -
2014 Poster: Learning Time-Varying Coverage Functions »
Nan Du · Yingyu Liang · Maria-Florina F Balcan · Le Song -
2014 Poster: Shaping Social Activity by Incentivizing Users »
Mehrdad Farajtabar · Nan Du · Manuel Gomez Rodriguez · Isabel Valera · Hongyuan Zha · Le Song -
2014 Poster: Scalable Kernel Methods via Doubly Stochastic Gradients »
Bo Dai · Bo Xie · Niao He · Yingyu Liang · Anant Raj · Maria-Florina F Balcan · Le Song -
2013 Poster: Robust Low Rank Kernel Embeddings of Multivariate Distributions »
Le Song · Bo Dai -
2013 Poster: Scalable Influence Estimation in Continuous-Time Diffusion Networks »
Nan Du · Le Song · Manuel Gomez Rodriguez · Hongyuan Zha -
2013 Oral: Scalable Influence Estimation in Continuous-Time Diffusion Networks »
Nan Du · Le Song · Manuel Gomez Rodriguez · Hongyuan Zha -
2012 Workshop: Confluence between Kernel Methods and Graphical Models »
Le Song · Arthur Gretton · Alexander Smola -
2012 Workshop: Spectral Algorithms for Latent Variable Models »
Ankur P Parikh · Le Song · Eric Xing -
2012 Poster: Learning Networks of Heterogeneous Influence »
Nan Du · Le Song · Alexander Smola · Ming Yuan -
2012 Spotlight: Learning Networks of Heterogeneous Influence »
Nan Du · Le Song · Alexander Smola · Ming Yuan