7 papers
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…
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…
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…
Learning Rules Explaining Interactive Theorem Proving Tactic Prediction
Liao Zhang, David M. Cerna, Cezary Kaliszyk
Formally verifying the correctness of mathematical proofs is more accessible than ever, however, the learning curve remains steep for many of the state-of-the-art interactive theor…
Automated Strategy Invention for Confluence of Term Rewrite Systems
Liao Zhang, Fabian Mitterwallner, Jan Jakubuv +1
Term rewriting plays a crucial role in software verification and compiler optimization. With dozens of highly parameterizable techniques developed to prove various system propertie…
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…
Online Machine Learning Techniques for Coq: A Comparison
Liao Zhang, Lasse Blaauwbroek, Bartosz Piotrowski +3
We present a comparison of several online machine learning techniques for tactical learning and proving in the Coq proof assistant. This work builds on top of Tactician, a plugin f…