wewbull

joined 3 years ago
[–] wewbull@feddit.uk 8 points 13 hours ago (1 children)

In the UK constitution there are laws that state that no government may bind the hands of a future government and that a vote can always be superceded by another vote.

Does the US not have such laws?

[–] wewbull@feddit.uk 1 points 15 hours ago (1 children)

5 years ago we were mid-pandemic. That's a big knowledge gap.

[–] wewbull@feddit.uk 1 points 15 hours ago (1 children)

The data is there, but it's not in what those companies say. It's in the books of the companies they have relationships with.

I do agree with your second statement though.

[–] wewbull@feddit.uk 4 points 20 hours ago (1 children)

I'm not sure how much distillation and building on top of each others results is going on. I could see all the models freeze in development when the money leaves the segment.

A model frozen in the past has limited usefulness.

[–] wewbull@feddit.uk 2 points 20 hours ago (3 children)

If you want it's "knowledge" to be up to date, the training never ends.

[–] wewbull@feddit.uk 4 points 22 hours ago (5 children)

Why wouldn't you include training? Training is vital to their product.

[–] wewbull@feddit.uk 5 points 22 hours ago (3 children)

They're playing all kinds of games with the numbers right now. They're trying to IPO so hiding costs under other headings outside the core business. Don't trust what they openly state. It's far worse.

[–] wewbull@feddit.uk 3 points 22 hours ago

I think you're probably a couple of orders of magnitude too low.

[–] wewbull@feddit.uk 3 points 23 hours ago (1 children)

I really hope not, because that's how they steal money from working people with 401k plans.

[–] wewbull@feddit.uk 2 points 23 hours ago

They started it.

[–] wewbull@feddit.uk 1 points 23 hours ago

Just invest in the things that we actually need. Renewables for example.

[–] wewbull@feddit.uk 2 points 23 hours ago

Useful doesn't mean profitable, sustainable or cost effective.

You're not paying the real cost right now.

 

Okay, we have a new contender for Most AI Thing to Ever Happen

  1. July 25th: someone messes around with an LLM and posts a proof of the Collatz conjecture that does, in fact, verify in the theorem prover. (The AI use is not disclosed on the github page) https:// github.com/xrchz/CollatzLean

  2. July 26th: several serious bugs are posted in the theorem provers, that in principle could allow a false statement to be "proven" true. They're serious, yes, but no need for panic, because you're not going to blunder into accidentally exploiting the bugs while writing a proof, probably. https:// github.com/leanprover/lean-kernel-arena/pull/81

  3. July 28th: someone who was right to be very skeptical of the Collatz proof, and had the expertise to study it with a fine-toothed comb, discovered it was exploiting a bug https:// github.com/leanprover/lean4/issues/14576

  4. The "proof" turns out to be exploiting multiple similar but distinct bugs to pass different solver variants!

  5. the human who posted the proof acknowledges the AI use and claims they did not knowingly point it towards the bugs it exploited. https:// leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/Counterexample.20to.20the.20Lean.20Conjecture.20.28Soundness.20Bug.29/near/613135216

Note that the proof was posted shortly before the related bug reports were posted. It is an open question if the AI found people discussing the bugs shortly before they were formally posted and "decided" to exploit them, if the AI "knew about it" as a learned strategy from the training stage (putting every single "proof" it's ever made and ever will make into profound doubt), or if it's recently been repeatedly blundering into it by sheer stupidity and that's how people noticed the bug at about the same time.

Theorem provers aren't magic, and have bugs just like all other programs. They are tools to help us double-check our reasoning. When you skip the reasoning and ask an AI to "prove" something for you that's over your head, you're entering an adversarial pact with the monkey-pawed Devil of Customer Satisfaction.

 

Great example of why using placeholders like xxx@deleteduser.com is a bad idea.

view more: next ›