Azimov

• Azimov 6 Aug 2026 19:16 UTC

  2 points

  0

  in reply to: Azimov’s comment on: Re­turn­ing to ARC

  For example, suppose a mechanism reliably detects something labelled “diamond”. We still need to know whether it tracks: - actual diamonds, - images or descriptions of diamonds, - the training data’s annotation conventions, - some accidental correlate, etc.

  I’m quite eager to see ARC’s theory of how internal computational strucctures become grounded in external properties we mean to ask about.

• Azimov 6 Aug 2026 18:42 UTC

  0 points

  0

  in reply to: paulfchristiano’s comment on: Re­turn­ing to ARC

  Thanks for your answer!

  The main philosophically tangled part is pointing to latent structure for which no good definition is available, for which we want to say something like “The presence of a diamond is the property that causes such-and-such observable regularities.”

  The distinction makes me think the missing object may be a validation layer rather than another kind of mechanistic explanation.
  

  I’ve been approaching a connected problem through the distinction between verification (is the thing right?) and validation (is it the right thing?). A mechanistic analysis can verify that a model satisfies a defined query but not yet sure if it can verify if/​how that query maintains the external property we intended to ask about.

  
  I thought of exploring possible latent properties through their invariance/​covariance across multiple observational interfaces (and interventions). A candidate reporter/​explanation would then “commute” across semantically equivalent representations, respond to property-changing interventions (and abstain where the available constraints do not identify a unique reference?).

  
  I’ve been testing a very small version of this using Lean-verified equational implications translated into different formal and natural-language representations. A probe can recover the label strongly within an interface, but it collapses almost to chance-level across semantically similar templates. After reading some of your ELK writings (+ others’ disambiguations), I started seeing this more like a mapper tied to one observational interface than a translator of a shared latent structure.

  
  Do you imagine something like an equivalence class identified by causal/​cross-representational constraints to be within scope for your work? I’m working my way towards semantic diffchecking accross representations (within diagonalization limits ofc) and this whole line of work looks fascinating.

• Azimov 5 Aug 2026 21:42 UTC

  3 points

  0

  on: Re­turn­ing to ARC

  Happy to hear you’re back with ARC! I’m a huge fan of the thought space.

  Assuming a bounded, well specified alignment property, what ensures that the object connecting a hypothesis to a mechanistic explanation to a loss function preserves the intended meaning?

  Also, why would training-gaming not move up one level then? from gaming behavioral evaluations to gaming the explanatory ontology or the mechanistic explanator?

• Azimov 4 Aug 2026 18:10 UTC

  1 point

  0

  on: A sys­tem overview for near-term, low-trust AI com­pute verification

  Cunningham’s law: I make assertions about what the (emerging) field of AI verification should aim for, and people with experience in international policy, cybersecurity and any relevant field of engineering can point out what this draft gets wrong.

  I used to like this law pre-LLMs, but it presumes verification is cheap relative to generation and lately that doesn’t fully stand.

  A frame I kept applying while reading is on a separation between security and safety. I had it described as:
  - security asks how we stop the world from breaking into a system;
  - safety asks how we stop a system from breaking into the world.
  
  The threat model contains two agents, which are both human coalitions. with no description for the compliant-prover /​ adversarial-model case. A model scheming through sanctioned channels can produce traffic that hashes clean and has syntactic checks passing because the syntax is faithful to the computation. The Aumann–Lindell inversion doesn’t transfer there, as deterrence assumes an adversary that values futures in which it got caught, whilist a misaligned model may not be playing an iterated game. Is the adversarial-model case in scope here, or left to another layer by design?

  Also, the bilateral setting seems to hand the prover the sampling protocol, the batching scheme, the fault budget, and control of the workload-to-hash-space mapping; can’t fully see it right now, but that feels gameable.
  
  

• Azimov 31 Jul 2026 18:07 UTC

  1 point

  0

  on: The Scal­able For­mal Over­sight Re­search Program

  Thanks for gathering these thoughts here! I recently stumbled on them and got pulled into the post.
  
  Small objection I’d like to make: You write that spec tooling most likely needs to be solved before any of the other problems become solvable, but I think it’s worse than that, because better tooling conserves the problem and relocates it.
  
  Formalization splits one hard question (is this true of the world) into two:

  • Does it follow from the spec? (mechanically checkable)

  • Does the spec capture the world? (not checkable from inside, like ever?)

  This seems to want for a shift into what a research program aimed at specifications should target: an exploration of validation (is it the right thing?) rather than verification (does it do the thing right?).
  
  Also, knowing when a check tests for the property it claims to be about instead of passing for some other reason connects to vacuities in formal verification.