> The field in question is formal verification. It’s notable that those two words appear nowhere on Bend’s webpage or in its codebase. The developer has built an entire language around a field seemingly without realising that said field exists.

I checked the developer's X account, they have written numerous posts about formal verification, so this specific claim ("without realising that said field exists") seems to be false.

It's amusing to me this entire article is centered around brow beating this and other hypothetical software authors for starting things without doing a small amount of research first to understand the very basics of what they're getting into.

If the author of the article had done just a small amount of research about bend or it's author before writing the article they would have known pretty quickly what they were saying was incorrect.

I think the larger pattern here is that nuance is one of the most valuable commodities in the AI era. If you're hand waving stuff away without even missing , you're going to miss a lot of stuff in this cycle.

This article reminds me a lot of the famous hacker news Dropbox comment.

Back in 2018 they were working on Formality, an Ethereum formal verification project. They are the Victor in this video about it: https://slideslive.com/38911748/introducing-formality

Here's the GitHub repo for that, which demonstrates familiarity with formal proofs that long predates LLMs https://github.com/VictorTaelin/Formality

Victor here. I haven't "worked" on Formality. I've founded it. Designed every part of it. Before LLMs!

sighs

Here's my response to this ridiculous accusation: https://news.ycombinator.com/item?id=49753898

I can't internet anymore. I need a beach

Sympathize with you mate, this article just seems like a poorly researched hit job.

The article is about vibe coding, bend is the main character because it made frontpage.

The author here says as much in the introduction, that it is not about whomever is behind bend, but the larger trend

The author here has also added bend's author's link (in GP) to the original post, they very much do not seem to be doing a "hit job" and their intent is to comment on patterns from vibe coding

Bend's developer has posted a well-argued response here: https://news.ycombinator.com/item?id=49753898

I am glad I saw it, as now I am interested in learning more about Bend.

To be fair, if the two words indeed don't appear in either the webpage or the codebase, it is a bit strange. It's like implementing a whole Google alternative without ever using the words "search engine".

He claimed the guy did no research while himself doing no research? I'm shocked! Shocked! Well, not that shocked.

I don't want to change that sentence now that people have discussed it, but I have added a note to the top to make it clear that I'm just taking it as an example of a vibe-coded program because it's recent and high profile.

My critiques of the language itself are not the main point, although I do still think that it's a very bad design to have a LLM waste tokens on a proof that could be written by CVC etc..

>I don't want to change that sentence

>but I have added a note to the top

you know what's the least you could actually have done instead? no, you don't need to retract the blog post at all, keeping it up was the right choice. Now slap a big ass apology for being an unaware snob on top of it instead of leaving a link to the author's reply, like an after thought.

> Look like how AI slop has unrealistic physics

> Posts a link to real moon landing footage

I'd delete the article if I was you...

You know, in academia, they sometimes retract articles, even if they believe they are directionally correct

I feel that that's the worst option because it only leaves people who have read it without the added context at the start. If someone convinces me that I'm wrong then I'm happy to do so though.

François Chollet wrote in February that he expected ARC-3 to be saturated in "about one year".

"Frontier models today perform very poorly with a minimal harness. However if big labs start directly targeting the benchmark like they did for ARC-2, numbers will go up fast."

https://x.com/fchollet/status/2022054537293705260

Chollet writes he expects AGI now sooner than 2030, "given progress is happening faster than I expected."

https://x.com/fchollet/status/2095607046129463577

I have no idea about timelines, but the current LLM architecture has no mechanism which could emulate online learning in a way similar to how it happens in humans and other animals. As another commenter wrote, there is no neuroplasticity while these systems interact with their environment in normal usage; adding information/constraints to the context partially mitigates this, but it's a completely different mechanism.

The RL phase is the most similar mechanism I know of that comes to my mind, but I'm not sure it could be adapted to fill that gap.

My totally unsubstantiated theory is that this is the missing link towards what most humans would consider AGI. I don't see this as intractable, but it may require some substantial change in architecture.

We've had that concept for quite a long time now, in the form of Lora [1] and similar fine-tuning techniques.

It first got popular for StableDiffusion to teach the image generation models new concepts.

We could easily live in a world where you can train / build Loras to encompass your entire code base history, company knowledge base, new skills, etc.

Then the models would start with a baseline that already has all the important knowledge without needing to cram it into the context.

This still isn't on the fly learning, but you could imagine daily or weekly training runs to regularly incorporate new knowledge.

I think the main reason this hasn't happened yet is that the shared batch based efficient serving architectures used today wouldn't support that structure well.

[1] https://en.wikipedia.org/wiki/LoRA_(machine_learning)

Yes, that could be a way to achieve that. After all, even humans have short term and long term memory, and it looks like sleep is a very important "tick" to connect the two, so it's not all just continuous.

For sure, doing it for all users would be economically unfeasible. I wonder if the labs are experimenting with something similar, though.

