# Darmani

Karma: 1,017
• Really appreciate this informative and well-written answer. Nice to hear from someone on the ground about SELinux instead of the NSA’s own presentations.

• I phrased my question about time and space badly. I was interested in proving the time and space behavior of the software “under scrutiny”, not in the resource consumption of the verification systems themsvelves.

LOL!

I know a few people who have worked in this area. Jan Hoffman and Peng Gong have worked on automatically inferring complexity. Tristan Knoth has gone the other way, including resource bounds in specs for program synthesis. There’s a guy who did an MIT Ph. D. on building an operating system in Go, and as part of it needed an analyzer that can upper-bound the memory consumption of a system call. I met someone at CU Boulder working under Bor-Yuh Evan Chang who was also doing static analysis of memory usage, but I forget whom.

So, those are some things that were going on. About all of these are 5+ years old, and I have no more recent updates. I’ve gone to one of Peng’s talks and read none of these papers.

• I must disagree with the first claim. Defense-in-depth is very much a thing in cybersecurity. The whole “attack surface” idea assumes that, if you compromise any application, you can take over an entire machine or network of machines. That is still sometimes true, but continually less so. Think it’s game over if you get root on a machine? Not if it’s running SELinux.

Hey, can I ask an almost unrelated question that you’re free to ignore or answer as a private message OR answer here? How good is formal verification for time and space these days?

I can speak only in broad strokes here, as I have not published in verification. My publications are predominantly in programming tools of some form, mostly in program transformation and synthesis.

There are two main subfields that fight over the term “verification”: model checking and mechanized/​interactive theorem proving. This is not counting people like Dawson Engler, who write very unsound static analysis tools but call it “verification” anyway. I give an ultra-brief overview of verification in https://​​www.pathsensitive.com/​​2021/​​03/​​why-programmers-shouldnt-learn-theory.html

I am more knowledgable about mechanized theorem proving, since my department has multiple labs who work in this area and I’ve taken a few of their seminars. But asking about time/​space of verification really just makes sense for the automated part. I attended CAV in 2015 and went to a few model checking talks at ICSE 2016, and more recently talked to a friend on AWS’s verification team about what some people there are doing with CBMC. Okay, and I guess I talked to someone who used to do model checking on train systems in France just two days ago. Outside of that exposure, I am super not-up-to-date with what’s going on. But I’d still expect massive breakthroughs to make the news rounds over to my corner of academia, so I’ll give my sense of the status quo.

Explicit state enumeration can crush programs with millions or billions of states, while symbolic model checking routinely handles $10^100$ states.

Those are both very small numbers. To go bigger, you need induction or abstraction, something fully automated methods are still bad at.

Yes, we can handle exponentially large things, but the exponential still wins. There’s a saying of SAT solvers “either it runs instantly or it takes forever.” I believe this is less true of model checking, though still true. (Also, many model checkers use SAT.)

If you want to model check something, either you check a very small program like a device driver, or you develop some kind of abstract model and check that instead.

• I agree with about everything you said as well as several more criticisms along those lines you didn’t say. I am probably more familiar with these issues than anyone else on this website with the possible exception of Jason Gross.

Now, suppose we can magic all that away. How much then will this reduce AI risk?

# [Question] How much does cy­ber­se­cu­rity re­duce AI risk?

12 Jun 2022 22:13 UTC
33 points
• I don’t see what this parable has to do with Bayesianism or Frequentism.

I thought this was going to be some kind of trap or joke around how “probability of belief in Bayesianism” is a nonsense question in Frequentism.

• I do not. I mostly know of this field from conversations with people in my lab who work in this area, including Osbert Bastani. (I’m more on the pure programming-languages side, not an AI guy.) Those conversations kinda died during COVID when no-one was going into the office, plus the people working in this area moved onto their faculty positions.

I think being able to backtrace through a tree counts as victory, at least in comparison to neural nets. You can make a similar criticism about any large software system.

