> Just as not every monotonically increasing function diverges to infinity, Recursive Self Improvement doesn't necessarily lead to ASI
It is disappointing just how little recognition there is of this point. For some reason, AI maximalists settled on an exponential model of growth in their mind, and I've yet to see one seriously consider whether RSI might not be that. It's a conversation ender, like bringing up an alternative axiom that cannot be debated, rather than a testable hypothesis.
I agree that exponential growth in particular is debatable, but if intelligence doesn't diverge to infinity then it must have an upper bound, which doesn't seem very believable. Intuitively, it should always be possible to add one more processing unit to increase your intelligence (however it is measured) by a fixed amount. So I don't think it can be below linear.
Hey, I appreciate your interest in the conversation!
> Intuitively, it should always be possible to add one more processing unit to increase your intelligence (however it is measured) by a fixed amount.
That's reasonable. The question is how much return you get on your investment, and whether there are "diminishing returns" or "economies of scale" for IQ-per-dollar.
> I agree that exponential growth in particular is debatable, but if intelligence doesn't diverge to infinity then it must have an upper bound, which doesn't seem very believable ... I don't think it can be below linear.
Being able to always increase your intelligence by some amount, at some cost, is compatible with any of "fixed upper bound" (e.g. exponential decay), "sublinear unbounded growth" (e.g. logarithmic), "linear growth," or "superlinear growth" (e.g. exponential growth). Sublinear growth and diminishing returns certainly seem consistent with every self-optimizing system we've seen so far, including agentic AI.
> How you allow people to purchase your offerings is part of the business and has its own costs associated with it.
I agree. Complaining "I have money, now give me your product!" is tantamount to "I have a product, now give me your money!"
That said, this and so many other aspects of a functional capitalist society rely on customers and corporations having roughly equal leverage over one another. But since corporations have insanely centralized bargaining power as collectives, have bent the legal system in their favor at every turn, and are consistently overprivileged by technological innovation (AI-as-price-researchers being one of the few exceptions), I have long since abandoned any social contract with them.
The reason HF didn't win a legal battle is because they didn't sue, and they didn't sue because OpenAI is their business partner (or at least are closely wedded through their mutual partner Nvidia). If HF really wanted to press charges, it's very likely they would have won on any demonstrable claims of damage.
If HF did have any hard feelings about the event, they were likely settled with OpenAI out-of-court.
Becoming a surface level/"vapid" work automaton would be a heavy price for to pay, perhaps not for you personally, but for me and I imagine many others. So, I'm not sure your example would lead me to the conclusion of your behavior. You mention being called at 3am as one incident that didn't mean much to you at the time and didn't become a pattern of exploitation, so what was really lost?
Maybe I'm lucky. I've so far not had to endure a job for which I was underpaid and expected to meet and exceed every contractual obligation placed on me.
The bar for Turing-complete is very low. The halting problem is to programming as Godel's incompleteness theorem is to metamathematics. Yet no one is seriously suggesting that we downgrade to axiomatic systems incapable of expressing Peano arithmetic, nor that our current axiomatic systems are impractical for proving theorems.
We cannot automatically and completely verify nontrivial semantic properties of arbitrary programs written in a Turing-complete language (Rice's theorem), but as long as we as humans can intuit correctness arguments for our programs, then formal methods will apply to it. Of course, declarative rather than imperative programming semantics tend to result in simpler correctness arguments, sidestepping reliance on global state and convoluted loop invariants.
I just don't think we need turing completeness to solve the problems we try to solve with software. You bring up how humans can reason and prove correctness for our programs, but I say we just force them to do that (making our programs no longer turing complete). I don't think I've ever encountered a problem that required steps that I didn't think I would be able to prove halted.
> I recognize that there is probably no objective way to deductively prove it because of the Halting Problem etc.
There is. But it will only be reliable if every transitive dependency of your codebase, all the way down to the hardware level, has been formally verified. Failing that, you have to rely on opaque contracts at the boundaries, and those are just promises that may be mistaken.
The Halting problem, Rice's theorem, etc. only apply if your goal is to automatically and completely deduce properties or their violations for arbitrary programs. If your goal is simply to prove security and correctness properties for well-understood classes of programs in industry, then there are no fundamental obstructions.
Formal verification is not magic. It can execute deductive proofs, but the relevance and utility of those results is a question of human values. Spec bugs are a thing. Bad design is a thing. Out-of-scope usage is a thing. Even a halting oracle won't help with those.
Not sure why you're responding with information that would imply they modeled Rust in Lean or vice versa. As I explained, their target was the compiled ELF binary, not Rust source. This way, they avoid including the entire Rust compiler and its as-yet formally undefined semantics into the trusted computing base. They lose guarantees about any compiled Signal binary that is not bit-for-bit this one, though.
Rust need not apply, since the proof is about the libsignal-cli ELF binary, compiled under reasonable assumptions (single-threaded, statically linked, etc). The semantics of the some-hundred instructions in their language in Lean were tested to adhere to Arm-provided ASL spec, as compared to two independent emulators.
It is disappointing just how little recognition there is of this point. For some reason, AI maximalists settled on an exponential model of growth in their mind, and I've yet to see one seriously consider whether RSI might not be that. It's a conversation ender, like bringing up an alternative axiom that cannot be debated, rather than a testable hypothesis.
reply