Right but... the difference between "a robot may not injure a human being" and "a robot must injure a human being" is quite important in the real world, even if the "mathematical content is correct". And if my silly example is too contrived, it still seems like this sort of thing happens all the time:
Lemme give an example of the kind of thing I'm picturing and you can tell me where it goes wrong. Lean Web tells me the following is fine:
import Mathlib
abbrev Scalar := ℂ
abbrev Real := Scalar
theorem negative_one_has_a_real_square_root :
∃ x : Real, x * x = -1 := by
exact ⟨Complex.I, Complex.I_mul_I⟩
But we know it's a lie. I hide those abbrevs in 100k lines of stuff that you haven't yet checked manually. I don't understand what could be stopping shenanigans like these, though I appreciate you trying to show me!
Okay this is more revealing, thank you. You’re saying that A and C are very small, humanly verifiable pieces of encoded logic. Can you give me an example of how Bs come into being and why they can never be wrong?
Yes but why do we write the last bit as an aside as if that’s not a massive yawning black hole for errors to hide in? All the other stuff is irrelevant, just like when Haskell and Rust people claim that if their code compiles it is correct.
Surely “the proof is the one you think it is” is the whole ballgame? Why is it impossible for a condition to be subtly reversed somewhere in the code, rendering the entire proof useless
In the real world? I’m begging for an explanation of why this is impossible because I have installed a Lean environment and it seems trivial to misname something, to mistake the order of arguments, to compare to the wrong value. There are infinitely many Lean programs that check but don’t do what they say they do, like every other language.
How many new lines of Lean do these recent Millennium Prize proofs introduce on top of known good axioms? I suppose I’m asking what the actual workflow is to inspect that code and come to the conclusion that it is faithfully reproducing the exact chain of proofs we think it is, because I know of no other substantial source code produced by LLMs that has literally zero bugs, however strong the type system of the language it’s writing in.
Hidden like any subtle bug that one might gloss over when inspecting the source code. The statement you’re trying to prove could be thousands of lines long and that semantic mismatch could occur anywhere. We seem to be very blasé about this.
So this is all great, but given that we’re being asked to accept 500k+ line Lean proofs that check but could easily have major semantic errors hidden in them, what’s the plan? These seem like uniquely fragile software artifacts, despite the excellent and robust promises made by the runtime.
My experience also. I discover new music at a higher rate than even my teens when I listened to the radio every night, and went to gigs and bought CDs weekly. I still have some music I have to use my own MP3s for but I feel incredibly well served by streaming.
Yes, we can come up with all sorts of weird situations where you can get it to be confused. But what I'm saying is it's _trivial_ to give it a simple prompt that prevents it from ever making any errors, and so I don't think it's this big LLM gotcha (of which there are many!)
Humans do make these errors when playing blindfolded. If you even the playing field and give the LLM the position at each turn, it does not make mistakes.
I maintain that the amount of effort to teach a human to do this vastly outweighs the amount of effort to teach an LLM to do this unless you're deliberately trying to make them fail. I honestly have no bigger point than that, I just think this isn't a very good thing by which to evaluate LLM capabilities. If there's no argument you'll accept, I am happy to move on.
A human wouldn't do that, they'd look at the board. I'm not disagreeing that to demonstrate clear superhuman ability the LLM should be able to do this, but it plays better than most humans blindfolded, and with fair prompts seems very good otherwise.
This is sad to hear! Early in my career I worked for a company making airport collaborative decision making (A-CDM) software. One of the most impactful projects to which I contributed was a model that calculated the exact right moment for a pilot to turn their engine on given likely pushback times etc. That saved quite a lot of fuel (and therefore cost and pollution) back in the day. It's a real shame if similar thinking isn't being applied to the problem you describe.
How long a prompt do you think would be required to cajole an LLM into making legal moves at the rate of a human? Or do you think no amount of prompting could do that?
Gotcha. I _do_ have extremely clear auditory hallucinations, especially when I'm sleepy, but I was never talented enough to write them down properly, so I can believe more vivid visual ones are possible. Just always anxious that's what people mean during these threads.
I really don't think this is the right definition. I don't think I have aphantasia: I picture things in my mind's eye, can manipulate those images, and I get the various stimulus responses described in some of the literature. But it's totally different than dreaming: it's an act of will, I can dismiss it at any time, and I would never be able to convince myself I was actually 'seeing' what I imagined.
AI curated lists of homogenous websites, flayed to their bare bones to inspire the utterly uninspired. The internet is better and weirder than this, even in these dark hours.
I remember losing sleep when I bought my RTX Pro 6000, but somehow they keep going up in price, and waddya know I’ve even done real work that appreciates the VRAM size.
Well look, the wall is already losing every point by volleying your serve so I feel like I'm on pretty strong ground here already. But give me an exact specification for your curved wall and I'll tell you how I'd beat it.