Showing 2026Show all
3 papers · 1 filter
cs.PL2026
Visored: A Controlled-Natural-Language Prover for LLM-Generated Mathematics
Xiyu Zhai, Xinyi Chen, Yiping Wang +3
We present a dependent-type-based prover designed around the way LLMs (and humans) tend to write mathematics, complementing existing systems such as Lean and Rocq. Its core design…
cs.SE2026
PBT-Bench: Benchmarking AI Agents on Property-Based Testing
Lucas Jing, Xinqi Wang, Liao Zhang +1
Existing code benchmarks measure whether an agent can produce any test that reproduces a known bug, or whether it can produce a patch that fixes a described issue. Neither isolates…
cs.SE2026
Neuro-Symbolic Generation and Validation of Memory-Aware Formal Function Specifications
Liao Zhang, Tong Chen, Xiwei Wu +4
Formal verification of memory-manipulating programs critically depends on precise function specifications that capture memory states written by experts. This requirement has become…