Gpass: a Goal-adaptive Neural Theorem Prover based on Coq for Automated Formal Verification
Formal Methods
Formal verification is a crucial means to assure software quality. Regrettably, the manual composition of verification scripts proves to be both laborious and time-consuming. In response, researchers have put forth automated theorem prover approaches; however, these approaches still grapple with several limitations. These limitations encompass insufficient handling of lengthy proof steps, difficulty in aligning the various components of a Coq program with the requirements and constraints of the proof goal, and inefficiencies. To surmount these limitations, we present Gpass, a goal-adaptive neural theorem prover based on deep learning technology. Firstly, we design a unique sequence encoder for Gpass that completely scans previous proof tactics through multiple sliding windows and provides information related to the current proof step. Secondly, Gpass incorporates a goal-adaptive feature integration module to align the reasoning process with the requirements of the proof goal. Finally, we devise a parameter selection method based on loss values and loss slopes to procure parameter sets with diverse distributions, thereby facilitating the exploration of various proof tactics. Experimental results demonstrate that Gpass attains better performance on the extensive CoqGym benchmark and proves 11.03%-96.37% more theorems than the prior work most closely related to ours. We find that the orthogonality between Gpass and CoqHammer proves their complementary capabilities, and together they prove a total of 3,774 theorems, which is state-of-the-art performance. In addition, we propose an efficiency optimisation approach that allows Gpass to achieve performance beyond Diva at one-sixth of the parameter sets.
Wed 30 AprDisplayed time zone: Eastern Time (US & Canada) change
11:00 - 12:30 | Formal Methods 1Research Track / New Ideas and Emerging Results (NIER) at 103 Chair(s): Cristian Cadar Imperial College London | ||
11:00 15mTalk | SpecGen: Automated Generation of Formal Program Specifications via Large Language ModelsFormal Methods Research Track Lezhi Ma Nanjing University, Shangqing Liu Nanyang Technological University, Yi Li Nanyang Technological University, Xiaofei Xie Singapore Management University, Lei Bu Nanjing University | ||
11:15 15mTalk | Gpass: a Goal-adaptive Neural Theorem Prover based on Coq for Automated Formal VerificationFormal Methods Research Track Yizhou Chen Peking University, Zeyu Sun Institute of Software, Chinese Academy of Sciences, Guoqing Wang Peking University, Dan Hao Peking University | ||
11:30 15mTalk | AI-Assisted Autoformalization of Combinatorics Problems in Proof AssistantsFormal Methods New Ideas and Emerging Results (NIER) | ||
11:45 15mTalk | Formally Verified Binary-level Pointer AnalysisFormal Methods Research Track Freek Verbeek Open Universiteit & Virginia Tech, Ali Shokri Virginia Tech, Daniel Engel Open University Of The Netherlands, Binoy Ravindran Virginia Tech | ||
12:00 15mTalk | EffBT: An Efficient Behavior Tree Reactive Synthesis and Execution FrameworkFormal Methods Research Track ziji wu National University of Defense Technology, yu huang National University of Defense Technology, peishan huang National University of Defense Technology, shanghua wen National University of Defense Technology, minglong li National University of Defense Technology, Ji Wang National University of Defense Technology | ||
12:15 7mTalk | SolSearch: An LLM-Driven Framework for Efficient SAT-Solving Code GenerationFormal Methods New Ideas and Emerging Results (NIER) Junjie Sheng East China Normal University, Yanqiu Lin East China Normal University, Jiehao Wu East China Normal University, Yanhong Huang East China Normal University, Jianqi Shi East China Normal University, Min Zhang East China Normal University, Xiangfeng Wang East China Normal University | ||
12:22 7mTalk | Listening to the Firehose: Sonifying Z3’s Behavior New Ideas and Emerging Results (NIER) |