MetaverseClub

wait, who opens the door?

Id prefer a privacy-care company over META, OAI, GOOG, etc.

misleading title!

BYD can single-hand crush US car makers for sooner or later.

>I'm shook. If you'd asked me this morning whether LLMs have native understanding of their weights that is less than human <-> neuron understanding, the same as human or more than human, I would have said "same to less" depending on definitions.

??? All LLM understands are their weights, dude, come on.

Sounds like if I'm smart enough and lucky enough I would have several Billions in my bank account.

The title is as stupid as Dario.

I think he looks like DAVID PATTERSON, the Turing award winner.

I wonder what are the use cases in their mind when designing this. For runtime assertions and documentations, yeah, it would work but it works without contract arguably ok.

For formal verification, the design is way off.

Please do not waste hardware (nowadays valuable) on Meta's privacy-leaking garbage.

Sam Assman needs money to buy a new super car or private jet?

I have no idea why people would ever want to touch anything from Meta.

Claude or ChatGPT for personal assistants? Big NONO.

Never ever trust OpenAI, they are evil.

"prominent names", lmao

At the end of the day, all the money Sam Assman used to lure people into doing crime will be paid for by all the 401k accounts of ordinary people.

My naive thoughts on Formal Verification (FV) and LLM:

We could leverage existing FV tools for a given programming language by using an LLM to generate a translator that maps the language to the FV tool's input format. This would essentially require a finite number of "abstract interpretation" functions—one for each language construct. While the total number of constructs might be large (e.g., around 500), each function would be independent. A function would only need to reason about the abstract semantics of a single construct, assuming the others adhere to their respective semantics. We could then distribute these LLM-generated functions among a group of experts (e.g., 100 reviewers). Thanks to the modularity of the functions, reviewers could evaluate their assigned subset in parallel without bottlenecks. The end result would be a working FV tool for the target language.