You’re right about the random forest there; I goofed there. Luckily, I also happen to know of another Osbert paper, and this one does indeed do a similar trick for neural nets (specifically for reinforcement learning); https://​​proceedings.neurips.cc/​​paper/​​2018/​​file/​​e6d8545daa42d5ced125a4bf747b3688-Paper.pdf

# Cam­bridge LW Meetup: Books That Change

8 May 2022 5:23 UTC
5 points

# Cam­bridge LW Meetup: Bean on Why You Should Stop Wor­ry­ing and Love the Bomb

5 Apr 2022 18:34 UTC
9 points

# Nu­clear Deter­rence 101 (and why the US can’t even hint at in­ter­ven­ing in Ukraine)

18 Mar 2022 7:25 UTC
34 points
• I’m a certified life coach, and several of these are questions found in life coaching.

E.g.:

Is there something you could do about that problem in the next five minutes?

Feeling stuck sucks. Have you spent a five minute timer generating options?

What’s the twenty minute /​ minimum viable product version of this overwhelming-feeling thing?

These are all part of a broader technique of breaking down a problem. (I can probably find a name for it in my book.) E.g.: Someone comes in saying they’re really bad at X, and you ask them to actually rate their skills and then what they could do to become 5% better.

You want to do that but don’t think you will? Do you want to make a concrete plan now?

Do you want to just set an alarm on your phone now as a reminder? (from Damon Sasi)

These are all part of the “commitment” phase of a coaching session, which basically looks like walking someone through SMART goals.

Do you know anyone else who might have struggled with or succeeded at that? Have you talked to them about it? (from Damon Sasi)

Who do you know who you could ask for help from?

I can’t say these are instances of a named technique, but they are things you’d commonly find a coach asking. Helping someone look inside themselves for resources they already have is a pretty significant component of coaching.

There’s a major technique in coaching not represented here called championing. Champion is giving someone positive encouragement by reinforcing some underlying quality. E.g.: “You’ve shown a lot of determination to get this far, and I know you’ll be able to use it to succeed at X.”

• I realize now that this expressed as a DAG looks identical to precommitment.

Except, I also think it’s a faithful representation of the typical Newcomb scenario.

Paradox only arises if you can say “I am a two-boxer” (by picking up two boxes) while you were predicted to be a one-boxer. This can only happen if there are multiple nodes for two-boxing set to different values.

But really, this is a problem of the kind solved by superspecs in my Onward! paper. There is a constraint that the prediction of two-boxing must be the same as the actual two-boxing. Traditional causal DAGs can only express this by making them literally the same node; super-specs allow more flexibility. I am unclear how exactly it’s handled in FDT, but it has a similar analysis of the problem (“CDT breaks correlations”).

• Okay, I see how that technique of breaking circularity in the model looks like precommitment.

I still don’t see what this has to do with counterfactuals though.

• I don’t understand what counterfactuals have to do with Newcomb’s problem. You decide either “I am a one-boxer” or “I am a two-boxer,” the boxes get filled according to a rule, and then you pick deterministically according to a rule. It’s all forward reasoning; it’s just a bit weird because the action in question happens way before you are faced with the boxes. I don’t see any updating on a factual world to infer outcomes in a counterfactual world.

”Prediction” in this context is a synonym for conditioning. is defined as .

