4 papers
On Reasoning-Centric LLM-based Automated Theorem Proving
Yican Sun, Chengwei Shi, Hangzhou Lyu +1
Automated theorem proving is fundamental to formal methods, and the recent trend is to integrate large language models (LLMs) and proof assistants to form effective proof agents. W…
Proof Strategy Extraction from LLMs for Enhancing Symbolic Provers
Jian Fang, Yican Sun, Yingfei Xiong
One important approach to software verification is interactive theorem proving. However, writing formal proofs often requires substantial human effort, making proof automation high…
VeriStruct: AI-assisted Automated Verification of Data-Structure Modules in Verus
Chuyue Sun, Yican Sun, Daneshvar Amrollahi +5
We introduce VeriStruct, a novel framework that extends AI-assisted automated verification from single functions to more complex data structure modules in Verus. VeriStruct employs…
GramTrans: A Better Code Representation Approach in Code Generation
Zhao Zhang, Qingyuan Liang, Zeyu Sun +6
Code generation has shown great promise in assisting software development. A fundamental yet underexplored question is how the choice of code representation affects model performan…