4 papers
A Learning Method for Symbolic Systems Using Large Language Models
Jian Fang, Yixun Yao, Yingfei Xiong
Automated theorem proving is essential for the formal verification of safety-critical systems. As the corpus of formal proofs grows, a natural paradigm is to learn from existing pr…
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…
Equality Saturation Guided by Large Language Models
Wentao Peng, Ruyi Ji, Yingfei Xiong
One critical issue with large language models (LLMs) is their inability to guarantee correctness. Although this problem can be addressed by applying LLMs to formal rewrite systems,…
HoarePrompt: Structural Reasoning About Program Correctness in Natural Language
Dimitrios Stamatios Bouras, Yihan Dai, Tairan Wang +2
While software requirements are often expressed in natural language, verifying the correctness of a program against such requirements is a hard and underexplored problem. Large lan…