TLA-Prover: Verifiable TLA+ Specification Synthesis via Preference-Optimized Low-Rank Adaptation
Source
arxiv.org
Author
Eric Spencer, Arslan Bisharat, Brian Ortiz, Khushboo Bhadauria, Mujtaba Nazari, TaiNing Wang, George K. Thiruvathukal, Konstantin Laufer, Mohammed Abuhamad
Date
Why it matters
Across 25 LLMs only 8.6% of generated TLA+ specs survive the TLC model checker. Using TLC itself as the reward signal, plus a grading tier that mutates the property to expose always-true specs, lifts pass@1 to 30% on held-out problems.
articleWhat TLA+ can and can't checkb-man
articleAre the Financial Reasoning from LLMs Credible? A Real World Test over Long-Horizon StatementsXinke Tong, Xuanming Zhang, Tianyi Tang, An Yang, Jiatu Hu, Guojie Lin, Zhenzhen Shi, Lingfeng Zeng, Boyu Yang, Bing Zhao, Hu Wei, Lin Qu, Dayiheng Liu
articleCode Transformation Rule Synthesis using LLMs: Potential and LimitsAxel Allain, Aymeric Blot, Djamel Eddine Khelladi, Mathieu Acher