6 papers
TLA+-Bench: An Execution-Grounded Benchmark and Dataset for Natural-Language to TLA Specification Generation
Arslan Bisharat, Eric Spencer, Brian Ortiz +8
Large language models increasingly write TLA formal specifications from natural-language descriptions, but progress is hard to measure: existing resources grade by resemblanc…
TLA-Prover: Verifiable TLA+ Specification Synthesis via Preference-Optimized Low-Rank Adaptation
Eric Spencer, Arslan Bisharat, Brian Ortiz +6
TLA+ is a formal specification language for verifying distributed systems and safety-critical protocols. Large language models (LLMs) frequently produce TLA+ specifications that fa…
Can LLMs Write Correct TLA+ Specifications? Evaluating Natural-Language-to-TLA+ Generation
Arslan Bisharat, Brian Ortiz, Eric Spencer +5
TLA+ has supported industrial verification at companies such as Amazon and Microsoft, yet writing correct TLA+ specifications from natural language still requires time and expertis…
SysLLMatic: Large Language Models are Software System Optimizers
Huiyun Peng, Arjun Gupte, Ryan Hasler +7
Automatic software system optimization can improve software speed, reduce operating costs, and save energy. Traditional approaches to optimization rely on manual tuning and compile…
Can Large-Language Models Help us Better Understand and Teach the Development of Energy-Efficient Software?
Ryan Hasler, Konstantin Läufer, George K. Thiruvathukal +5
Computing systems are consuming an increasing and unsustainable fraction of society's energy footprint, notably in data centers. Meanwhile, energy-efficient software engineering te…
Large Language Models for Energy-Efficient Code: Emerging Results and Future Directions
Huiyun Peng, Arjun Gupte, Nicholas John Eliopoulos +8
Energy-efficient software helps improve mobile device experiences and reduce the carbon footprint of data centers. However, energy goals are often de-prioritized in order to meet o…