Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Can LLMs model real-world systems in TLA+?

sigops.org

Post reply on HN
Print view View original

31–40 of 40 posts

Re: Can LLMs model real-world systems in TLA+?

#31

Post by schaefer »

_doctor_love wrote: post #16
ofrzeta wrote: post #9

Earlier quoted context omitted.

It looks quite complicated and I have no idea what it is doing. Obviously, since I don't know about TLA+. But what about someone who knows TLA+? It still seems hard to make sure it is valid. And it's just for a relatively simple game.

There is a nice guide to TLA+ from Hillel Wayne here: https://learntla.com/ PlusCal is recommended as the gentler on-ramp to TLA+ for first learning.

From the link above, I also found Leslie Lamport's Home page[1], The original developer of TLA+. Leslie's home page contains an incredible amount of info about TLA. There's a published Book with pdf available. There are video courses and talks.

There are also git repos of examples[2] and tools[3]

Thanks for the link, _doctor_love

[1] https://lamport.azurewebsites.net/ [2] https://github.com/tlaplus/Examples [3] https://github.com/tlaplus/tlaplus/

Re: Can LLMs model real-world systems in TLA+?

#33

Post by pron »

iFire wrote: post #8

I don't use tla+ to model real-world systems anymore, Claude is able to model systems in Lean 4 and the binary executable can handle real input or I can directly generate c / rust on proofs with numeric types that have ring structure (integers, rationals, bits). https://github.com/lambdaclass/truth_research_zk

The point of TLA+ is easily readable specs with refinements. That's why it was designed in a novel way rather than in the older executable-with-more-complex-logic style that Lean (and other maths/spec languages) offer. I'm not saying you should prefer TLA+'s approach, but that's what it's meant to accomplish and LLMs don't change that.

Re: Can LLMs model real-world systems in TLA+?

#34

Post by tombert »

comex wrote: post #19
ofrzeta wrote: post #9

Earlier quoted context omitted.

It looks quite complicated and I have no idea what it is doing. Obviously, since I don't know about TLA+. But what about someone who knows TLA+? It still seems hard to make sure it is valid. And it's just for a relatively simple game.

Well, for one thing: > Decline to buy: property stays with bank (auction abstracted out) Ignoring an entire game mechanic is really stretching the definition of “abstracted out”… Also, at the bottom it defines a “Liveness: someone eventually wins” property which I believe cannot be proven. Monopoly doesn’t have any rules forcing the game to end eventually. There is only a probabilistic guarantee, and even that only a…

Yeah, I finally started thoroughly reading it this morning, and the lack of a guarantee of winning was one thing that stuck out to me as well.

I do think Claude is getting better at this stuff but I will probably keep writing the specs myself for now.

Re: Can LLMs model real-world systems in TLA+?

#35

Post by _flux »

ofrzeta wrote: post #9
tombert wrote: post #7

Claude has certainly been getting better with TLA+. It's not perfect yet but for laughs I got it to model the rules of Monopoly last night [1]. I haven't done any exhaustive checking on it yet, but it certainly looks passable. It is pretty impressive at how good it's gotten at this, in a relatively short amount of time no less. I still usually write my specs by hand, but who knows how much longer I'll be doing that.…

It looks quite complicated and I have no idea what it is doing. Obviously, since I don't know about TLA+. But what about someone who knows TLA+? It still seems hard to make sure it is valid. And it's just for a relatively simple game.

I've played a bit with having a Claude generate a TLA+ model, I review it, Claude reviews it, and then Claude checks for alignment with the actual system. The code in the system can be annotated with comments to link back to the model, and vice versa, to make human and AI review easier.

I think it's highly promising. I might even call it a success. For example, I was able to express a bug in the system and Claude was able to find me a property that would reveal that in the model; and then revise the model to eliminate that bug, and then revise the code accordinly.

Additionally (with OpenAI) I have a small guest management system I had the LLM generate a TLA+ model about the API which endpoints a client can request from it, and which tokens it learns from it (there are session ids, event ids, guest ids and invitation ids that interact in interesting ways, as guests are not required to have an invitation to the system, and they can have only magic-link protected account, resulting in different visibility on the contact details of others), and what data it can or cannot access with those tokens.

I still haven't manually verified, but it seems rather promising as well.

Re: Can LLMs model real-world systems in TLA+?

#38

Post by _doctor_love »

schaefer wrote: post #31
_doctor_love wrote: post #16

Earlier quoted context omitted.

There is a nice guide to TLA+ from Hillel Wayne here: https://learntla.com/ PlusCal is recommended as the gentler on-ramp to TLA+ for first learning.

From the link above, I also found Leslie Lamport's Home page[1], The original developer of TLA+. Leslie's home page contains an incredible amount of info about TLA. There's a published Book with pdf available. There are video courses and talks. There are also git repos of examples[2] and tools[3] Thanks for the link, _doctor_love [1] https://lamport.azurewebsites.net/ [2] https://github.com/tlaplus/Examples [3] https…

Welcome! Just one guy out here trying to be the change

Re: Can LLMs model real-world systems in TLA+?

#40

Post by Kab1r »

I've been building a TLA style Temporal Logic library for Verus (using LLMs). My experience so far is that LLMs are surprisingly useful at generating the mechanical proof scaffolding (when they're not occasionally trying to cheat with `assume(false)` statements), but they are not a substitute for knowing what property you actually want.
Post reply on HN