The cool thing is that you can sometimes "retcon" an existing system using this approach
So in that case you're not even making any performance concessions; the actual running code isn't changing. You're just imposing an abstraction on top of it for the purpose of analysis. The actual running code doesn't have to change for that analysis to bear fruit (e.g., quashing a bug or just increasing understanding/confidence). That's what it sounds like Hillel did with the A,B,C example in the blog post.
Another sort of funny point is that this basic trick is most often used when performance isn't acceptable, as a way of providing a modicum of stability/debugging to an ostensibly uber-optimized system which, once deployed, turns out to be kinda fragile.
Maybe I'm missing something here, but the last type matches 2 pretty well. For example,
> None of that mattered at the scope we were modeling, so we abstracted it all away: "on receiving message, nondeterministically enter state A, B, or C."
That sounds like the author is describing an NFA.
> whereby we execute all the future possibilities... e.g. "amb" operator
Isn't "execute all possibilities" closer to the dual of amb than it is to amb? At least in terms of how the denotation of amb is operationalized.
But it is a good point that sometimes you want to give an actual operational meaning to a literal non-determinism operator.
"nondeterminism as abstraction" is, imo, the best example of an "FM export".
Usually you think of nondeterminism as adding complexity to a system -- concurrency, randomness, etc.
So it's kind of surprising to notice that translating a deterministic system into a non-deterministic system is often the first step people take when proving things about complicated algorithms.
Planning, optimization and reinforcement learning are the canonical examples where the reason for this step is easiest to see. These are usually very complex algorithms. You could prove things about an actual implementation, line of code by line of code, but that would be a toooon of work.
If instead you can find over-approximation `inv : State x Action -> List[State]`, and if you know that this invariant is strong enough to imply whatever other properties you want, then you just need to make sure that `inv` over-approximates the actual behavior of the underlying system (either by interrogation or by construction).
It's a very simple observation, motivated by the pragmatics of engineering proofs about complicated systems, which can have a direct impact on how you think about designing those same systems. Now that huge inscrutable models are all the rage, it's a fun little FM trick I used almost every day even though I rarely work on systems that I'd bother to formally model or verify.
My take-away from this story is almost the opposite of yours. Nature provides a lot of valuable resources, and this story is a beautiful example of how failing to properly steward our natural environment can be extremely expensive.
> Instead, they were planning it, fighting bureocracy and wasting money for years.
I do not know anything about CZ or about this project, but jumping to "waste" seems excessively pessimistic.
It could just be that the agency's budget is finite and this project is low priority in the organization's capital projects prioritization. Just because they first planned this project 7 years ago doesn't mean they have been actively working on it continuously for the last 7 years...
This is common even in tiny economic units. E.g., I planned out our family's new furnace setup a couple of years ago, but probably won't actually allocate capital to that upgrade for another few years. In the meantime, I promise I am not spending all day every day thinking about our furnace. Just because a project takes 7 years from start of planning to finished project doesn't mean that there were 7 years of work there :)
> If the beavers built it in two days, it means that half a dozen men could have easily built it at an extremely low cost in a week.
That really depends on what you mean by "it".
I got to watch a beaver dam go up recently. Not the active work, but regular snapshots of the build site, as it were. I will use that as a case study.
If the goal here is to literally build a beaver dam, then probably you're correct. The dam I saw go up is small and built out of pretty small trees. Maybe 3-5 inch diameter. Softer wood. I think a small group of humans with very cheap tools could make quick cheap work of felling and moving the trees.
As for the dam itself, they'd figure something out. But I am skeptical that most teams would be able to build a like-quality dam out of felled trees and found materials. Beavers are dam good at what they do.
More importantly, though, building a more typical modern human dam in that same location would not be cheap or fast. You would easily spend hundreds of thousands of dollars on cutting and blasting a path before you could even get concrete to the worksite. There's no way the entire project would be done in a week. It definitely wouldn't be low cost no matter the schedule. Getting it done in a few weeks would be... probably possible, but a logistical tour de force and astronomically expensive. This is all just talking about the actual work, ignoring government permitting entirely.
The AG's advisory is essentially a memo from the AG explaining how the AG thinks existing statute applies to a new technology. It's not new legislation or new case law, but it is worth paying attention to for various reasons.
The section of the advisory referencing disproportionate impact is quoting, nearly word for word, a portion of Cal. Code Regs. Tit. 2, § 14027.
So, this section of the advisory essentially amounts to the AG saying "using AI to do something illegal is still illegal".
That does not really answer your question, though.
> What kind of standard is disproportionate impact?...
The kind that does has been codified in CA and other jurisdictions' statutes for a long while now. This means that the standard is extremely well-litigated in the state's courts, and so the answer to "what is disproportionate impact?" is, I think, something like:
"That seems complicated; there's probably a rich case law that provides clarity in some situations but also highlights areas of ambiguity in other situations. If you're in it for profit, and have any questions, get a lawyer who specializes in that area of the law to review your specific circumstance; if you're in it for civics/curiosity, start with the statute then start reading significant case law or law reviews regarding that statute."
It's also the kind of standard that can attract flame wars... hopefully not here, though ;-)
If you've been hacking on/with LLMs, please apply! The job posting casts a wide net, so please don't self-disqualify if you only check some of our boxes. Prior research experience is great but we're more interested in cool things you've built than in pdfs you've pushed through academic gauntlets :-)
> Formally proving with a system based on probabilities (temperature, etc.) is for me an oxymoron. But I am not a mathematician.
In the context of automated theorem proving, proof search and proof checking could not be more different.
Proof search is undecidable for most logics. For that reason, heuristics are commonly used to guide proof search. This has always been the case; heuristic proof search predates the use of LLMs for theorem proving by decades.
Proof checking, on the other hand, is not just decidable but usually quite tractable and cheap. Therefore, proof checkers are typically deterministic and fast. Ideally the checker is also implemented in small amount of relatively simple and heavily audited code.
> I am not sure if this is better than generating cooking recipes with a LLM and asking a cook if they make sense or not.
Conceptually it's not at all similar to asking a cook if a recipe is "correct". For lean proofs, "correct" has an entirely precise meaning. The "cook" (i.e., proof checker) is basically free (much less than $0.01/hr). The cook (proof checker) takes at most a few seconds to read and respond to any particular recipe. And the cook (i.e., checker) never makes mistakes.
The relationship between asking a cook if a recipe is good and asking Lean to check a proof is approximately the difference between asking a mediocre human computer to compute a derivative and asking a modern mechanical computer to do the same (using a classical algorithm for doing so, not an LLM; no one is using LLMs to check proofs -- there's really no point to doing so, because the checking problem is easy).
"There is a leisure class at both ends of the economic spectrum."
But even setting that aside, the article goes on to mention Albania (low CoL) and access to healthcare. The latter, in particular, checks out. I have great insurance, but my out-of-pocket max equals somewhere between 5 and 10 round-trips to Europe. It's not hard to imagine there exist people who can setup the circumstances such that working in the USA part of the year and living somewhere else part of the year is massively more economical than staying in the USA.
Actually, doesn't that exact situation describe a huge fraction of the US agricultural labor force?
So in that case you're not even making any performance concessions; the actual running code isn't changing. You're just imposing an abstraction on top of it for the purpose of analysis. The actual running code doesn't have to change for that analysis to bear fruit (e.g., quashing a bug or just increasing understanding/confidence). That's what it sounds like Hillel did with the A,B,C example in the blog post.
Another sort of funny point is that this basic trick is most often used when performance isn't acceptable, as a way of providing a modicum of stability/debugging to an ostensibly uber-optimized system which, once deployed, turns out to be kinda fragile.