TCSE logo 
 Sigsoft logo
Sustainability badge
Wed 30 Apr 2025 11:15 - 11:30 at 103 - Formal Methods 1 Chair(s): Cristian Cadar

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 Apr

Displayed 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
15m
Talk
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
15m
Talk
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
15m
Talk
AI-Assisted Autoformalization of Combinatorics Problems in Proof AssistantsFormal Methods
New Ideas and Emerging Results (NIER)
Long Doan George Mason University, ThanhVu Nguyen George Mason University
11:45
15m
Talk
Formally Verified Binary-level Pointer AnalysisFormal MethodsArtifact-Available
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
15m
Talk
EffBT: An Efficient Behavior Tree Reactive Synthesis and Execution FrameworkFormal MethodsArtifact-FunctionalArtifact-Available
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
7m
Talk
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
7m
Talk
Listening to the Firehose: Sonifying Z3’s BehaviorArtifact-FunctionalArtifact-ReusableArtifact-AvailableFormal Methods
New Ideas and Emerging Results (NIER)
Finn Hackett University of British Columbia, Ivan Beschastnikh University of British Columbia
:
:
:
: