3 ms·

Human Judgment as a Specification

57 points by surprisetalk 4mo ago

jMyles 4mo ago
> This is also why PICK can usefully fail. Sometimes none of the model’s candidates is right, and PICK ends with zero survivors. Under the spec-elucidation reading, that outcome means: the commitments you made through classification could not be satisfied by anything the model produced. Better to know than to ship the regex anyway. Zooming out (but only a little) from the impetus to formalize a commitment to a particular class of result candidate (what the author here is calling "spec elucidation"), we can also imagine this same evolution of concerns being applied in order to cause what we currently term "AI safety" into something more like "AI ethics". For example, if we can elucidate the specifications for things like peace and justice to ensure that the class of results is formally verified as non-participation in war (or perhaps, further in the future, non-participation in state activities whatsoever), we may be able to throw cold water on all the vitriolic arguments about model capabilities and which need to be banned or delayed lest we accelerate the apocalypse (or whatever is actually on the mind of the ban-this-model constituency). I like how the author ends tersely with: > If you have a formal language with the closure properties above — we suspect you would be surprised how many do — we would very much like to hear from you. That's certainly not me, but I bet it's true that it's somebody.
- NitpickLawyer 4mo ago
  > ensure that the class of results is formally verified as non-participation in war There are very few things that cannot be stated as dual use, with one totally benign and one totally screwed up. It's like wanting a hammer to distinguish if it's striking a nail for a roof vs. a nail for an illegal animal pen. That's the wrong application of constraints. The hammer shouldn't care.
  - jMyles 4mo ago
    The author addresses this point as well: > This is also why we do not believe PICK becomes less useful as models improve. Better models do not make user intent more articulate — asked for “a regex matching countries of North America”, a more capable model still cannot tell you whether you want the Caribbean included, or where you want to stop heading south. Better models produce better candidates, faster — which shifts user effort precisely toward the work PICK is built to support.
    - NitpickLawyer 4mo ago
      That's not I'm saying tho. I quoted the "non-participation in war" bit. I don't see how any system can ascertain if a prompt asking for an algorithm is dual use or not.
      - jMyles 4mo ago
        Well, taking the example in the article about a formal verification to determine whether a regex is for a collection of phone numbers or countries, and if a country is specified as "America", to formally verify whether that means North America or all Americas including the Caribbean: A regex which "properly" determines this in a witness/formal verification model is subject to the same sorts of political distinctions and nuances, right down to subjective interpretation of which nation-states are legitimate, etc, that participation in warfare/predation/injustice are. If the USA says that Cuba is part of the USA, and the rest of the Western Hemisphere says it's not, then the formal verification is necessarily matching the prompt intention to a social and political milieu, which, while subjective, is still cognizable and subject to introspection and, in some cases, a type of consensus. It seems similarly possible to formally verify that results do or do not meet similar subjective-but-cognizable criteria: does the result trigger engagement of weapons systems? Does it they implicate borders in a way that diminishes the sovereignty of a people? (which, like the regex example, have subjective but cognizable nuances)? Does the result serve to enrich (a perhaps pre-supplied) list of criminals/cartels/contractors/war profiteers? All of these seem like similar problems to the regex example. I don't disagree with your high-level contention that powerful dual-use technology can always cut through the good and evil in each of us. But I think that's precisely the point of searching for formally-verifiable spec-elucidation. If it were obvious from the outset whether or not a particular word represents the same of a nation-state widely regarded as sovereign, or whether an action was or was not an act of war, then we'd not need AI (let alone formal verification of a prompt-result match) in the first place.
otekengineering 4mo ago
this is the type of thing you need to build a foundation sturdy enough to let you operate higher up the stack and ratchet to design-by-metaphor and then design-by-philosophy. those design skills are taught in humanities departments, not engineering departments, so this is a weird feeling place for those of us that wandered over from a technical field.
remywang 4mo ago
> Telling people “you must read all the code generated by an LLM” is definitely meaningful—but it is not at all moderate (so most people won’t do it) But they should! The code is the best source of truth on what the software is doing after all. Instead of giving up on that, we should make it easier to read generated code, e.g. by generating less code in a higher level language. On the flip side, forcing myself to read all the code also resulted in a smaller, higher quality code base.
ekidd 4mo ago
> Telling people “you must read all the code generated by an LLM” is definitely meaningful—but it is not at all moderate (so most people won’t do it). I am honestly heartbroken to live in a world where reading the code is seen as an unreasonable ask by either students or by professional working programmers.
- sieabahlpark 4mo ago
  [dead]
- ramses0 4mo ago
  Don't tell me you're reading all assembly generated by your local golang or javac compiler? And that you've read every line of code down the dependency tree for your node_modules? I'm just upset that we are throwing away the original prompts for generated code in such a cavalier fashion.
  - wild_egg 4mo ago
    `npm install` is the OG vibecoding
  - ekidd 4mo ago
    The difference is that a compiler is a rigorous, (nearly) determinisic, heavily tested artrifact built by expert humans. I have only encountered genuine code generation bugs in compilers twice in my career. And yes, those bugs I did trace to the assembly. An LLM prompt, even a huge one, is an incredibly vague document that leaves out most of the edge cases. And even Fable 5 happily ignores clear instructions in its prompt. Now, to be fair, I absolutely expect the buggy slop to win, and to drive out the people that either write their own code or at least read the output. This will, in turn, make customers less willing to spend money on software after they get burnt a few times by buggy garbage. I think this is pretty much inevitable once Fable returns. It's just too damn good at long time horizon tasks, generating far more mostly sorta working code than any human could reasonably read.
    - warkdarrior 4mo ago

