311–320 of 385 posts
Earlier quoted context omitted.
Calling Lean "AI" is quite a stretch. Though I'm also in the camp that dislikes the inflationary use of "AI" for LLMs, so I have sympathies for your viewpoint.
Finding a path in a maze was AI once.
To me "AI" is machine learning, statistical algorithms trained on data. That's not true for Lean.
Earlier quoted context omitted.
Illusion of transparency. You are imagining yourself asking this question, while standing in the gym and looking at the bar (or something like this). I, for example, have no idea how the weights are attached and which removal actions are allowed. Yeah, LLMs have a tendency to run with some interpretation of a question without asking follow-up questions. Probably, it's a consequence of RLHFing them in that way.
And none of those details matter to solve the problem correctly. I'm purposefully not putting any answers here because I want to see if future generations of these tools suddenly see the non-obvious solution. But you are right about the fact that the details matter, one detail is mentioned very explicitly that holds the key. If you do solve it don't post the answer.
You didn't even label your ASCII art, so I've no clue what you mean, are the bars at the end the supports or weights? Can I only remove one weight at a time? Initially I assumed you mean a weightlifting bar the weights on which can only be removed from its ends. Is that the case or what? What's the double slash in the middle?
Also: "what order and/or arrangement or of removing the weights" this isn't even correct English. Arrangement of removing the weights? State the problem clearly, from first principles, like you were talking to a 5 year old.
The sibling comment is correct, you're clearly picturing something in your mind that you're failing to properly describe. It seems obvious to you, but it's not.
Earlier quoted context omitted.
Is anyone working on applying these techniques to formal verification of software? My limited understanding of Rust is that it applies a fixed set of rules to guarantee memory safety. The rules are somewhat simple and limiting, for ease of understanding and implementation, but also because of undecidability. Programmers run into situations where they know that their code won't cause memory errors, but it doesn't foll…
An issue with this approach is that it may not be robust. That is, you could run into a casr where a minor modification of your program is suddenly not provable anymore, even though it is still correct. The heuristic (AI or otherwise) has necessarily limits, and if your are close to the "edge" of its capabilities then a minor change could push it across. If the proof is rooted in the programmer's understanding who ca…
Earlier quoted context omitted.
The same could be said about programmers, but we have adapted and started writing it all down so that AI cab use it.
No no, in comparison to academia, programmers have been extremely diligent at documenting exactly how stuff works and providing fairly reproducible artifacts since the 1960s. Imagine trying to teach an AI how to code based on only slide decks from consultants. No access todocumentation, no stack overflow, no open source code used in the training data; just sales pitches and success stories. That's close to how absurd…
Earlier quoted context omitted.
This is what has excited me for many years - the idea I call "scientific refactoring" What happens if we reason upwards but change some universal constants? What happens if we use Tao instead of Pi everywhere , these kind of fun questions would otherwise require an enormous intellectual effort whereas with the mechanisation and automation of thought, we might be able to run them and see!
I'm using LLMs to rewrite every formula featuring the Gamma function to instead use the factorial. Just let "z!" mean "Gamma(z+1)", substitute everywhere, and simplify. Then have the AI rewrite any prose.
Earlier quoted context omitted.
I think you suppose wrong. A statement like "the area of the square whose side is the hypotenuse is equal to the sum of the areas of the squares on the other two sides" doesn't seam out of reach of an algorithmic procedure like a classical NLP.
Sure, we can write a procedure that recognizes some formal grammar, which intersects with the natural language. Defining the formal grammar that fully captures the current natural language understanding of the mathematical community is a bit harder.
Earlier quoted context omitted.
An apt analogy. A human is a general intelligence that can fly with an F-16. What happens when we put an artificial general intelligence in an F-16? That's what happened here with this proof.
Not really. A completely unintelligent autopilot can fly an F-16. You cannot assume general intelligence from scaffolded tool-using success in a single narrow area.
I assumed extreme performance of a general AI matching and exceeding average human intelligence when placed in an F16 or an equivalent cockpit specified for conducting math proofs.
That’s not agi at all. I don’t think you understand that LLMs will never hit agi even when they exceed human intelligence in all applicable domains.
The main reason is they don’t feel emotions. Even if the definition of agi doesn’t currently encompass emotions people like you will move the goal posts and shift the definition until it does. So as AI improves, the threshold will be adjusted to make sure they will never reach agi as it’s an existential and identity crisis to many people to admit that an AI is better than them on all counts.
Earlier quoted context omitted.
> it's really not clear to me that humans would be a valuable component in knowledge work for much longer. To me, this sounds like when we first went to the moon, and people were sure we'd be on Mars be the end of the 80's. > Even ARC-AGI-2 is now at over 50%. Any measure of "are we close to AGI" is as scientifically meaningful as "are we close to a warp drive" because all anyone has to go on at this point is pure sp…
> To me, this sounds like when we first went to the moon, and people were sure we'd be on Mars be the end of the 80's. Unlike space colonisation, there are immediate economic rewards from producing even modest improvements in AI models. As such, we should expect much faster progress in AI than space colonisation. But it could still turn out the same way, for all we know. I just think that's unlikely.
Earlier quoted context omitted.
Here “much of” is doing the heavy lifting. Are you willing to commit to a percentage or a range? I work at an insurance company and I can’t see AI replacing even 10% of the employees here. Too much of what we do is locked up in decades-old proprietary databases that cannot be replaced for legal reasons. We still rely on paper mail for a huge amount of communication with policyholders. The decisions we make on a daily…
Yes, absolutely willing to commit. I can't find a single reliable source, but from what I gather, over 70% of people in the West do "pure knowledge work", which doesn't include any embodied actuvities. I am happy to put my money that these jobs will start being fully taken over by AI rapidly soon (if they aren't already), and that by 2035, less than 50% of us will have a job that doesn't require "being there". And re…