03
Determinism From Ambiguity
How does fuzzy human intent become behaviour you can defend?
Getting from a sentence someone said to a rule that is repeatable, inspectable and diffable.
6 lessons · 8 checks · 56 min
Why it sits here
Third because modules 01 and 02 give you a loop and a substrate, and neither answers the question that decides whether the system is auditable: is the model in the hot path? Everything downstream — what you can replay, what you can prove, what you can change safely — follows from where you put it.
Lessons
- The one distinction that organises everythingTwo places to put the model. Not points on a spectrum — different systems with different failure modes.10m
- Why temperature zero is not determinismThe folk explanation is wrong in an interesting way, and the right one has two halves.9m
- Shape, not semanticsConstrained decoding guarantees membership in a language. It guarantees nothing about truth.7m
- The destination formatIf the model is a compiler, something has to be the target language. The criteria are not the obvious ones.10m
- The verification ladderYou cannot verify against intent. So you build a ladder of proxies and stay honest about which rung you are on.12m
- Versioning, effective dates and driftA compiled rule is a durable artifact. Most of this is unglamorous and most systems get it wrong in the same places.8m
Pre-reading
12 sources · ~9h if you read all of itRanked, not exhaustive. The lessons stand on their own, so treat the first tier as the genuinely load-bearing sources and the rest as depth when a lesson makes you want it.
Read properly
- Defeating Nondeterminism in LLM InferenceThinking Machines LabReplaces the wrong folk explanation with the right one. 80 unique completions from 1,000 identical greedy requests.45 min
- Cedar: Expressive, Fast, Safe, Analyzable AuthorizationCutler, Disselkoen, Hicks, Rungta, Torlak et al · arXiv:2403.04651The only mainstream policy language designed backwards from "we must be able to prove things about policy sets". Read the spec repo alongside it.90 min
- Faithful Autoformalization via Roundtrip Verification and RepairAmrollahi, Lopez, Barrett · arXiv:2604.25031Automated round-trip equivalence checking with stage diagnosis, evaluated on statutory text. The upgrade to rung 1 of the verification ladder.40 min
- Why Don't People Use Formal Methods?Hillel WayneThe taxonomy you need to decide how much rigour to buy, and the cost argument that stops you over-investing.30 min
- Automating String Processing in Spreadsheets using Input-Output ExamplesGulwani, POPL 2011The canonical shipped programming-by-example success, and the canonical treatment of ambiguity as a product concern rather than a modelling one.60 min
- SymCert: Verifying SMT-based policy analysesTorlak, FMCAD 2026How you get counterexamples a human can read out of an SMT model. Only if you go deep on policy analysis.90 min
Skim one section
- Interactive Program SynthesisLe, Perelman, Polozov, Raza, Udupa, Gulwani · arXiv:1703.03539The formal treatment of the loop you are building: incomplete specs, non-programmer users, ambiguity resolved by targeted feedback.40 min
- Prose2PolicyGupta, Sreenivasamurthy · Apple Machine Learning ResearchSkim to the three numbers. 95.3% compile, 98.9% negative tests, 82.2% positive. The gap is the whole argument for changeset gating.20 min
- Decision Logs and Policy TestingOpen Policy Agent docsNot for Rego. For the decision-record schema, including the bundle revision that makes a decision explainable a year later.30 min
- Efficient Guided Generation for Large Language ModelsWillard & Louf · arXiv:2307.09702How constrained decoding works, at the level where you can reason about what it can and cannot enforce.30 min
Citation grade
- Let Me Speak Freely?Tam, Wu, Tsai, Lin, Lee, Chen · arXiv:2408.02442Format restriction degrades reasoning. The counterweight to "just turn on JSON mode".20 min
- Hypothesis documentationhypothesis.readthedocs.ioShrinking, the example database, stateful testing. What makes property testing operationally worth it.20 min