If intervention sounds circular...I don’t know what to say other than read Chapter 1 of Pearl ( https://​​www.amazon.com/​​Causality-Reasoning-Inference-Judea-Pearl/​​dp/​​052189560X ).

To give a two-sentence technical explanation:

A structural causal model is a straight-line program with some random inputs. They look like this

u1 = randBool()

rain = u1

sprinkler = !rain

wet_grass = rain || sprinkler

It’s usually written with nodes and graphs, but they are equivalent to straight-line programs, and one can translate easily between these two presentations.

In the basic Pearl setup, an intervention consists of replacing one of the assignments above with an assignment to a constant. Here is an intervention setting the sprinkler off.

u1 = randBool()

rain = u1

sprinkler = false

wet_grass = rain || sprinkler

From this, one can easily compute that.

If you want the technical development of counterfactuals that my post is based on, read Pearl Chapter 7, or Google around for the “twin network construction.”

Or I’ll just show you in code below how you compute the counterfactual “I see the sprinkler is on, so, if it hadn’t come on, the grass would not be wet,” which is written

We construct a new program,

u1 = randBool()

rain = u1

sprinkler_factual = !rain

wet_grass_factual = rain || sprinkler_factual

sprinkler_counterfactual = false

wet_grass_counterfactual = rain || sprinkler_counterfactual

This is now reduced to a pure statistical problem. Run this program a bunch of times, filter down to only the runs where sprinkler_factual is true, and you’ll find that wet_grass_counterfactual is false in all of them.

If you write this program as a dataflow graph, you see everything that happens after the intervention point being duplicated, but the background variables (the rain) are shared between them. This graph is the twin network, and this technique is called the “twin network construction.” It can also be thought of as what the do(y | x → e) operator is doing in our Omega language.

• While I can see this working in theory, in practise it’s more complicated as it isn’t obvious from immediate inspection to what extent an argument is or isn’t dependent on counterfactuals. I mean counterfactuals are everywhere! Part of the problem is that the clearest explanation of such a scheme would likely make use of counterfactuals, even if it were later shown that these aren’t necessary.

1. Is the explanation in the “What is a Counterfactual” post linked above circular?

2. Is the explanation in the post somehow not an explanation of counterfactuals?

The key unanswered question (well, some people claim to have solutions) in Functional Decision theory is how to construct the logical counterfactuals that it depends on.

I read a large chunk of the FDT paper while drafting my last comment.

The quoted sentence may hint at the root of the trouble that I and some others here seem to have in understanding what you want. You seem to be asking about the way “counterfactual” is used in a particular paper, not in general.

It is glossed over and not explained in full detail in the FDT paper, but it seems to mainly rely on extra constraints on allowable interventions, similar to the “super-specs” in one of my other papers: https://​​www.jameskoppel.com/​​files/​​papers/​​demystifying_dependence.pdf .

I’m going to go try to model Newcomb’s problem and some of the other FDT examples in Omega. If I’m successive, it’s evidence that there’s nothing more interesting going on than what’s in my causal hierarchy post.

• I’m having a little trouble understanding the question. I think you may be thinking of either philosophical abduction/​induction or logical abduction/​induction.

Abduction in this article is just computing P(y | x) when x is a causal descendant of y. It’s not conceptually different from any other kind of conditioning.

In a different context, I can say that I’m fond of Isil Dillig’s thesis work on an abductive SAT solver and its application to program verification, but that’s very unrelated.

• I’m not surprised by this reaction, seeing as I jumped on banging it out rather than checking to make sure that I understand your confusion first. And I still don’t understand your confusion, so my best hope was giving a very clear, computational explanation of counterfactuals with no circularity in hopes it helps.

Anyway, let’s have some back and forth right here. I’m having trouble teasing apart the different threads of thought that I’m reading.

After intervening on our decision node do we just project forward as per Causal Decision Theory or do we want to do something like Functional Decision Theory that allows back-projecting as well?

I think I’ll need to see some formulae to be sure I know what you’re talking about. I understand the core of decision theory to be about how to score potential actions, which seems like a pretty separate question from understanding counterfactuals.

More specifically, I understand that each decision theory provides two components: (1) a type of probabilistic model for modeling relevant scenarios, and (2) a probabilistic query that it says should be used to evaluate potential actions. Evidentiary decision theory uses an arbitrary probability distribution as its model, and evaluates actions by P(outcome |action). Causal decision theory uses a causal Bayes net (set of intervential distributions) and the query P(outcome | do(action)). I understand FDT less well, but basically view it as similar to CDT, except that it intervenes on the input to a decision procedure rather than on the output.

But all this is separate from the question of how to compute counterfactuals, and I don’t understand why you bring this up.

When trying to answer these questions, this naturally leads us to ask, “What exactly are these counterfactual things anyway?” and that path (in my opinion) leads to circularity.

I still understand this to be the core of your question. Can you explain what questions remain about “what is a counterfactual” after reading my post?