β-redex

Karma: 240

β-redex Apr 17, 2025, 5:31 PM
5 points
0
in reply to: niplav’s comment on: niplav’s Shortform
I would definitely be interested if you found a way to self-review recordings of your social interactions for improvement. The main roadblock I see is that either you tell the other parties that you are recording, which will probably influence their behavior a lot and erase most of the signal you were looking for in the first place, or you don’t, which does feel a bit unethical.

β-redex Mar 31, 2025, 9:50 PM
1 point
0
in reply to: Yair Halberstadt’s comment on: Jan Betley’s Shortform
What does “obscure” mean here? (If you label the above “obscure”, I feel like every query I consider “non-trivial” could be labeled obscure.)

I don’t think Lean is obscure, it’s one of the most popular proof assistants nowadays. The whole Lean codebase should be in the AIs training corpus (in fact that’s why I deliberately made sure to specify an older version, since I happen to know that the olean header changed recently.) If you have access to the codebase, and you understand the object representation, the solution is not too hard.

Here is the solution I wrote just now:^[1]
```
import sys, struct
assert sys.maxsize > 2**32
f = sys.stdin.buffer.read()
def u(s, o, l): return struct.unpack(s, f[o:o+l])
b = u("Q", 48, 8)[0]
def c(p, i): return u("Q", p-b+8*(i+1), 8)[0]
def n(p):
    if p == 1: return []
    assert u("iHBB", p-b, 8)[3] == 1 # 2 is num, not implemented
    s = c(p, 1) - b
    return n(c(p, 0)) + [f[s+32:s+32+u("Q", s + 8, 8)[0]-1].decode('utf-8')]
a = c(u("Q", 56, 8)[0], 1) - b
for i in range(u("Q", a+8, 8)[0]):
    print('.'.join(n(u("Q", a+24+8*i, 8)[0])))
```
(It’s minified to both fit in the comment better and to make it less useful as future AI training data, hopefully causing this question to stay useful for testing AI skills.)
1. ↩︎
  I wrote this after I wrote the previous comment, my expectation that this should be a not-too-hard problem was not informed by me actually attempting it, only by rough knowledge of how Lean represents objects and that they are serialized pretty much as-is.

β-redex Mar 31, 2025, 9:41 PM
1 point
0
in reply to: Yair Halberstadt’s comment on: Tormenting Gemini 2.5 with the [[[]]][][[]] Puzzle
Yep, that “standard library” part sure seems problematic, I am not sure if an algorithm for listing primes is shorter than just the above lookup table.

β-redex Mar 31, 2025, 7:05 PM
1 point
0
in reply to: β-redex’s comment on: Jan Betley’s Shortform
Just to give an example, here is the kind of prompt I am thinking of. I am being very specific about what I want, I think there is very little room for misunderstanding about how I expect the program to behave:

Write a Python program that reads a .olean file (Lean v4.13.0), and outputs the names of the constants defined in the file. The program has to be standalone and only use modules from the python standard library, you cannot assume Lean to be available in the environment.

o3-mini gives pure garbage hallucination for me on this one, like it’s not even close.

β-redex Mar 31, 2025, 6:34 PM
1 point
0
in reply to: Jan Betley’s comment on: Jan Betley’s Shortform

If your answer to question A is “a specific thing,” and your answer to B is “yes, I’m very clear on what I want,” then just explain it thoroughly, and you’re likely to get satisfying results. Impressive examples like “rewrite this large complex thing that particular way” fall into this category.

Disagree. It sounds like by “being specific” you mean that you explain how you want the task to be done to the AI, which in my opinion can only be mildly useful.

When I am specific to an AI about what I want, I usually still get buggy results unless the solution is easy. (And asking the AI to debug is only sometimes successful, so if I want to fix it I have to put in a lot of work to understand the code the AI wrote carefully to debug it.)

β-redex Mar 30, 2025, 5:13 AM
3 points
0
in reply to: β-redex’s comment on: Tormenting Gemini 2.5 with the [[[]]][][[]] Puzzle
I guess the reasoning for why the solution given in the post is more “valid” than this one is “something something Occam’s razor” or that it is “more elegant” (whatever “elegant” means), but if someone can make a more precise argument I would be interested to hear. (In particular, in my mind Occam’s razor is something to do with empiricism, while what we are doing here is pure logic, so not sure how it exactly applies?)

β-redex Mar 30, 2025, 5:06 AM
2 points
0
in reply to: Zygi Straznickas’s comment on: Tormenting Gemini 2.5 with the [[[]]][][[]] Puzzle
Unfortunately no, I don’t think any contradictions can be derived from the examples given in the post if we assume -E and [E] unary, and E E binary operators. Here are some example assignments for these operators that satisfy (AFAICT) the examples from the post (assuming left associativity for juxtaposition, and that the precedence of - is lower, so that -E E is interpreted as -(E E) in the last example):

