Comment by perching_aix

13 hours ago

I've been thinking about autoformalizing local laws using agents into TLA+ or something, but it's sufficiently past enough my actual skillset that I'm pretty sure I'd just end up wrestling with slop like a pig in the mud. It's a shame though, I consider law to be just kind of a shitty codebase, with natural language being tortured into cooperating, so it's a really natural fit.

I'll probably yield to my temptations eventually and proceed anyways. Lord help me from all the creative but completely detached interpretations I'll land on.

I did this for a few federal agencies, here a few examples

https://ice.dhs.dev/program/13732-human-trafficking-investig...

https://atf.doj.dev/program/44825-open-gun-store-need-ffl

LMK if you want to know more.

  • I do, though I'm not entirely sure what am I looking at on those links. Could you start by explaining that? They look like training courses or something.

    I saw a sequence diagram browsing around, seemed to be specific to a sample scenario?

    • Each time I try and explain, it flags comment and says its ai slop.

      Each "program" here is a government program, agents orchestrate everything including the collaboration between all parties required.

      High points: I have been able to help over 100 people get housing with no HITL on my side.

      Note: Each host/subdomain is a project, they all inherit policy from each other and that drives the program generation and orchestration layer. Policies can be managed for the diff agencies at rnc/dnc.dev

    • tl;dr a "program" here is a government program (get an FFL, file a discrimination charge, apply for a benefit), codified so that every step has an actor, typed inputs and outputs, and a citation to the provision that authorizes it. Agents then walk each party through it. And note it points the opposite way from ChatGPT-drafts-your-tribunal-claim in TFA: that dynamic broke because AI made filing free while adjudicating stayed expensive, so the queue explodes. Codifying the procedure attacks the other side; what's actually required, where it actually goes, and whether you have it; before it becomes a hearing in 2030.

      Fair question, and the "training course" read is not an accident; it's the same shape underneath. A program is an ordered chain of modules, each with a declared actor and typed inputs/outputs. Courses are also that. So it renders with the same components. The sequence diagram you found isn't a sample scenario, it's the deal template's actual step graph; the thing an instance runs on.

      Three authored files per domain:

      - an ontology: the domain's vocabulary, its regulatory frameworks with real citations, the O*NET occupations that staff it, the systems of record it touches

      - intents: what a person actually shows up wanting ("open a gun store, need an FFL"), with typed parameters

      - deal templates, one per intent: ordered pipeline_steps, each with an actor, inputs, outputs, and a policy_check

      The page you clicked is generated from the last two deterministically. No model in that path.

      The part that speaks to your TLA+ instinct: I deliberately don't formalize what the law means. I formalize the procedure, and bind each step to the provision that authorizes it. Formalizing semantics is exactly where you get the creative, detached interpretations you're worried about, because every gap gets filled by the model's guess. Formalizing procedure asks the model to transcribe and cite, which is checkable:

      - every step input is a ref; param:x, step:3.some_output, system:NICS.event; and it has to resolve. A step: ref must name an earlier step's declared output, so the dataflow is a DAG with referential integrity.

      - every step's policy_check must name a framework declared in the ontology. A step that no provision authorizes fails validation.

      So most hallucination becomes a build error instead of a plausible sentence. That's the whole trick. Not a smarter model; a narrower artifact.

      Concretely, since you're right to expect slop: my first pass at four new agencies came back with 100% of step inputs referencing parameters that didn't exist, and prompts that literally said "Subject?". The validator refused all forty programs. That's the mechanism working; I'd have merged them on a read-through.

      Intents and flows for ATF, if you want to see the layer under the program page: https://wiki.doj.dev/agent/atf

      Limits, since you'll ask. It decides nothing; no adjudication, and consequential steps are human-gated. It's also not a formal method: the invariants are referential integrity and citation binding, not model checking. The genuinely temporal parts are the deadlines, and those do bite; the NLRB's six-month charge window runs from filing and service, with service being the filer's own duty, so a filing-date-only clock computes the wrong date on a deadline that destroys the claim if you miss it.

      Re: the sibling comment about discretion; that's the actual pitch. Discretion hides in the gap between the written rule and the practiced procedure. Writing the practiced procedure down, with a citation per step, is what makes the gap visible.

      1 reply →