4 ms·
A fascinating thought. But then who verifies that the TLA+ specification does indeed match the human specification? I’m guessing using an LLM as a translator n
by omneity 1y ago
A fascinating thought. But then who verifies that the TLA+ specification does indeed match the human specification?
I’m guessing using an LLM as a translator narrows the gap, and better LLMs will make it narrower eventually, but is there a way to quantify this? For example how would it compare to a human translating the spec into TLA+?
- justanotheratom 1y agomaybe run it through few other LLMs depending on how much confidence you need - o3 pro, gemini 2.5 pro, claude 3.7, grok 3, etc..
- svieira 1y agoThen you need to be able to formally prove the equivalence of various TLA+ programs (maybe that's a solved problem?)
- omneity 1y agoNo idea about SOTA but naively it doesn't seem like a very difficult problem: - Ensure all TLA+ specs produced have the same inputs/outputs (domains, mostly a prompting problem and can solved with retries) - That all TLA+ produce the same outputs for the same inputs (making them functionally equivalent in practice, might be computationally intensive) Of course that assumes your input domains are countable but it's probably okay to sample from large ranges for a certain "level" of equivalence. EDIT: Not sure how that will work with non-determinism though.
- justanotheratom 1y agoI didn't mean generate separate TLA programs. Rather, other LLMs review and comment on whether this TLA program satisfies the user's specification.
- Taikonerd 1y agoA fair question! I'd say it's not that different from using an LLM to write regular code: who verifies that the code the LLM wrote is indeed what you meant?
- fmap 1y agoThe usual way to check whether a definition is correct is to prove properties about it that you think should hold. TLA+ has good support for this, both with model checking as well as simple proofs.