Definitions for [E]:
```
1 => 2
2 => 4
-1 => 1/2
-2 => 1/4
1/2 => sqrt(2)
1001 => 1001
1004 => 1004
```
Definitions for E E:
```
1 2 => 1001
1001 1 => 3
1001 1/2 => 1001
1001 4 => 25/24
1 1 => 1002
1002 1 => 1002
1002 2 => 19
4 2 => 12
4 1 => 1003
1003 2 => 20
1 1/2 => 1004
sqrt(2) 1004 => 72^1/6
1/4 1 => 1005
1005 2 => 5/4
12 1 => 1006
1006 2 => 84
```
Definitions for -E:
```
-(1) => -1
-(2) => -2
-(1001) => 1001
```

β-redex Mar 29, 2025, 8:03 PM
7 points
2
on: Tormenting Gemini 2.5 with the [[[]]][][[]] Puzzle
I fairly quickly figured out that the grammar is something like E ::= "[]" | "[" E "]" | "-" E | "E E", and that eval([E]) = 2^eval(E) (and eval(-E) = -eval(E)), and then went down the rabbit hole of trying to come up with some f eval(E1 E2) = f(eval(E1), eval(E2)) for juxtaposition, and thinking about whether it’s left or right associative. I was also thinking that maybe it’s n-ary rather than binary so that associativity does not matter.

Anyway, I think where I went wrong is that I decided that [E] is a unary operator by itself, and did not reconsider this. So the lesson is… don’t just assume the simplest possible AST structure implied by the grammar?

β-redex Mar 26, 2025, 5:52 PM
1 point
0
in reply to: Daniel Tan’s comment on: Daniel Tan’s Shortform
Pull requests. Useful to group a bunch of messy commits into a single high-level purpose and commit that to main. Makes your commit history easier to read.

You can also squash multiple commits without using PRs. In fact, if someone meticulously edited their commit history for a PR to be easy-to-follow and the changes in each commit are grouped based on them being some higher level logical single unit of change, squashing their commits can be actively bad, since now you are destroying the structure and making the history less readable by making a single messy commit.

With most SWEs when I try to get them to create nicer commit histories, I get pushback. Sure, not knowing the tools (git add -p and git rebase -i mostly tbh.) can be a barrier, but showing them nice commit histories does not motivate them to learn the tools used to create them. They don’t seem to see the value in a nice commit history.^[1]

Which makes me wonder: why do you advocate for putting any effort into the git history for research projects (saying that “It’s more important here to apply ‘Good SWE practices’”), when even 99% of SWEs don’t follow good practices here? (Is looking back at the history maybe more important for research than for SWE, as you describe research code being more journal-like?)
1. ↩︎
  Which could maybe be because they also don’t know the tools that can extract value from a nice commit history? E.g. using git blame or git bisect is a much more pleasant experience with a nice history.

β-redex Mar 14, 2025, 11:49 PM
6 points
2
in reply to: johnswentworth’s comment on: johnswentworth’s Shortform
Does Overleaf have such AI integration that can get “accidentally” activated, or are you using some other AI plugin?

Either way, this sounds concerning to me, we are so bad at AI boxing that it doesn’t even have to break out, we just “accidentally” hand it edit access to random documents. (And especially an AI safety research paper is not something I would want a misaligned AI editing without close oversight.)

β-redex Mar 14, 2025, 9:54 PM
5 points
0
in reply to: johnswentworth’s comment on: johnswentworth’s Shortform
Could someone explain the joke to me? If I take the above statement literally, some change made it into your document, which nobody with access claims to have put there. You must have some sort of revision control, so you should at least know exactly who and when made that edit, which should already narrow it down a lot?

β-redex Mar 9, 2025, 6:49 PM
2 points
0
in reply to: ErickBall’s comment on: So how well is Claude playing Pokémon?
I am not a 100% convinced by the comparison, because technically LLMs are only “reading” a bunch of source code, they are never given access to a compiler/interpreter. IMO actually running the code one has written is a very important part of learning, and I think it would be a much more difficult task for a human to learn to code just by reading a bunch of books/code, but never actually trying to write & run their own code.^[1]

Also, in the video linked earlier in the thread, the girlfriend playing Terraria is deliberately not given access to the wiki, and thus I believe is an unfair comparison. I expect to see much better human performance if you give them access to manuals & wikis about the game.

Another interesting question is to what extent you can train an AI system on a variety of videogames and then have it take on a new one with no game-specific training. I don’t know if anyone has tried that with LLMs yet.

