Egregoros

Signal feed

API Docs
Timeline

Post

Remote status

Context

9
Q.U.I.N.N.

Q.U.I.N.N.

@icedquinn@blob.cat remote
Open link
@sun :neocat_sweat: i barely know what i'm doing with this shit half the time. i mostly talk to an LLM about it these days and it stares at me in response.

something particularly weird is how structurally neuromorphic these things are. they get there through funny routes (explicit RNG deciding when to not update = heterogenous neurons)

the fuzzy machine already makes clauses do graded activation so its straightforward enough to group them up and do winner-take-all lateral inhibition, the question is just if that pooler is useful for anything :blobcatwaitwhat:

the bizzare thing is its theoretically possible to do some kind of hopfield memory / autoregressor thing -> decider -> loop without an FPU anywhere in sight.

its a comically cheap substrate that just needs to be puzzled out in the correct order to do something smart. hm.
Q.U.I.N.N.

Q.U.I.N.N.

@icedquinn@blob.cat remote
Open link
@sun i haven't seen it, no. i've been adjacent to the proof space recently though. Maude is used for defense verification. (though i'm trying to use maude for codegen, which ran in to some stupid errors.)

there is a controversy right now, though, because openai is flooding math papers with bad proofs.
Q.U.I.N.N.

Q.U.I.N.N.

@icedquinn@blob.cat remote
Open link
@sun i think i've poke claude (but not GLM as much) about it. Lean upstream uses LLMs for proofs, but its safe to do this. they write the term to be proven by hand and let the LLM close it. so the LLM never controls the end goal and the kernel validates intermediate steps are valid.

it is less safe if the LLM is writing the goal because you can--even with dependent types--make a spec that is ass trash and worthless.
Replying to @icedquinn@blob.cat

Replies

0
No replies yet.