4 papers
ReCrit: Transition-Aware Reinforcement Learning for Scientific Critic Reasoning
Wanghan Xu, Yuhao Zhou, Hengyuan Zhao +8
Large language models can fail in critic interaction not only by answering incorrectly, but also by abandoning an initially correct scientific solution after user criticism. This i…
Can LLMs Perform Synthesis?
Derek Egolf, Yuhao Zhou, Stavros Tripakis
How do LLMs compare with symbolic tools on program synthesis tasks? We investigate this question on several synthesis domains: LTL reactive synthesis, syntax-guided synthesis, dist…
Towards Language Model Guided TLA+ Proof Automation
Yuhao Zhou, Stavros Tripakis
Formal theorem proving with TLA+ provides rigorous guarantees for system specifications, but constructing proofs requires substantial expertise and effort. While large language mod…
Retrieval-Augmented TLAPS Proof Generation with Large Language Models
Yuhao Zhou
We present a novel approach to automated proof generation for the TLA+ Proof System (TLAPS) using Large Language Models (LLMs). Our method combines two key components: a sub-proof…