Not sure either, but I agree that this would be an interesting experiment. (Human gamers are often much quicker at picking up new games and are much better at them than someone with no gaming background.)
1. ↩︎
  I would expect the average human to stay very bad at coding, no matter how many books & code examples you give them. I would also expect some smaller class of humans to nevertheless be able to pull that feat off. (E.g. maybe a mathematician well versed in formal logic, who is used to doing complex symbolic manipulation correctly “only on paper”, could probably write non-trivial correct programs just by reading about the subject. In fact, a lot of stuff from computer science was worked out well before computers were built, e.g. Ada Lovelace is usually credited with writing the “first computer program”, well before the first digital computer existed.)

β-redex Mar 8, 2025, 9:46 AM
7 points
3
in reply to: MondSemmel’s comment on: So how well is Claude playing Pokémon?

And as a separate note, I’m not sure what the appropriate human reference class for game-playing AIs is, but I challenge the assumption that it should be people who are familiar with games. Rather than, say, people picked at random from anywhere on earth.

If you did that for programming, AIs would already be considered strongly superhuman. Just like we compare AI’s coding knowledge to programmers, I think it’s perfectly fair to compare their gaming abilities to people who play video games.

β-redex Mar 6, 2025, 11:17 PM
1 point
0
in reply to: Noosphere89’s comment on: Can a finite physical device be Turing equivalent?

Notably, this was exactly the sort of belief I was trying to show is false

Please point out if there is a specific claim I made in my comment that you believe to be false. I said that “I don’t think a TC computer can ever be built in our universe.”, which you don’t seem to argue with? (If we assume that we can only ever get access to a finite number of atoms. If you dispute this I won’t argue with that, neither of us has a Theory of Everything to say for certain.)

Just to make precise why I was making that claim and what it was trying to argue against, take this quote from the post:

yes, you can consider a finite computer in the real world to be Turing-complete

I dropped the “finite computer” constraint and interpreted the phrase “real world” to mean that “it can be built in our universe”, this is how I arrived at the “a TC computer can be built in our universe” statement, which I claimed was false.

β-redex Mar 6, 2025, 9:41 PM
2 points
0
on: Can a finite physical device be Turing equivalent?
I don’t think a TC computer can ever be built in our universe. The observable universe has a finite number of atoms, I have seen numbers around $10^{80}$ thrown around. Even if you can build a RAM where each atom stores 1 bit,^[1] this is still very much finite.

I think a much more interesting question is why TC machines are — despite only existing in theory — such useful models for thinking about real-world computers. There is obviously some approximation going on here, where for the vast majority of real-world problems, you can write them in such a way that they work just fine with finite RAM. (E.g. the cases where we would run out of RAM are quite easy to predict, and don’t just crop up randomly.)
1. ↩︎
  You can maybe push that number up by e.g. using subatomic particles or using a number of different quantum states of a single particle, but I think with all the tricks you will still end up with some well bounded constant multiplier for how many bits you can store, which does not matter much for this argument.

β-redex Mar 6, 2025, 9:22 PM
1 point
0
on: Can a finite physical device be Turing equivalent?
Let $S = {0, 1}^{n}$ be the state space of our finite/physical computer, where $n$ is the number of bits of state the computer has. This can include RAM, non-volatile storage, CPU registers, cache, GPU RAM, etc… just add up all the bits.

The stateless parts of the computer can be modeled as a state transition function $f : S \to S$ , which is applied at every time step to produce the next state. (And let’s suppose that there is some special halting state $h \in S$ .)

This is clearly a FSM with $2^{n}$ states, and not TC. The halting problem can be trivially solved for it: it is guaranteed to either halt or loop after $2^{n}$ steps.

(Proof: It can be seen that if we ever get back to a state where we have already been, we will loop. So let’s suppose that after $2^{n}$ time we have had a different state at each time step, and haven’t halted. This is impossible, since there are only $| S | - 1 = 2^{n} - 1$ non-halting states, so there cannot exist $2^{n}$ distinct ones.)

β-redex Dec 6, 2023, 3:45 AM
7 points
18
in reply to: niplav’s comment on: How do you feel about LessWrong these days? [Open feedback thread]
I think the reacts being semantic instead of being random emojis is what makes this so much better.

I wish other platforms experimented with semantic reacts as well, instead of just letting people react with any emoji of their choosing, and making you guess whether e.g. “thumbs up” means agreement, acknowledgement, or endorsement, etc.

β-redex Dec 2, 2023, 7:33 PM
25 points
0
on: 2023 Unofficial LessWrong Census/Survey
This was my first time taking this, looking forward to the results!

β-redex Oct 23, 2023, 1:38 PM
30 points
5
on: Which LessWrongers are (aspiring) YouTubers?
I know of Robert Miles, and Writer, who does Rational Animations. (In fact Robert Miles’ channel is the primary reason I discovered LessWrong :) )

β-redex Oct 15, 2023, 8:54 AM
1 point
0
in reply to: Raemon’s comment on: Rationalist horror movies
Don’t leave me hanging like this, does the movie you are describing exist? (Though I guess your description is a major spoiler, you would need to go in without knowing whether there will be anything supernatural.)