badrunaway

we are talking about lean proofs. Given a formal statement and a proof - the lean can verify whether it's correct or not. It's like generating computer programs to solve a problem - the problem lied in generating useful solutions/sub-solutions so that the search is effective. They achieve this via using gemini as a lean proof generator aka. using a world model LLM fine tuned to generate lean proofs in a more effective manner.

Humans are even better at this as you mention - but effectively the approach is similar. Come up with lot of ideas and see what proves it.

I think what we need to look at is that AI systems were not able to do it before and now they are able to do it. Sooner these systems with millions of dollars of compute will just scale the algorithms and beat humans at this as well - just like they did for chess, go, shogi etc.

This will in a few months change everything forever. Exponential growth incoming soon from Deepmind systems.

I guess I need to tell them to not even send any personal detail / bank detail to anyone including me. I sort of felt like may be there is a better solution than just trusting them to follow this. Like we have insurance for death kind of scenarios and medical insurance.. some sort of systematic protection would have been better.

That's also a fear I have. But having grown up on internet it helps in adjusting to these changes fast. Secondly, I got a degree in CS and been a developer for a decade so yeah I know a video can be a deepfake instinctively. It's harder to scam us than a generation who retired already when deepfake/deepvoicecloning arrived and may be never had a CS exposure.

So, my reasoning is little stupid but it goes like this. I am in my 30s. Let's say if I lose all my money in a scam also - I have time to earn it back and still make it back. Whereas our elders (parents are 60+) who have savings and rely on their savings and can't really earn now - and also have lot of medical bills to pay with their age ==== for them it's like one-shot ending right? That's why I considered them as special case.

Recently someone I know got a call where they mimicked their child's voice using AI and asked them to send immediate money otherwise child will be in danger. This has got me into thinking - my parents would also do the same for me/ and everyone's would-- add deepfake into it -- how the fuck we are support to assume people won't give emotional response? forget about personal details, people who care about you can might directly do a transfer.

LLMs right now don't employ any logic. There can always be corners of "I don't know" or "I can't do that" - than the current system which is 100% confident in it's answer because it's not actually trying to match any constraint at all. So at some point the system will apply logic but may not be as formal as we do in pure math.

Yes, that's why there was no human in the loop and I was using LLMs as a proxy to bottom up approach in step 1. But the hallucinations can creep into the knowledge graph also as mentioned by another commentator

I thought addition of the "logical" constraints in the existing training loop using KGs and logical validation would help into reducing wrong semantic formation at the training loop itself. But your point is right that what if the whole knowledge graph is hallucinated during the training itself.

I don't have answer to that. I felt there would be lesser KG representations which would fit a logical world, than what fits into the current vast vector spaces of network's weight and biases. But that's just a idea. This whole thing stems from this internal intuition that language is secondary to my thought process and internally I feel I can just play around concepts without language - what kind of Large X models will meet that kind of capability I don't know!

Oh, exactly. But let me know your thoughts on this - let's say if you have a graph which represents existing sci-fi novel = rather than the current model which is just blindly generating text on statistical probabilities would it not help to have to model output also try to fit into this rather imperfect sci-fi novel KG? If it doesn't fit logically. Based on how strong your logic requirements are system can be least creative to most creative etc.

I was not actually aware that building KG from text is NP-hard problem. I will check it out. I thought it was a time consuming problem when done manually without LLMs but didn't thought it was THAT hard. Hence I was trying to introduce LLM into the flow. Thanks, will read about all this more!

Haha, asking chat-gpt surely won't work. Everything can "feel" like a halting problem if you want perfect results with zero error with uncertain and ambiguous new data adding.

My take - Hallucinations can never be made to perfect zero but they can be reduced to a point where these systems in 99.99% will be hallucinating less than humans and more often than not their divergences will turn out to be creative thought experiments (which I term as healthy imagination). If it hallucinates less than a top human do - I say we win :)

I had KGs in mind with automated construction which can improve and converge during training phase. I was hypothesizing that if we give incentive during training phase to also construct KGs and bootstrap the initial KGs from existing LLMs - the convergence towards a semantically correct KG extension during inference can be achieved. What do you think?

Interesting. I haven't really seen much into this space. But anything which can provably represent concepts and relationships without losing information can work. Devil might be in details; nothing is as simple as it looks on first sight.

Current architecture of LLMs focus mainly on the retrieval part and the weights learned are just converged to get best outcome for next token prediction. Whereas, ability to put this data into a logical system should also have been a training goal IMO. Next token prediction + Formal Verification of knowledge during training phase itself = that would give LLM ability to keep consistency in it's knowledge generation and see the right hallucinations (which I like to call imagination)

The process can look like-

1. Use existing large models to convert the same previous dataset they were trained on into formal logical relationships. Let them generate multiple solutions

2. Take this enriched dataset and train a new LLM which not only outputs next token but also a the formal relationships between previous knowledge and the new generated text

3. Network can optimize weights until the generated formal code get high accuracy on proof checker along with the token generation accuracy function

In my own mind I feel language is secondary - it's not the base of my intelligence. Base seems more like a dreamy simulation where things are consistent with each other and language is just what i use to describe it.

Got it. 'Finding Fun' is one good metric.

I have actually a lot of free time and I want to build things that people love.

yea - but that won't satisfy me. Upvote is sort of one metric on how much novel your work is? something like that.

I believe language allows having more than one layer i.e. enabling complexity of representation. For example, If I want to think about the person thinking inside - these kind of recursive concepts need some sort of symbolic nesting to even materialise the idea.

Intuitively I feel efficiency is the outcome of existing world model.. approach can look like yours - I don't see why there has not been efforts on scaling monte carlo tree search for extending the existing world model via tree search. My guess is that it would diverge to hallucinations too fast because it doesn't have a strong logical building block already

like darwin selection between the subsystem approaches? Put in a lot of different kind of LLMs and let them play the same game inside with each other.. whosoever wins the simulation is allowed to externally present the approach... something like that?

When we talk about system 2; is it possible that [generating large number of programs; evaluating them of the task; choosing top K outcomes; feeding it back to Neural net] can act as system 2 for a AGI? Isn't that how we think intelligently as well- by making lot of hypothesis internally and evaluating them - and updating our model?

Can someone summarise what this changes overall in the field? What I got is that there was no proper formalism to study emergence earlier and now we have a mathematical framework.

Oh, that one I have added in code manually (500ms). Some random delay to make it sound pleasing. Thank you.

I believe there should be a clear indicator in UI of every OS when any new program listens to your keystrokes.. it should be the norm

nobody ported python to wasm yet?

A cleaner API you mean which exposes what is necessary only.

what can be done to stop all this? We need some sort of OS level layer to validate these things. If we put a local LLM which checks the bytecode of things which are getting installed/running for security = will that solve all this? My heart goes out to those who must have lost their money due to this.

hey, I tried it on chrome on my iphone but was not able to reproduce. May I know which lag are you pointing to- 1. Website loading lag 2. First keypress sound 3. The subsequent sound after keypress Sorry, for the bad experience.

So much fun! I am so inspired to build!

Manim I have tried once. While it's cool - it feels designed for a specific use case. I will check out canvas API!