# The use of Alloy and LLM's **URL:** \ **Category:** Experimental\ **Created:** [March 12, 2024, 9:15am UTC](https://alloytools.discourse.group/t/the-use-of-alloy-and-llms/449 "2024-03-12T09:15:19Z")\ **Posts on this page:** 6\ **Page:** 1
**Author:** ![peter.kriens](https://yyz2.discourse-cdn.com/free1/user_avatar/alloytools.discourse.group/peter.kriens/32/3_2.png) [@peter.kriens](https://alloytools.discourse.group/u/peter.kriens)\ **Post date:** [March 12, 2024, 9:15am UTC](https://alloytools.discourse.group/t/the-use-of-alloy-and-llms/449/1 "2024-03-12T09:15:19Z")
I’ve been heavily engaged with GPT-4 recently. It is fascinating how much it knows but trying to use it in a real setting (controlling the Eclipse IDE) it is a nightmare, it does some things surprisingly well but then makes the most basic mistakes. Thank god there is git to restore the workspace previous state. Interestingly, it is quite good at correcting a mistake after a proper diagnosis or a _counter example_. It often feels like an open loop system where the human is supposed to be the feedback provider. Sadly, this requires extensive knowledge by the ‘clever Hans’ (as this mechanism is called). I wonder if we could use Alloy as the ‘clever Hans’? If the LLM generates an Alloy program we could generate counter examples and feed these back. GPT-4 can generate Alloy models but they are usually not very clever or good but I think with a thorough description of the Alloy language and maybe extensively training an LLM? Clearly the syntax does not have to be Alloy, the idea is to be able to generate counter examples so the LLM is confronted with the consequences of its proposals. Is anybody else thinking along these lines? ---
**Author:** ![awwaiid](https://yyz2.discourse-cdn.com/free1/user_avatar/alloytools.discourse.group/awwaiid/32/222_2.png) [@awwaiid](https://alloytools.discourse.group/u/awwaiid)\ **Post date:** [March 15, 2024, 9:53pm UTC](https://alloytools.discourse.group/t/the-use-of-alloy-and-llms/449/2 "2024-03-15T21:53:54Z")
Hi! This is exactly what I’m going to be working on starting in a week – I’ve enrolled at [The Recurse Center](https://recurse.com) for a 6-week (March 25 - May 3) professional sabbatical. I have lots of ideas, but generally I’m playing in this space of Formal Models integrated into day-to-day dev settings, bridged by LLM. I generally work in Rails applications, and have good vibes with Alloy, so I’m starting with Alloy+LLM+Rails. Pre-gaming in research a bit, this is very aligned with the work that [Sullivan](https://allisonius.github.io/) is doing at [SCOPE Lab](https://scopelabuta.github.io/), and I’ve run into other Rails+Alloy projects too, such as Near’s earlier work on [Rubicon](https://dl.acm.org/doi/10.1145/2393596.2393667), a (defunct) ruby RSpec DSL that integrates Alloy into working test suites. I’m imagining taking a working codebase (say a Rails app), extracting one or more Alloy models using LLM stuff, maybe also taking some direction of what we want to explore / prove / disprove, and then generate back unit tests (say Rspec tests) that pass/fail as expected. In Rails this might be focused on the models, API interactions, existing test functionality, etc – so I’m hoping that there is _enough_ consistent structure there for the cleverness of Hans to turn into something practical. Maybe something that can get into the CI/CD pipeline. Dunno. One of my co-workers suggested focusing on cancan access control as an even more focused subset, which makes sense, and there are likely other areas. But I want to swing for the stars. I welcome ideas!!! Since I’ll be working on this more or less full time, I’m also up for direct collaboration or brainstorming on zoom and whatnot. I’ll be in Brooklyn for the duration and would be happy to buy someone an IRL coffee if they wanna talk Alloy+LLM+Rails or some overlap therein 🙂 ---
**Author:** ![peter.kriens](https://yyz2.discourse-cdn.com/free1/user_avatar/alloytools.discourse.group/peter.kriens/32/3_2.png) [@peter.kriens](https://alloytools.discourse.group/u/peter.kriens)\ **Post date:** [March 18, 2024, 10:00am UTC](https://alloytools.discourse.group/t/the-use-of-alloy-and-llms/449/3 "2024-03-18T10:00:37Z")
This sounds incredibly interesting! You’re moving in a direction, I think that I also tried to pursue in Java. Some of my thoughts are in this video: [https://www.youtube.com/watch?v=\_j3SdIGqYG8](https://www.youtube.com/watch?v=_j3SdIGqYG8) This post was, however, more in the direction of letting the LLM make a proposal/plan in Alloy and then creating an instance and feed it back. Anyway, keep us posted, or keep me posted (peter.kriens@aqute.biz), very interested in these efforts. ---
**Author:** ![awwaiid](https://yyz2.discourse-cdn.com/free1/user_avatar/alloytools.discourse.group/awwaiid/32/222_2.png) [@awwaiid](https://alloytools.discourse.group/u/awwaiid)\ **Post date:** [March 28, 2024, 2:08pm UTC](https://alloytools.discourse.group/t/the-use-of-alloy-and-llms/449/4 "2024-03-28T14:08:12Z")
What a delightful video @peter.kriens! Yes, this is definitely the same area that I’m exploring here. I’m doing exploration on what interactions can be very practical, and on what layer (cli, embedded in test suite, ci/cd). Once I’ve got a few ideas I’d love to chat live in the next few weeks – I’ll email to coordinate but will also post here a public zoom that anyone interested will be welcome to join as an ad-hoc demo and discussion group. Anyone else working in this space? ---
**Author:** ![ioyou](https://yyz2.discourse-cdn.com/free1/user_avatar/alloytools.discourse.group/ioyou/32/230_2.png) [@ioyou](https://alloytools.discourse.group/u/ioyou)\ **Post date:** [May 4, 2024, 10:42am UTC](https://alloytools.discourse.group/t/the-use-of-alloy-and-llms/449/5 "2024-05-04T10:42:53Z")
@awwaiid, it’s been a while, and I was wondering if you have any feedback based on your experience at RC =) I came across this [article](https://arxiv.org/pdf/2404.11050), which seems to give a taste of the possibilities of repairing (or generating) Alloy specs. I want to apply that to TLA+ in the future. ---
**Author:** ![NganTran-0017](https://yyz2.discourse-cdn.com/free1/user_avatar/alloytools.discourse.group/ngantran-0017/32/250_2.png) [@NganTran-0017](https://alloytools.discourse.group/u/NganTran-0017)\ **Post date:** [September 30, 2024, 2:58pm UTC](https://alloytools.discourse.group/t/the-use-of-alloy-and-llms/449/6 "2024-09-30T14:58:26Z")
Hi, I am working in the same direction that @peter.kriens mentioned above. It would be great if we can connect and talk about it via Zoom. Ps: Thank you @peter.kriens for sharing the video! Thanks, Natalie Tran