34 ms·

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 ve

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 language". 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? I think that is possible, if you have a formal language and logic that is flexible enough, and close enough to informal English. Yes, I am talking about abstraction logic [1], of course :-) So the goal would be to have English (German, ...) as the ONLY programming language, invisibly backed underneath by abstraction logic. [1] http://abstractionlogic.com http://abstractionlogic.com

AdieuToLogic 1y ago
> 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 and therefore subject to ambiguity. The inverse is not nearly as difficult to support. Much like how a property in an API initially defined as being optional cannot be made mandatory without potentially breaking clients, whereas making a mandatory property optional can be backward compatible. IOW, the cardinality of "0 .. 1" is a strict superset of "1".
- practal 1y ago
  > The problem with trying to make "English -> formal language -> (anything else)" work is that informality is, by definition, not a formal specification and therefore subject to ambiguity. The inverse is not nearly as difficult to support. 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.
  - amelius 1y ago
    LLMs are pretty good at writing small pieces of code, so I suppose they can very well be used to compose some formal logic statements.
singularity2001 1y ago
lean 4/5 will be a rising star!
- practal 1y ago
  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.
  - gylterud 1y ago
    I think type theory is exactly right for this! Being so similar to programming languages, it can piggy back on the huge amount of training the LLMs have on source code. 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.
    - practal 1y ago
      > Being so similar to programming languages I think it is more important to be close to English than to programming languages, because that is the critical part: "As close to a programming language as necessary, as close to English as possible" is the goal, in my opinion, without sacrificing constraints such as simplicity.
      - gylterud 1y ago
        Why? Why would the language used to express proof of correctness have anything to do with English? English was not developed to facilitate exact and formal reasoning. In natural language ambiguity is a feature, in formal languages it is unwanted. Just look at maths. The reasons for all the symbols is not only brevity but also precision. (I dont think the symbolism of mathematics is something to strive for though, we can use sensible names in our languages, but the structure will need to be formal and specialised to the domain.) I think there could be meaningful work done to render the statements of the results automatically into (a restricted subset of) English for ease of human verification that the results proven are actually the results one wanted. I know there has been work in this direction. This might be viable. But I think the actual language of expressing results and proofs would have to be specialised for precision. And there I think type theory has the upper hand.
kordlessagain 1y ago
This thread perfectly captures what Karpathy was getting at. We're witnessing a fundamental shift where the interface to computing is changing from formal syntax to natural language. But you can see people struggling to let go of the formal foundations they've built their careers on.
- skydhash 1y ago
  Not really. There’s a problem to be solved, and the solution is always best exprimed in formal notation, because we can then let computers do it and not worry about it. We already have natural languages for human systems and the only way it works is because of shared metaphors and punishment and rewards. Everyone is incentivized to do a good job.
- neuronic 1y ago
  It's called gatekeeping and the gatekeepers will be the ones left in the dust. This has been proven time and time again. Better learn to go with the flow - judging LLMs on linear improvements or even worse on today's performance is a fool's errand. Even if improvements level off and start plateauing, things will still get better and for careful guided, educated use LLMs have already become a great accelerator in many ways. StackOverflow is basically dead now which in itself is a fundamental shift from just 3-4 years ago.
- norir 1y ago
  Have you thought through the downsides of letting go of these formal foundations that have nothing to do with job preservation? This comes across as a rather cynical interpretation of the motivations of those who have concerns.
- mkleczek 1y ago
  This is why I call all this AI stuff BS. Using a formal language is a feature, not a bug. It is a cornerstone of all human engineering and scientific activity and is the _reason_ why these disciplines are successful. What you are describing (ie. ditching formal and using natural language) is moving humanity back towards magical thinking, shamanism and witchcraft.
lelanthran 1y ago
> 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? I think that is possible, if you have a formal language and logic that is flexible enough, and close enough to informal English. That sounds like a paradox. Formal verification can prove that constraints are held. English cannot. mapping between them necessarily requires disambiguation. How would you construct such a disambiguation algorithm which must, by its nature, be deterministic?
- practal 1y ago
  Going from informal to formal can be done using autoformalization [1]. The real question is, how do you judge that the result is correct? [1] Autoformalization with Large Language Models — https://papers.nips.cc/paper_files/paper/2022/hash/d0c6bc641a56bebee9d985b937307367-Abstract-Conference.html https://papers.nips.cc/paper_files/paper/2022/hash/d0c6bc641...
redbell 1y ago
> "English is the new programming language." For those who missed it, here's the viral tweet by Karpathy himself: https://x.com/karpathy/status/1617979122625712128 https://x.com/karpathy/status/1617979122625712128
- throwaway314155 1y ago
  Referenced in the video of course. Not that everyone should watch a 40 minute long video before commenting but his reaction to the "meme" that vibe coding became when his tweet was intended as more of a shower thought is worth checking out.
  - diggan 1y ago
    > became when his tweet was intended as more of a shower thought That was so obvious to me, and most of the people I talked to at the time, yet the ecosystem and media seems to have run with his "vibe-coding" idea as something people should implement in production yesterday, even though it wasn't meant as a "mantra" or even "here is where we should go"...
andrepd 1y ago
Not gonna lie, after skimming the website and a couple preprints for 10 minutes my crank detector is off the charts. Your very vague comments adds to it. But maybe I just don't understand.
- practal 1y ago
  Yes, you just don't understand :-) I am working on making it simpler to understand, and particularly, simpler to use. PS: People keep browsing the older papers although they are really outdated. I've updated http://abstractionlogic.com http://abstractionlogic.com to point to the newest information instead.

