Showing 2024Show all
3 papers · 1 filter
cs.LO2024
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…
cs.LO2024
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…
cs.PL2024
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…