β-redex

Karma: 262

β-redex May 12, 2025, 10:32 PM
9 points
0
in reply to: tcheasdfjkl’s comment on: How to title your blog post or whatever

What? I am telling you it is.

and preferentially read things that take less cognitive effort (all else equal, of course)

Sorry, no offense meant, I am just genuinely surprised. But I believe you now, I guess our experiences are just very different in this regard.

β-redex May 12, 2025, 9:40 PM
2 points
0
in reply to: tcheasdfjkl’s comment on: How to title your blog post or whatever
that sentence is semantically dense and grammatically complicated. I have to put in some work to break it down into noun phrases and such and figure out how it fits together. requiring cognitive work of potential readers before they’ve even decided if they want to read your thing is extremely anti-memetic

Sorry, but I call bullshit on this being a problem for you, or any other LW reader.

Now you are probably right that if you take the general population, for a significant number of people parsing anything but the simplest grammatical structures is going to impart noticeable extra cognitive load, lowering overall memetic fitness.

But as the post outlined, we are not optimizing for the number clicks, we are optimizing for something like P(loves article|clicked). See also https://www.lesswrong.com/posts/vidXh2DJtnqH5ysrZ/a-blog-post-is-a-very-long-and-complex-search-query-to-find

So if you are worried about someone bouncing off the title because of its grammatical complexity, you better also write the article with simple grammar (and simple content). Are there situations where your main goal is to reach as many people as possible? Sure, but for that you probably want to optimize both the title and content with that in mind. And at this point what you are doing is probably more like “political communication” than “writing something for like-minded people”.

the tone of it sounds like a dry academic paper. those are typically not very fun to read. it signals that this will also not be fun to read

For me it signals more positive things like seriousness and better epistemics^[1], but you probably have a point that there is space to signal the tone of the article in the title. Still, I don’t think reducing its information density is the right way to do it.
1. ↩︎
  Well, on blog posts at least. On actual academic papers everyone is expected to write in a serious sounding academic style, so there is much less signal there.

β-redex May 12, 2025, 7:41 PM
6 points
−1
on: How to title your blog post or whatever
I’m worried about Chicago

In what world is this a good title? It basically gives zero information about the topic of the article, it is exactly the kind of clickbait title that purposefully omits any relevant information from the title to try to make people click. I personally associate such clickbait titles with terrible content, and they make me much less likely to click.^[1]

What would be wrong with just using the subtitle as the actual title? It’s much more informative:

Slowing national population growth plus remote work spell big trouble for Midwestern cities
1. ↩︎
  Unfortunately various platforms actively push authors towards clickbait titles, and even if the author dislikes them they often don’t have a choice. Often good content is actually hiding behind terrible clickbait titles (and thumbnails) nowadays, so I sometimes have to make an active effort to click on clickbait because otherwise I could be missing out on discovering some good content.

β-redex May 8, 2025, 10:05 PM
6 points
0
on: Orienting Toward Wizard Power
Interesting. While the post resonates with me, I feel like I am trying to go in the opposite direction right now, trying to avoid getting nerd sniped by all the various fields I could be getting into, and instead strategically choosing the skills so that they are the most useful for solving the bottlenecks for my other goals that are not “learning cool technical things”.

Which is interesting, because so far based on your posts you struck me as the kind of person I am trying to be more like in this regard, being more strategic about my goals. So maybe the pendulum swings back, and eventually you find out that letting yourself get nerd sniped by random things does have some hidden benefits? I guess I will find out in a few years (if we are alive).

β-redex Apr 26, 2025, 2:39 PM
12 points
1
in reply to: faul_sname’s comment on: faul_sname’s Shortform
Wonder if correctness proofs (checked by some proof assistant) can help with this.^[1]

I think the main bottleneck in the past for correctness proofs was that it takes much more effort to write the proofs than it takes to write the programs themselves, and current automated theorem provers are nowhere near good enough.

Writing machine checked proofs is a prime RL target, since proof assistant kernels should be adversarially robust. We have already seen great results from stuff like AlphaProof.
1. ↩︎
  One counterargument I could see is that writing the correctness properties themselves could turn out to be a major bottleneck. It might be that for most real world systems you can’t write succinct correctness properties.

β-redex Apr 25, 2025, 7:17 PM
7 points
5
in reply to: Lucius Bushnaq’s comment on: Alexander Gietelink Oldenziel’s Shortform
Just to add another data point, as a software engineer, I also find it hard to extract utility from LLMs. (And this has not been for a lack of trying, e.g. at work we are being pushed to use LLM enabled IDEs.) I am constantly surprised to hear when people on the internet say that LLMs are a significant productivity boost for them.

My current model is that LLMs are better if you are working on some mainstream problem domain using a mainstream tech stack (language, library, etc.). This is approximately JavaScript React frontend development in my mind, and as you move away from that the less useful LLMs get. (The things I usually work on are using a non-mainstream tech stack and/or have a non-mainstream problem domain (but in my mind all interesting problems are non-mainstream in that sense), so this would explain my lack of success.)

β-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.