Meetings

[benbrastmckie]

Hey nice work this week!

I thought it would be convenient to leave some notes in a dedicated issue thread for the meetings each week. I also created a meetings file (this was just for me to prepare), but figured an issue would be easiest for small or general stuff that comes up each week, and to recap after. Here are a few points.

• The prefix function looks great, and I agree that we probably don't need an infix function, or at least can wait.
• The only remaining TODOs on the prefix function seem to be a little clean up and other wise we can move on.
• I will talk to Graham and try to get some simple Z3 solvers working with the right kind of constraints.
• I think it makes sense to focus on researching Z3 for this week, doing some reading and setting up some simple test solvers that use bitvectors.
• Hopefully next week we can start to identify constraints and design algorithms for generating those constraints.
• One other topic we only touched on at the end is how to represent states which could also be a useful thing to start thinking about (I'll open a separate issue with some thoughts.)

It's great seeing this thing slowly start to come to life. Maybe at the end we can generate a little gource video from our git logs :)

[mbuit82]

Thanks! Yeah I saw the meetings doc, looks good. I'll look at state representations. The gource video looks cool!

[benbrastmckie]

I created the file test_model.py to get a concrete model working for two sentence letters. This was the thought:

• Try to get the test model to work with appropriate model constraints.
• Abstract the generator functions that add appropriate constraints for each sentence letter.
• Add concrete semantic constraints for some explicitly given complex sentence.
• Abstract semantic constraint generator function which works through complex sentences recursively.

I was thinking we could try to get some elements of the concrete model working. I also put some questions together in the meeting notes.

[benbrastmckie]

Hey great meeting earlier! I created a file called Plan.md in the /Design/ directory with a broad outline of how to proceed, though this will probably continue to evolve.

I also updated the TODO. I should be able to revise Strategies tomorrow, and will then start working on building some concrete models. Once those are working, I think we will be in very good shape to start working on the constraint generator functions which should really open things up.

[benbrastmckie]

Hey just finished updating everything. The state fusion representations are looking great! One question I had about this definition: my linter says that "Either all return statements should return an expression or none should." I presume that means for the null state and otherwise:

''' for i, char in enumerate(bit_vec_backwards): if char == "b": if not state_repr: return "□" # null state return state_repr[0 : len(state_repr) - 1] if char == "1": state_repr += alphabet[i] state_repr += "." '''

Just wanted to check that we are all good there before moving on.

Good luck with the talk and let me know if you get stuck on any of the next TODOs. I think once we are unable to unpack the extensions of the Z3 models a lot will open up. Should be cool!

[mbuit82]

I think your linter may be complaining about the fact that in the first return statement a string is returned, not an expression representing a string (making sure that all returns return expressions is important for recursive functions but nothing else as far as I can think of). It's probably ignorable.

Thank you :) I'll let you know if I get stuck on any TODOs—it's cool seeing it start to take shape!

Also, did you manage to find the video you were talking about, where they guy inputted English to chatgpt and then fed it to Z3?

[benbrastmckie]

Hey so I fixed the merge conflict stuff and uncommented your code additions (attempt b). Also, here is the chatgpt regimentation idea:

https://www.youtube.com/watch?v=TLGEUfh6zl4&t=1s

It would be great to have a local LLM that is specifically trained and tuned for regimentation. Seems like just the kind of thing they are very good at since it is essentially translation and there is lots of data.

[benbrastmckie]

Nice work this week! The checker is coming along really nicely. I was able to merge in the definition of alt_bits pushing state version until just before printing. After removing the declaration of alternative everything is running much faster.

I'll try to work on the semantics to get that straightened out and will probably need help with parts of that once I have a better idea of what to do there. For the time being, I thought it might be helpful for you to have a go at setting up model checkers so that you can get some better sense of how the semantics works and what the shape of the challenges are for generating Z3 constraints since this is what the semantics aims to do. I included two natural choices (sat and unsat) to take a look at.

The remaining TODOs are on hold until I can sort out the semantics and figure out what is going on with the existential claims in the Z3 constraints. I suspect the semantics won't take too long, and then we can finish building and testing these constraint generator functions which will make finding models a lot easier.

[mbuit82]

Sounds good! I think the N>4 issue is taken care of, though it raised a question for me that I think you should take a look at when you get time (see the new issue called N>4).

As for the model checkers for me to set up: sounds good, I think that's a great idea—are the two choices you had in mind the two under Models in TODO.md?

[benbrastmckie]

That's great! Seems like it is working nicely. I see what you are talking about regarding the way it prints states and commented in that issue.

I added some natural entailment claims to the TODOs. I also added a more recent version of the paper to docs in case you wanted context or other cases to consider. I don't discuss all of them there, but figured it wouldn't hurt to have everything in one place. The paper itself may be distracting since we are not dealing with time at all for the time being. So I mostly included it for the examples.

As for poss_strength it is no longer crashing and the results look pretty good. I switched to non_null_verifier there and it gave no models when N=3, but found a model when N=5. So that by itself is a good result. The model itself also looks correct. The only thing that is strange is that the null state is said to be a world despite being a part of every world. So there must be some problem with the definition of world_bits.

[benbrastmckie]

Hey great meeting earlier! I updated the TODOs with some ideas, but feel free to self-assign, working on whatever feels most pressing. Some of the items would make sense to develop in separate branches. If you do create a branch, it might be good to create an issue as well (I'll do the same) which we can close once the branch is merged. It seems like the next main topics are

• reorganizing what we have already
• abstracting data structure builder from print
• refining the semantics, debugging, testing, etc

Although these projects will probably overlap, I'll focus on the semantics to try to fix what is still not working. I also want to look into finding a Z3 mentor and perhaps ssh access to some more compute power for when the time comes.

As for the design elements, I think it would be good to start to sketch out some of what we have as it is beginning to get complicated. I'll try to create a markdown document which outlines what we have already. Hopefully this will help us make design choices going forward. The idea is we could make changes to a copy of the architecture to come up with a good plan before setting about implementing that plan in a new branch.

[benbrastmckie]

Just went back through the alt_bits issue and I don't think it is an issue after all. Here's what is going on:

• we are at world a where Box A is true
• Box A is verified by the null state
• to find the Box A alternatives, the model checker looks for the biggest part of world a that is compatible with a verifier for Box A which in this case is the world a itself
• then it looks for all worlds containing that biggest part a, but there is only one such world, namely a.
• this is just what it should do
• more generally, whenever B is true at a world w, the B alternatives to w will include w.
• if B only has one verifier and that verifier is a part of w, then w is the only B alternative to w.