Current browse context:
cs.AI
Change to browse by:
References & Citations
Computer Science > Artificial Intelligence
Title: Learning Heuristics for Template-based CEGIS of Loop Invariants with Reinforcement Learning
(Submitted on 16 Jul 2021 (v1), last revised 15 Jun 2022 (this version, v3))
Abstract: Loop-invariant synthesis is the basis of program verification. Due to the undecidability of the problem in general, a tool for invariant synthesis necessarily uses heuristics. Despite the common belief that the design of heuristics is vital for the performance of a synthesizer, heuristics are often engineered by their developers based on experience and intuition, sometimes in an \emph{ad-hoc} manner. In this work, we propose an approach to systematically learning heuristics for template-based CounterExample-Guided Inductive Synthesis (CEGIS) with reinforcement learning. As a concrete example, we implement the approach on top of PCSat, which is an invariant synthesizer based on template-based CEGIS. Experiments show that PCSat guided by the heuristics learned by our framework not only outperforms existing state-of-the-art CEGIS-based solvers such as HoICE and the neural solver Code2Inv, but also has slight advantages over non-CEGIS-based solvers such as Eldarica and Spacer in linear Constrained Horn Clause (CHC) solving.
Submission history
From: Taro Sekiyama [view email][v1] Fri, 16 Jul 2021 11:17:05 GMT (843kb,D)
[v2] Sat, 14 Aug 2021 09:06:21 GMT (945kb,D)
[v3] Wed, 15 Jun 2022 09:32:07 GMT (1838kb,D)
Link back to: arXiv, form interface, contact.