4 papers
AoA: Theorem Proving Agent over Abstract Syntax Tree of Redesigned Language
Qiyuan Xu, Joshua Ong Jun Leang, Renxi Wang +4
Interactive theorem proving (ITP) underpins program verification and formalized mathematics, but its manual effort limits scalability. LLM-based proof agents promise to ease this e…
Pythagoras-Prover: Advancing Efficient Formal Proving via Augmented Lean Formalisation
Joshua Ong Jun Leang, Zheng Zhao, Mihaela CÄtÄlina Stoian +5
Modern Lean theorem provers achieve strong performance only with substantial training and inference compute, driven in part by scarce verified proof data and the long reasoning tra…
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…
A Minimalist Proof Language for Neural Theorem Proving over Isabelle/HOL
Qiyuan Xu, Renxi Wang, Peixin Wang +2
Neural Theorem Proving (NTP) employs LLMs to automate formal proofs in proof assistants. While LLMs have achieved relatively remarkable success in informal reasoning tasks using na…