← Search

Xiaokun Luan

2 accepted papers

2026

Neural Theorem Proving for Verification Conditions: A Real-World Benchmark

ICLR 2026poster

Theorem proving is fundamental to program verification, where the automated proof of Verification Conditions (VCs) remains a primary bottleneck. Real-world program verification frequently encounters hard VCs that existing Automated Theorem Provers cannot prove, leading to a critical need for extensi…

Cited by 0SourcecodeScholar
2025

Position: Trustworthy AI Agents Require the Integration of Large Language Models and Formal Methods

ICML 2025poster

Large Language Models (LLMs) have emerged as a transformative AI paradigm, profoundly influencing broad aspects of daily life. Despite their remarkable performance, LLMs exhibit a fundamental limitation: hallucination—the tendency to produce misleading outputs that appear plausible. This inherent…

Cited by 0SourcePDFScholar