evhub

• evhub 15 Sep 2018 23:09 UTC

  1 point

  on: Owen’s short-form blog

  Is there an RSS feed?

• evhub 11 Jul 2018 19:43 UTC

  4 points

  in reply to: rk’s comment on: Dependent Type Theory and Zero-Shot Reasoning

  Dimensional analysis is absolutely an instance of what I’m talking about!

  As for only being able to do constructive stuff, you actually can do classical stuff as well, but you have to explicitly assume the law of the excluded middle. For example, if in Lean I write

  axiom lem (P: Prop): P ∨ ¬P

  then I can start doing classical reasoning.

  Also, you’re totally right that you could also do $h\left(h\right(fxx\left)\right)$ and so on as much as you want, but there’s no real reason to do so, since if you start from the simplest possible way to do it you’ll solve the problem by the time you get to $h\left(fxx\right)$.

• evhub 11 Jul 2018 3:34 UTC

  2 points

  on: Conditions under which misaligned subagents can (not) arise in classifiers

  There are a couple of pieces of this that I disagree with:

  • I think claim 1 is wrong because even if the memory is unhelpful, the agent which uses it might be simpler, and so you might still end up with an agent. My intuition is that just specifying a utility function and an optimization process is often much easier than specifying the complete details of the actual solution, and thus any sort of program-search-based optimization process (e.g. gradient descent in a nn) has a good chance of finding an agent.

  • I think claim 3 is wrong because agenty solutions exist for all tasks, even classification tasks. For example, take the function which spins up an agent, tasks that agent with the classification task, and then takes that agent’s output. Unless you’ve done something to explicitly remove agents from your search space, this sort of solution always exists.

  • Thus, I think claim 6 is wrong due to my complaints about claims 1 and 3.

Dependent Type Theory and Zero-Shot Reasoning