121–130 of 827 posts
Earlier quoted context omitted.
[flagged]
Maybe we can collect all of this salt and operate a Thorium reactor with it, this in turn can then power AI.
Can we please stop standardizing on putting things in the root? /.well-known/ exists for this purpose. example.com/.well-known/llms.txt https://en.m.wikipedia.org/wiki/Well-known_URI
You can't just put things there any time you want - the RFC requires that they go through a registration process. Having said that, this won't work for llms.txt, since in the next version of the proposal they'll be allowed at any level of the path, not only the root.
Excuse me???
The beginning was painful to watch as is the cheering in this comment section. The 1.0, 2.0, and 3.0 simply aren't making sense. They imply a kind of a succession and replacement and demonstrate a lack of how programming works. It sounds as marketing oriented as "Web 3.0" that has been born inside an echo chamber. And yet halfway through, the need for determinism/validation is now being reinvented. The analogies make…
Great talk, thanks for putting it online so quickly. I liked the idea of making the generation / verification loop go brrr, and one way to do this is to make verification not just a human task, but a machine task, where possible. Yes, I am talking about formal verification, of course! That also goes nicely together with "keeping the AI on a tight leash". It seems to clash though with "English is the new programming l…
lean 4/5 will be a rising star!
I am betting though that type theory is not the right logic for this, and that Lean can be leapfrogged.
Where do these analogies break down? 1. Similar cost structure to electricity, but non-essential utility (currently)? 2. Like an operating system, but with non-determinism? 3. Like programming, but ...? Where does the programming analogy break down?
only in English, and also non-deterministic.
English is soooooo ambiguous
It’s fascinating to think about what true GUI for LLM could be like. It immediately makes me think a LLM that can generate a customized GUI for the topic at hand where you can interact with in a non-linear way.
Fun demo of an early idea was posted by Oriol just yesterday :) https://x.com/OriolVinyalsML/status/1935005985070084197
I like my tools to be predictable. Google search trying to predict that I want the image or shopping tag based on my query already drives me crazy. If my entire operating system did that, I'm pretty sure I'd throw my computer out a window.
Earlier quoted context omitted.
lean 4/5 will be a rising star!
You would definitely think so, Lean is in a great position here! I am betting though that type theory is not the right logic for this, and that Lean can be leapfrogged.
I am not sure lean in part is the right language, there might be challengers rising (or old incumbents like Agda or Roq can find a boost). But type theory definitely has the most robust formal systems at the moment.
Great talk, thanks for putting it online so quickly. I liked the idea of making the generation / verification loop go brrr, and one way to do this is to make verification not just a human task, but a machine task, where possible. Yes, I am talking about formal verification, of course! That also goes nicely together with "keeping the AI on a tight leash". It seems to clash though with "English is the new programming l…
> So the question is, can you hide the formal stuff under the hood, just like you can hide a calculator tool for arithmetic? Use informal English on the surface, while some of it is interpreted as a formal expression, put to work, and then reflected back in English? The problem with trying to make "English -> formal language -> (anything else)" work is that informality is, by definition, not a formal specification an…
Both directions are difficult and important. How do you determine when going from formal to informal that you got the right informal statement? If you can judge that, then you can also judge if a formal statement properly represents an informal one, or if there is a problem somewhere. If you detect a discrepancy, tell the user that their English is ambiguous and that they should be more specific.
You can generate 1.0 programs with 3.0 programs. But can you generate 2.0 programs the same way?
I don't think it's currently possible to ask a model to generate the weights for a model.