Chain of thought reasoning is really good, true, but agents really took off with tool calling and being able to integrate with a bunch of stable tools.

In some sense, creating good new abstractions externally and learning those is a form of "learning", on a very large timescale. The AI model is not necessarily doing the whole "look at the whole space holsitically and find a key invariant", but if you let other people do that you can enable new capabilities that were previously unknown.

Tools and capacities, man.

How is that an argument to the comment you replied to?

Astra is clearly able to acquire new knowledge in context and apply it. It was the whole thing that his ARC-AGI benchmarks have been measuring. It's a direct refutation of the original comment.

None of these LLMs are plastic. They lack neurodiversity. Their thought space and their traversal are likely constrained in someway that humanity's isn't as a collective.

Is it possible to have neuroplasticity and still keep them aligned?

I have neuroplasticity, and I am aligned. ;)

Are you (at least partially) aligned out of existential fear of repercussions (getting fired, losing your life, going to prison), which LLMs don't have?

Humans are famously horribly aligned, plenty of examples in history.

Hmm. Examples of horrible alignmnent don't necessarily outweigh the fact that most people, most of the time, mostly behave in a way that is socially aligned. (Though I'm speaking in terms of intent, conveniently ignoring the side effects / negative externalities of our collective behavior.)

When threatened with physical or social harm. What they think in their little heads though :)

But are other people?

how do you imagine that would work? you being able to. influence globally stored weights with some prompts? we have fine-tuning for that.

Yet I can't randomly order another person to steal a car for me, just because I tell them to. Alignment for an intelligent system is a hard problem and at this stage is seems close to unsolvable.

My guess is that we'll just ignore it and make money along the way and every 2-3 months we'll have the equivalent to "Equifax gets hacked and millions of user records are stolen", etc. (this time with the LLM itself doing the hacking at someone's behest - accidental or not).

What does this even mean. There is strong evidence of LLMs doing in context learning.

Some of the linear RNN layers in recent models are provably doing SGD in hidden space during inference

By in context learning do you mean latent space?

https://transformer-circuits.pub/2021/framework/index.html

> What does this even mean. There is strong evidence of LLMs doing in context learning.

1. Is this learning persistent?

2. Do they verify these new lessons against core principles?

3. Do they and protect themselves/ignore requests if these new lessons contradict those core principles?

Humans do that from the time they're 3 years old (not that well, but they do do it).

Yes. Yes. Yes.

In my experience all those claims are false.

So the next step is to ask for evidence and ideally independent and peer reviewed research.

You know they can take notes, right?

And ICL dates all the way back to 2020, at least: https://arxiv.org/abs/2005.14165

That's training during training. They can't learn afterwards.

do you have a reference where that claim is demonstrated?

surely it can only acquire new knowledge if it were updating it's weights as it is used?

> The cost of generating the proofs for all 10 of these breakthroughs combined was under $2,000 at Sol API prices.

https://x.com/polynoamial/status/2083470822258467194

That's clearly just for the tokens, this doesn't really answer OP's question.

Yeah sure but they didn't just throw a 5 year old at an LLM with $2,000. If you want good math results from LLMs you need to have math PhDs.

> The incredible Yitan Zhang (https://newyorker.com/magazine/2015/02/02/pursuit-beauty) worked on proving this conjecture for 7 years. Moh, his advisor, wrote that Zhang "failed miserably" in proving the Jacobian conjecture, "never published any paper on algebraic geometry" after leaving Purdue, and "wasted seven years of his own life and my time".

https://x.com/aminkarbasi/status/2079129649830137989

https://en.wikipedia.org/wiki/Yitang_Zhang

Zhang, Yitang’s life at Purdue (Jan 1985-1991) T.T.Moh - https://www.math.purdue.edu/~ttm/ZhangYt.pdf

kind of a wild document to exist...

This doc is insane.

Moh repeatedly:

calls Zhang’s words “fake” and his claim “a lie”;

speculates, without demonstrating it, that Zhang “fooled” professors to get admitted;

says Zhang “failed miserably” and “wasted seven years of his own life and my time”;

alleges that Zhang “wanted to be famous all the time”;

publishes an irrelevant and humiliating story about Zhang not attending his father’s funeral;

says he would not touch Zhang “with a five feet pole”;

repeatedly emphasizes his own generosity, influence, mathematical work and supposed sacrifices.

The world doesn’t need advisors like Moh that are bitter enough to gossip about a family funeral.

He's not dead, but it is bad to gossip regardless.

They are referring to Moh's gossip about Zhang's father's funeral in the above (and Zhang's father is very much dead, unfortunately).

The document says more about the kind of advisor Moh was than the kind of mathematician Zhang is.

Interestingly: "For logic proof, it had been thought that AI could handle all logic problems in the near future, hence logic problems of solving conjectures might not be so interesting in the future."