Showing cs.LOShow all
3 papers · 1 filter
cs.LO2025
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…
cs.LO2025
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…
cs.LO2023
Compositional Inductive Invariant Based Verification of Neural Network Controlled Systems
Yuhao Zhou, Stavros Tripakis
The integration of neural networks into safety-critical systems has shown great potential in recent years. However, the challenge of effectively verifying the safety of Neural Netw…