Hao-Yu Li

SWE-Proof: Can Language Models Resolve Real-World Issues with Machine-Checked Proofs?

Ensuring the correctness of LLM-generated code is a core challenge for modern software engineering. Benchmarks for agentic code generation check correctness with held-out test suites, which are inherently incomplete and increasingly susceptible to memorization. Formal verification avoids both problems, but existing wor...