Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Litex: The First Formal Language Learnable in 1-2 Hours

github.com

Post reply on HN
Print view View original

61–70 of 86 posts

Re: Litex: The First Formal Language Learnable in 1-2 Hours

#61

Post by mkl »

teiferer wrote: post #40
1dom wrote: post #28

Earlier quoted context omitted.

No you're not questioning it, you're making statements against it, without evidence, which is just as useless as the statement without evidence. Like I suggested, like the person you responded to suggested: when science tries to prove or disprove LLM intelligence it generally descends into disagreements about definition or evidence (neither of which you provided). The reason why no evidence was provided for the origi…

My claims: 1. LLMs are widely called "intelligent". Evidence for my claim: The term "artificial intelligence" that is used everywhere. It has its own TLD. 2. There is no evidence that this terminology is applicable. Questioning it faces some variant of "well do you have evidence to the contrary?". Evidence for my claim: This thread. You are welcome to disprove my claims, as in the scientific spirit that you say you u…

> The term "artificial intelligence" that is used everywhere. It has its own TLD.

That's the country code TLD for Anguilla: https://en.wikipedia.org/wiki/.ai

Re: Litex: The First Formal Language Learnable in 1-2 Hours

#63

Post by exe34 »

teiferer wrote: post #40
1dom wrote: post #28

Earlier quoted context omitted.

No you're not questioning it, you're making statements against it, without evidence, which is just as useless as the statement without evidence. Like I suggested, like the person you responded to suggested: when science tries to prove or disprove LLM intelligence it generally descends into disagreements about definition or evidence (neither of which you provided). The reason why no evidence was provided for the origi…

My claims: 1. LLMs are widely called "intelligent". Evidence for my claim: The term "artificial intelligence" that is used everywhere. It has its own TLD. 2. There is no evidence that this terminology is applicable. Questioning it faces some variant of "well do you have evidence to the contrary?". Evidence for my claim: This thread. You are welcome to disprove my claims, as in the scientific spirit that you say you u…

the way it goes is that a device/program of some sort displays a broad number of behaviours that previously was believed to be a future sign of artificial intelligence (e.g. somewhat coherent text, Turing test, giving the impression of following instructions and arriving at the correct results, etc).

some people claim this is artificial intelligence of a lower quality than humans, and these people expect that such mechanisms will eventually match and then potentially surpass humans.

then there's another crowd coming along and claiming no, this isn't intelligence at all, for example it can't tie its shoelaces.

my point was that every time you try to say that no this can't be what intelligence means, it needs to do X, I can find a human who can't do X, no matter how many years you might try to coach them. (for example, I will never be a musician/composer. I simply lack the gene.)

The retort is always "oh but in principle a human could do this". well, maybe next year's LLM will do it in practice, not just in principle, for all I know.

As they say, person who says it can't be done should not stop person doing it.

Heavier than air flight was once thought to be impossible. As long as you don't have a solid mathematical theorem that says only carbon replicators born from sexual intercourse can be intelligent, I expect some day silicon devices will do everything carbon creatures can do and more.

Re: Litex: The First Formal Language Learnable in 1-2 Hours

#64

Post by exe34 »

card_zero wrote: post #20
teiferer wrote: post #19

Earlier quoted context omitted.

That's underestimating human intelligence. Even low-IQ humans can in principle learn how to use Lean to represent a multivariate system. It might take a while, but in principle their brain is capable of that feat. In contrast, no matter how long I sit down with ChatGPT or Gemini or whatnot, it won't be able to. Because they are not intelligent. It's a great achievement of the AI hype that the burden of proof has been…

IDK, they look intelligent, like the world looks flat.

As opposed to most humans? Have you tried reasoning with somebody "just trying to do my job sir"?

Re: Litex: The First Formal Language Learnable in 1-2 Hours

#65

Post by ngruhn »

CaptainOfCoit wrote: post #45
ngruhn wrote: post #36

Earlier quoted context omitted.

fyi: they finally renamed Coq. It's called Rocq now.

Guess they had to change the logo too? Just because evangelical anglophone users couldn't get past the name sounding like "cock" or what?

Yes, but I don't think it has anything to do with evangelicalism. It's just like Uranus. You can't talk about without it always being a bit unserious.

Re: Litex: The First Formal Language Learnable in 1-2 Hours

#66

Post by layer8 »

The title seems to be misusing the term “formal language”: https://en.wikipedia.org/wiki/Formal_language

The simplest formal language is the empty set, which I would argue doesn’t take hours to learn.

So “formal language” is almost certainly not what is meant here, but it’s not clear what else exactly is meant either.

Re: Litex: The First Formal Language Learnable in 1-2 Hours

#68

Post by aitchnyu »

aktuel wrote: post #15
Almondsetat wrote: post #5

This github README is written by an LLM.

It is more likely that the author is not a native english speaker (project author seems to be chinese) and may have used some tool to help with the translation.

I have also been accused of being a Markhov chain, before 2022. I communicate in English only for work and social media so writing may sometimes seem strange to native speakers.

Re: Litex: The First Formal Language Learnable in 1-2 Hours

#69

Post by teiferer »

gus_massa wrote: post #60
teiferer wrote: post #12

Earlier quoted context omitted.

Kids hardly know what a multivariate equation is. Unless you use "kid" to denote 20-year old college students enrolled in a math program which some people do. The other claim is doubtful too: > while it require an experienced expert hours of work in Lean 4. No, it doesn't. If you have an actual expert, it only takes a few minutes. And besides, isn't this exactly what an artificial intelligence would solve? Take some…

I studied 2x2 linear equation system in high school at 14 (13?) y.o. It was a technical school with more math and physics, and later specialization (like chemistry, electronics, building, ...). I think in a normal school they study that at 16 y.o. We also teach 2x2 systems to 18 y.o. in the fists year of the university for architects, medics and other degree that don't need a huge amount on math. (Other degrees like…

And if you ask one of those medics 5 years later to solve one, the response might make you depressed. (Or just 4 weeks after their maths exam.)

Re: Litex: The First Formal Language Learnable in 1-2 Hours

#70

Post by teiferer »

exe34 wrote: post #63
teiferer wrote: post #40

Earlier quoted context omitted.

My claims: 1. LLMs are widely called "intelligent". Evidence for my claim: The term "artificial intelligence" that is used everywhere. It has its own TLD. 2. There is no evidence that this terminology is applicable. Questioning it faces some variant of "well do you have evidence to the contrary?". Evidence for my claim: This thread. You are welcome to disprove my claims, as in the scientific spirit that you say you u…

the way it goes is that a device/program of some sort displays a broad number of behaviours that previously was believed to be a future sign of artificial intelligence (e.g. somewhat coherent text, Turing test, giving the impression of following instructions and arriving at the correct results, etc). some people claim this is artificial intelligence of a lower quality than humans, and these people expect that such me…

> my point was that every time you try to say that no this can't be what intelligence means, it needs to do X, I can find a human who can't do X,

Indeed, the point you are making is reasonable. But I'm trying to say that the premise is wrong. Nobody should be expected to come up with a reason why it is not intelligence. We should expect to be presented with evidence that it is intelligence. Absent that, the null hypothesis is that it isn't, just like any other computer program before isn't, uncontroversially.

I'm sure you already got my point, apologies for repeating it, but some clarification to clearly carve out our points may not hurt.

Post reply on HN