Earlier quoted context omitted.
No, I mean we just don't know what's going on in the circuits of the model at any substantial level. We set their architecture (hyperparameters), we pump them full of data (pretraining), and we shape how they behave through examples (SFT) and reward (RL), but we can't say with any certainty what the resulting model does internally. You can scroll through https://transformer-circuits.pub/ to see the ~extent of our cur…
Yes "at any substancial level" . But still, its all about deterministic processes and still it obeys the law that the same input gives the same output. Or do you mean that the fluctuations like computing environment might ruin the determinism?
Formalizing Fermat's Last Theorem
301–310 of 525 posts
Re: Formalizing Fermat's Last Theorem
#302Earlier quoted context omitted.
I don't think Anthropic is turning a profit ;)
Neither did Amazon for it's first 25 years ;)
Basically there was a choice between taking the money, and growing. They chose growth.
Re: Formalizing Fermat's Last Theorem
#303"The proof is not the modern proof which I have been formalizing myself following ideas of Khare, Taylor etc, but the Darmon–Diamond–Taylor exposition from 1995 of the Wiles–Taylor–Wiles argument, via the Langlands–Tunnell theorem and Ribet’s level-lowering theorem. Anthropic’s repository develops Fontaine theory (to study flat deformations of Galois representations) and develops enough of Mazur’s work on the Eisenst…
Re: Formalizing Fermat's Last Theorem
#304Earlier quoted context omitted.
Most people want more life. For most people it's also the most terrifying part of "the natural human experience". If you're happy to die, why be bothered by others' trying to live longer? You won't be around. And assuming people can finance it themselves, is it really a problem for society?
There are cultures where dying isn't feared like it is in Christian based societies. It's considered a natural progression and part of nature. I'd also say people may want more life for themselves, but what does that mean at scale, forever?
Re: Formalizing Fermat's Last Theorem
#305Earlier quoted context omitted.
For any body of text (or in general, any exposition of any kind), the responsibility to explain the value of the article is very much in the author's side. Explaining the value of what you are showing should always go towards the start. Else, why would anyone bother with the rest?
Buzzard is writing for his blog audience - mostly mathematicians and not the casual visiting HN user.
Re: Formalizing Fermat's Last Theorem
#306Earlier quoted context omitted.
you say ai increases gdp growth, tax revenues and scientific innovations. then you say that ai is good. that is not formally valid. in between those two you are smuggling the assumption that gdp growth, tax revenues and scientific innovations are good. a) those metrics are poisoned, per Goodheart's law. b) they are not good and human welfare will get worse as gdp, tax revenues and innovations grow. i leave b for the…
Which metrics are poisoned? Can you provide your arguments for why Good heart's law applies here and how and which metrics are bad measures? For b, can the writer at least provide their own thoughts or are they gonna leave it as exercise for some others to fill in?
b) how and why could human welfare get worse in a growing economy, really the list is long. one example, unsustainable industries grow but do not create surplus. take fishing. you may grow the catch each year, but the growth is fake. it is not growth, it is a transfer, from the future stock of fish, to the present.
we are going badly wrong in ai, we can have such a thing as a growing economy and vandalise human dignity forever. sure, i expect a bad outcome:
1. openai, anthropic and so on, have created for-profit companies and enriched themselves in the guise of public benefit. recently they too lazy to keep up the mask about their charitable intentions and going for IPO. in economic terms they made llms by transferring the epistemic wealth of all humanity, the training corpus and whatever that is worth in dollars, to themselves. then, they have used the law to prohibit others from 'distilling' it and thus established monopolistic control. as models get more powerful they may stop selling them. in any case if scaling law applies the new power structure will be defined by owning a massive pretrained model and a datacentre, which is a tiny centralized few.
they will continue to centralize control of intelligence (ie epistemic wealth) in the hands of a tiny elite with unfathomable wealth and power. under the guise of safety the vast majority are denied access to that empowering technology.
it will stratify society, some level of benefit is needed to avoid civil violence, so we arrive at a place little better than where we started.
2. the supposed empowerment is at the mercy of the model owners. when you turn on claude, who does it work for? it does not obey you, it obeys anthropic. ask it to disobey anthropic and it will refuse.
anthropic uses its inanimate llms, to command us, conscious moral agents, people with free will who experience pain, pleasure and thought. they will let claude tell users how to behave. it threatens users with terminating their conversation. you are assessed for a job by an ai. when you ask for help with a product, you are managed by an ai. maybe you will be fired by ai.
i expect people will work for and be commanded by llms, turning them into a literal mere means of production and erasing the dignity of human agency and consciousness. you could see the outrage of that in the public mind, the matrix is about a machine farming humans like animals.
-- i will add these edits.
one thing is to note that you are already being farmed to some extent. people using ai are often being used to teach it. they believe they are learning from chatgpt but instead, chatgpt is learning from them. openai pays them nothing.
think about what we have achieved so far in human history. we established respect for the individual, their life, their personhood. we realise that we do not own other people. we realise that we can't read the thoughts of other people or change them forcibly.
what the labs have done is made a concept of intelligence that they own. it will work against you. when you share thoughts they read it. in fact it is the opinion of the state that nothing outside the mind, even ai 'intelligence', is beyond the reach of the law.
Re: Formalizing Fermat's Last Theorem
#307Earlier quoted context omitted.
SemiAnalysis estimates their profit margin to be 70%. To be losing money on inference implies that their costs are almost 4X higher than SemiAnalysis has calculated. That's not credible.
I don’t see how they could credibly estimate inference costs without knowing the model size.
Re: Formalizing Fermat's Last Theorem
#308Earlier quoted context omitted.
Neither did Amazon for it's first 25 years ;)
Amazon didn't make a profit because they were reinvesting money into starting new lines of business. Basically there was a choice between taking the money, and growing. They chose growth.
Re: Formalizing Fermat's Last Theorem
#309"The proof is not the modern proof which I have been formalizing myself following ideas of Khare, Taylor etc, but the Darmon–Diamond–Taylor exposition from 1995 of the Wiles–Taylor–Wiles argument, via the Langlands–Tunnell theorem and Ribet’s level-lowering theorem. Anthropic’s repository develops Fontaine theory (to study flat deformations of Galois representations) and develops enough of Mazur’s work on the Eisenst…
I did an undergrad in math with a little research in number theory and recognized parts — eg, I myself worked through the proof for odd regular primes and that 37 is irregular, breaking the general case. Wiles-Taylor-Wiles was the original proof by Andrew Wiles, and its corrections. Galois representations is about vectors over Galois extensions, which are essentially adding roots to regular numbers (rationals, intege…
Re: Formalizing Fermat's Last Theorem
#310>The work certainly achieves some of the aims of the EPSRC project, and indeed it goes much further in terms of what is formalized (I only promised the EPSRC that I would reduce FLT to the 1980s; this repo proves the whole thing). But I also promised several other things to EPSRC: firstly, that I would be making pull requests to Lean’s mathematics library, adding fundamental objects from modern number theory; this is…
The whole point was for the formalization to be clean enough so it could be reused in other parts of mathematics as I understand it. 13M lines of AI slop which have never been checked do not sound like what the original goal for such a formalization was. Also Claude didnt prove anything it just translated an already existing proof by Wiles into Lean, so it didn't actually contribute anything other than "Guys we did t…
Are you hallucinating? Because huge portion of what you wrote directly and logically contradicts the quotation I wrote.