Xiaoxue Zhu

Enhancing Neural Theorem Proving via High-Quality Proof Selection and Verifier Feedback

Recent advances in large language models have accelerated neural theorem proving (NTP). Isabelle is a mature and important formal theorem prover that has been widely used in software and hardware verification. However, progress in the Isabelle setting remains limited. Existing approaches either opti…