5 papers
Symbolic-Neural Soft-Logic Reasoning: Towards Robust and Verifiable Thinking Chains via Cooperative Evolution
Rui Wang, Zeming Wei, Yihao Zhang +1
Large Language Models (LLMs) have demonstrated impressive progress in complex reasoning tasks, largely driven by the Chain-of-Thought (CoT) paradigm, which decomposes difficult pro…
Neural Theorem Proving for Verification Conditions: A Real-World Benchmark
Qiyuan Xu, Xiaokun Luan, Renxi Wang +5
Theorem proving is fundamental to program verification, where the automated proof of Verification Conditions (VCs) remains a primary bottleneck. Real-world program verification fre…
Generically Automating Separation Logic by Functors, Homomorphisms and Modules
Qiyuan Xu, David Sanan, Zhe Hou +3
Foundational verification considers the functional correctness of programming languages with formalized semantics and uses proof assistants (e.g., Coq, Isabelle) to certify proofs.…
Psychometric-Based Evaluation for Theorem Proving with Large Language Models
Jianyu Zhang, Yongwang Zhao, Long Zhang +4
Large language models (LLMs) for formal theorem proving have become a prominent research focus. At present, the proving ability of these LLMs is mainly evaluated through proof pass…
The Fusion of Large Language Models and Formal Methods for Trustworthy AI Agents: A Roadmap
Yedi Zhang, Yufan Cai, Xinyue Zuo +9
Large Language Models (LLMs) have emerged as a transformative AI paradigm, profoundly influencing daily life through their exceptional language understanding and contextual generat…