TLA-Prover: Verifiable TLA+ Specification Synthesis via Preference-Optimized Low-Rank Adaptation
Source
Eric Spencer, Arslan Bisharat, Brian Ortiz, Khushboo Bhadauria, Mujtaba Nazari, TaiNing Wang, George K. Thiruvathukal, Konstantin Laufer, Mohammed Abuhamad
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.
articleHow well LLM-based test generation techniques perform with newer LLM versions?Michael Konstantinou, Renzo Degiovanni, Mike Papadakis
articleCost-Effective Automated Judging of Natural-Language Mathematical ProofsBenjamin Grayzel