3 papers
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
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…
cs.PL2025
Transformers are Efficient Compilers, Provably
Xiyu Zhai, Runlong Zhou, Liao Zhang +1
Transformer-based large language models (LLMs) have demonstrated surprisingly robust performance across a wide range of language-related tasks, including programming language under…