57 points by surprisetalk 4mo ago

> This is also why PICK can usefully fail. Sometimes none of the model’s candidates is right, and PICK ends with zero survivors. Under the spec-elucidation reading, that outcome means: the commitments you made through classification could not be satisfied by anything the model produced. Better to know than to ship the regex anyway. Zooming out (but only a little) from the impetus to formalize a commitment to a particular class of result candidate (what the author here is calling "spec elucidation"), we can also imagine this same evolution of concerns being applied in order to cause what we currently term "AI safety" into something more like "AI ethics". For example, if we can elucidate the specifications for things like peace and justice to ensure that the class of results is formally verified as non-participation in war (or perhaps, further in the future, non-participation in state activities whatsoever), we may be able to throw cold water on all the vitriolic arguments about model capabilities and which need to be banned or delayed lest we accelerate the apocalypse (or whatever is actually on the mind of the ban-this-model constituency). I like how the author ends tersely with: > If you have a formal language with the closure properties above — we suspect you would be surprised how many do — we would very much like to hear from you. That's certainly not me, but I bet it's true that it's somebody.

NitpickLawyer 4mo ago
> ensure that the class of results is formally verified as non-participation in war There are very few things that cannot be stated as dual use, with one totally benign and one totally screwed up. It's like wanting a hammer to distinguish if it's striking a nail for a roof vs. a nail for an illegal animal pen. That's the wrong application of constraints. The hammer shouldn't care.
- jMyles 4mo ago
  The author addresses this point as well: > This is also why we do not believe PICK becomes less useful as models improve. Better models do not make user intent more articulate — asked for “a regex matching countries of North America”, a more capable model still cannot tell you whether you want the Caribbean included, or where you want to stop heading south. Better models produce better candidates, faster — which shifts user effort precisely toward the work PICK is built to support.
  - NitpickLawyer 4mo ago
    That's not I'm saying tho. I quoted the "non-participation in war" bit. I don't see how any system can ascertain if a prompt asking for an algorithm is dual use or not.
    - jMyles 4mo ago
      Well, taking the example in the article about a formal verification to determine whether a regex is for a collection of phone numbers or countries, and if a country is specified as "America", to formally verify whether that means North America or all Americas including the Caribbean: A regex which "properly" determines this in a witness/formal verification model is subject to the same sorts of political distinctions and nuances, right down to subjective interpretation of which nation-states are legitimate, etc, that participation in warfare/predation/injustice are. If the USA says that Cuba is part of the USA, and the rest of the Western Hemisphere says it's not, then the formal verification is necessarily matching the prompt intention to a social and political milieu, which, while subjective, is still cognizable and subject to introspection and, in some cases, a type of consensus. It seems similarly possible to formally verify that results do or do not meet similar subjective-but-cognizable criteria: does the result trigger engagement of weapons systems? Does it they implicate borders in a way that diminishes the sovereignty of a people? (which, like the regex example, have subjective but cognizable nuances)? Does the result serve to enrich (a perhaps pre-supplied) list of criminals/cartels/contractors/war profiteers? All of these seem like similar problems to the regex example. I don't disagree with your high-level contention that powerful dual-use technology can always cut through the good and evil in each of us. But I think that's precisely the point of searching for formally-verifiable spec-elucidation. If it were obvious from the outset whether or not a particular word represents the same of a nation-state widely regarded as sovereign, or whether an action was or was not an act of war, then we'd not need AI (let alone formal verification of a prompt-result match) in the first place.

otekengineering 4mo ago

this is the type of thing you need to build a foundation sturdy enough to let you operate higher up the stack and ratchet to design-by-metaphor and then design-by-philosophy. those design skills are taught in humanities departments, not engineering departments, so this is a weird feeling place for those of us that wandered over from a technical field.

remywang 4mo ago

> Telling people “you must read all the code generated by an LLM” is definitely meaningful—but it is not at all moderate (so most people won’t do it) But they should! The code is the best source of truth on what the software is doing after all. Instead of giving up on that, we should make it easier to read generated code, e.g. by generating less code in a higher level language. On the flip side, forcing myself to read all the code also resulted in a smaller, higher quality code base.

ekidd 4mo ago

> Telling people “you must read all the code generated by an LLM” is definitely meaningful—but it is not at all moderate (so most people won’t do it). I am honestly heartbroken to live in a world where reading the code is seen as an unreasonable ask by either students or by professional working programmers.

sieabahlpark 4mo ago
[dead]
ramses0 4mo ago
Don't tell me you're reading all assembly generated by your local golang or javac compiler? And that you've read every line of code down the dependency tree for your node_modules? I'm just upset that we are throwing away the original prompts for generated code in such a cavalier fashion.
- wild_egg 4mo ago
  `npm install` is the OG vibecoding
- ekidd 4mo ago
  The difference is that a compiler is a rigorous, (nearly) determinisic, heavily tested artrifact built by expert humans. I have only encountered genuine code generation bugs in compilers twice in my career. And yes, those bugs I did trace to the assembly. An LLM prompt, even a huge one, is an incredibly vague document that leaves out most of the edge cases. And even Fable 5 happily ignores clear instructions in its prompt. Now, to be fair, I absolutely expect the buggy slop to win, and to drive out the people that either write their own code or at least read the output. This will, in turn, make customers less willing to spend money on software after they get burnt a few times by buggy garbage. I think this is pretty much inevitable once Fable returns. It's just too damn good at long time horizon tasks, generating far more mostly sorta working code than any human could reasonably read.
  - warkdarrior 4mo ago