AdieuToLogic 1y ago

> 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 and therefore subject to ambiguity. The inverse is not nearly as difficult to support. Much like how a property in an API initially defined as being optional cannot be made mandatory without potentially breaking clients, whereas making a mandatory property optional can be backward compatible. IOW, the cardinality of "0 .. 1" is a strict superset of "1".

practal 1y ago
> The problem with trying to make "English -> formal language -> (anything else)" work is that informality is, by definition, not a formal specification and therefore subject to ambiguity. The inverse is not nearly as difficult to support. 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.
- amelius 1y ago
  LLMs are pretty good at writing small pieces of code, so I suppose they can very well be used to compose some formal logic statements.

singularity2001 1y ago

lean 4/5 will be a rising star!

practal 1y ago
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.
- gylterud 1y ago
  I think type theory is exactly right for this! Being so similar to programming languages, it can piggy back on the huge amount of training the LLMs have on source code. 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.
  - practal 1y ago
    > Being so similar to programming languages I think it is more important to be close to English than to programming languages, because that is the critical part: "As close to a programming language as necessary, as close to English as possible" is the goal, in my opinion, without sacrificing constraints such as simplicity.
    - gylterud 1y ago
      Why? Why would the language used to express proof of correctness have anything to do with English? English was not developed to facilitate exact and formal reasoning. In natural language ambiguity is a feature, in formal languages it is unwanted. Just look at maths. The reasons for all the symbols is not only brevity but also precision. (I dont think the symbolism of mathematics is something to strive for though, we can use sensible names in our languages, but the structure will need to be formal and specialised to the domain.) I think there could be meaningful work done to render the statements of the results automatically into (a restricted subset of) English for ease of human verification that the results proven are actually the results one wanted. I know there has been work in this direction. This might be viable. But I think the actual language of expressing results and proofs would have to be specialised for precision. And there I think type theory has the upper hand.

kordlessagain 1y ago

This thread perfectly captures what Karpathy was getting at. We're witnessing a fundamental shift where the interface to computing is changing from formal syntax to natural language. But you can see people struggling to let go of the formal foundations they've built their careers on.

skydhash 1y ago
Not really. There’s a problem to be solved, and the solution is always best exprimed in formal notation, because we can then let computers do it and not worry about it. We already have natural languages for human systems and the only way it works is because of shared metaphors and punishment and rewards. Everyone is incentivized to do a good job.
neuronic 1y ago
It's called gatekeeping and the gatekeepers will be the ones left in the dust. This has been proven time and time again. Better learn to go with the flow - judging LLMs on linear improvements or even worse on today's performance is a fool's errand. Even if improvements level off and start plateauing, things will still get better and for careful guided, educated use LLMs have already become a great accelerator in many ways. StackOverflow is basically dead now which in itself is a fundamental shift from just 3-4 years ago.
norir 1y ago
Have you thought through the downsides of letting go of these formal foundations that have nothing to do with job preservation? This comes across as a rather cynical interpretation of the motivations of those who have concerns.
mkleczek 1y ago
This is why I call all this AI stuff BS. Using a formal language is a feature, not a bug. It is a cornerstone of all human engineering and scientific activity and is the _reason_ why these disciplines are successful. What you are describing (ie. ditching formal and using natural language) is moving humanity back towards magical thinking, shamanism and witchcraft.

lelanthran 1y ago

> 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? I think that is possible, if you have a formal language and logic that is flexible enough, and close enough to informal English. That sounds like a paradox. Formal verification can prove that constraints are held. English cannot. mapping between them necessarily requires disambiguation. How would you construct such a disambiguation algorithm which must, by its nature, be deterministic?

practal 1y ago
Going from informal to formal can be done using autoformalization [1]. The real question is, how do you judge that the result is correct? [1] Autoformalization with Large Language Models — https://papers.nips.cc/paper_files/paper/2022/hash/d0c6bc641a56bebee9d985b937307367-Abstract-Conference.html https://papers.nips.cc/paper_files/paper/2022/hash/d0c6bc641...

redbell 1y ago

> "English is the new programming language." For those who missed it, here's the viral tweet by Karpathy himself: https://x.com/karpathy/status/1617979122625712128 https://x.com/karpathy/status/1617979122625712128

throwaway314155 1y ago
Referenced in the video of course. Not that everyone should watch a 40 minute long video before commenting but his reaction to the "meme" that vibe coding became when his tweet was intended as more of a shower thought is worth checking out.
- diggan 1y ago
  > became when his tweet was intended as more of a shower thought That was so obvious to me, and most of the people I talked to at the time, yet the ecosystem and media seems to have run with his "vibe-coding" idea as something people should implement in production yesterday, even though it wasn't meant as a "mantra" or even "here is where we should go"...

andrepd 1y ago

Not gonna lie, after skimming the website and a couple preprints for 10 minutes my crank detector is off the charts. Your very vague comments adds to it. But maybe I just don't understand.

practal 1y ago
Yes, you just don't understand :-) I am working on making it simpler to understand, and particularly, simpler to use. PS: People keep browsing the older papers although they are really outdated. I've updated http://abstractionlogic.com http://abstractionlogic.com to point to the newest information instead.