All of Sven Nilsen's Comments + Replies

I think that most people imagine themselves as gatekeepers for controlling the world, when in reality the world is controlled by systems we don't fully understand. For example, I don't think people really know what "money" means in the real world. You can imagine yourself as a person who knows it, but can you verify that your understanding matches reality?

If we want to have a chance to control the future to some degree, then it means that humans need to take over the world. It is not sufficient to stop AGI from taking over the world, but we also need to ensure that the future of the world is aligned with human values. For now, it seems that stuff like "money" is running the show.

Obviously, problems are not exclusive! I find it easier to imagine a civilization that has survived for a long time and made significant technological progress: How would a such civilization approach ASI? I think they will analyze the problem to death and use automated theorem proving as much as possible and having a culture where only a tiny amount of ideas ever get implemented, even if most of those ideas never implemented would seem very good to us. In short: Higher standards for safety.

One challenge with the "people will use it for bad stuff"-situation... (read more)

It is also worth thinking if you put in context that people said "no, obviously, humans would not let it out of the box". Their confident arguments persuaded smart people into thinking that this was not a problem.

You also have the camp "no, the problem will not be people telling the AI do bad stuff, but about this hard theoretical problem we have to spend years doing research on in order to save humanity" versus "we worry that people will use it for bad things" which in hindsight is the first problem that occurred, while alignment research either comes too... (read more)

3Seth Herd8mo
Yes; but I think that conclusion is based on a logical fallacy that we can only worry about one of those problems. Both are real. This helps with alignment but doesn't solve it, particularly outer alignment and alignment stability. It definitely increases the practical problem of malicious use of aligned AGI.

The error margin LeCun used is for independent probabilities, while in an LLM the paths that the output takes become strongly dependent on each other to stay consistent within a path. Once an LLM masters grammar and use of language, it stays consistent within the path. However, you get the same problem, but now repeated on a larger scale.

Think about it as tiling the plane using a building block which you use to create larger building blocks. The larger building block has similar properties but at a larger scale, so errors propagate, but slower.

If you use i... (read more)

The error margin is larger than it appears as estimated from tokens, due to combinatorial complexity. There are many paths that the output can take and still produce an acceptable answer, but an LLM needs to stay consistent depending on which path is chosen. The next level is to combine paths consistently, such that the dependence of one path on another is correctly learned. This means you get a latent space where the LLM learns the representation of the world using paths and paths between paths. With other words, it learns the topology of the world and is able to map this topology onto different spaces, which appear as conversations with humans.

I'm not sure I understand correctly: you are saying that it's easier for the LLM to stay coherent in the relevant sense than it looks from LeCun's argument, right?

I up-voted your post because I think this is a useful discussion to have, although I am not inclined to use the same argument and my position is more conditional. I learned this lesson from the time I played with GPT-3, which seemed to me as a safe pathway toward AGI, but I failed to anticipate how all the guardrails to scale back deployment were overrun by other concerns, such as profits. It is like taking a safe pathway and incrementally make it more dangerous over time. In the future, I expect something similar to happen to GPT-4, e.g. people develop ha... (read more)

I saw somebody on twitter suggesting "LessBad" to match "LessWrong".

2Steven Byrnes5mo
Funny thing: the intention of "LessWrong" is "less wrong than I was before" but I have heard people take it to mean "less wrong than everyone else is". (LessBad obviously has the same problem.)

If ChatGPT is asked questions like "should we put in safeguards in the development of self-improving AIs" then is it likely to answer "yes". Now, if ChatGPT was given political power, it becomes a policy that world leaders need to solve. Do we need constraints on GPU computing clusters? Maybe ChatGPT answers "STOP", because it thinks the question is too complex to answer directly. It is always more difficult to decide on what actions to do in order to implement general policies, than agreeing about the overall policy. However, if we can align our overall p... (read more)

Maybe you can talk to Eric Weiser, who kindly provided me a proof in Lean 3:

The experts in dependent types I know, think Path Semantics might help provide a better foundation or understanding in the future, or perhaps languages with some new features. We don't know yet, because it takes a lot of work to get there. I don't have the impression that they are thinking about Path Semantics, since there is already a lot to do in ... (read more)

OK, that thread is from last year, before HOOO EP was completed. HOOO EP is now completed.

You should not be confused by the term "Path Semantics", as this is the name of my project. The foundational level of Path Semantics is a set of logical languages consisting of IPL, HOOO EP, PSQ and PSI.

Of course HOOO EP is a made up term. I am the person who invented it. However, the Prop library contains stuff about IPL, which is not something I invented. You don't have to understand HOOO EP to trust that IPL is previous work, as it is well established field. Consid... (read more)

One of us seems to be deeply confused about what math is, because I strongly believe that Gödel's Incompleteness Theorem is not about sexuality or castration. From my perspective, this is some alt-math; a postmodern misinterpretation of how math is actually used (hint: not to make complicated metaphors about penises). If this is actually popular in some branches of academia (which sadly doesn't sound unlikely), may gods have mercy on us. Someone who self-publishes on Academia edu (writing about topics such as: "Nine Men’s Morris Game as Structural Analogy for the Western Worldview", "Did Schelling Discover the Higher Logical Types of Being?", "Foundational Mathematical Categories and Passive Syntheses in Anti-Oedipus", "Exploring the Tetractys and what is Beyond at the level of the Site/Event and the Holon within the structure of the Emergent Event") is the endorsement for your mathematical theories? Sorry, I previously wasn't specific, but when I asked for "a scientific paper written by someone else, referring to your paper or to your program", I assumed someone who does math, or computer science. Not a self-publishing philosopher who uses math as a metaphor for sexuality. Because I want to know whether your writing makes sense mathematically, and don't really care whether it can or cannot be used as convenient postmodern metaphor. Could we agree that "math as known to and used by mathematicians" and "math as known to and used by postmodern philosophers" are simply two different things? And while your contributions may be novel and valuable for the latter, this website is about the former. Thus the confusion.

Path semantics is built upon previous works, e.g. Homotopy Type Theory:

This kind of previous work is cited all of the place. I have no idea why you think there is no preexisting discussion going on.

Yes, all you needed was simply to ask:

Here is a theory based on the work of 3 people in collaboration:

I can give you more examples.

Let's say you don't trust the Pocket-Prover library. Yet, this library is a brute force theorem prover that no person so far has reported bugs. I understand you won't trust it without further investigation, but there are no other people who have reasonable doubt about it. Where ... (read more)

No one is blocking you from discussion. The reason why you get so few responses is (my best guess) because no one here understands what you are talking about. To put it bluntly, I am trying to figure out whether you are a crackpot. So far, your defense seems unimpressive to me. What you do is supposed to be math, but it does not resemble the math as I know it. Words like "path semantic", "semantical qubit", "joker calculus", "Seshatism", "HOOO EP", it all seems completely made up. The only person on the internet who uses these words is you. The paper that refers to you, is summarized as "Explorations of the relations between Inside Theories and Outside Theories of Sven Nilsen in relation to Sexuation of Lacan, the Antimonies of Kant and the deconstructive equations of Derrida as taken up by Zizek." That sounds to me like something written in a parallel universe, where math is considered a sub-discipline of literary criticism. Your most quoted sources are yourself, and Wikipedia. It's not just me who is confused. Looking at r/rust, where you posted about your library, the reactions are: "I can’t even remotely parse this.", "Bro I have no idea.", "im so confused", "The document you linked is not published in any scientific journal and hasn't been peer reviewed. Scientifically, it is the equivalent of a blog post.", "It is literally a chain of thoughts, linking together completely unrelated concepts from a wide variety of fields without explaining it." ...actually, now I see that whatever I tried to tell you, someone else already did. Anyone else who wants to join this debate, please read that Reddit thread first.

I assume you can assume for yourself that what I write is nonsense, but this does not prove that I am writing nonsense. Claiming that my work is generated by GPT is false, when it isn't.

That's not how logic works. If no evidence I provide can convince you otherwise, then your condition for changing your mind is predicated on that the agent proving you evidence is not me. This is not acceptable for me, because if I give you link to somebody who uses my work or a computer program that uses my theory, then you will not accept it as a reason to investigate further.

You didn't make a claim that some of my work is wrong, you made the claim that the ENTIRE thing is wrong, which is a gaslighting argument.

1Walker Vargas8mo
No, if you are contributing to a preexisting discussion, there should be some older work you can cite. For example, you learned about the theory of path semantics from something that wasn't written by you. Cite that source.
Eh, I am quite aware of the chance that I am just making an idiot out of myself. Yet I felt that this was a question someone should ask, because... well, you know the story about the Emperor's new clothes. If I am wrong here, I am really sorry. However, please consider the evidence I have, from my perspective. What conclusion would you make out of it in my place? * you talk about something no one else does, on the entire part of internet indexed by Google; * yet you talk about it as if it's something people are supposed to know; * googling for "Leibniz' first principle" is similarly fruitless (okay, you added it to the article, but the weird thing is using a phrase no one else on the entire internet does, and assuming it standard); * this is a website with many people highly knowledgeable about math and logic, yet none of them started a dialog (whether agreement or disagreement) with you; * I happen to have some decent-but-not-exceptional background in math myself, and nothing on the Wikipedia page about first-order logic seems related to what you wrote here. I emphasize that it is not the last bullet point alone, but all five of them together, that made me write this. What conclusion would you have made in my place? What is your explanation for why no one else seems to talk about "path semantic" and "semantical qubit" on the internet? If the computer program that uses your theory was also written by you, that indeed would not convince me. On the other hand, a scientific paper written by someone else, referring to your paper or to your program, that could make me change my mind, if you could link it.

I'll give short introduction here to some of the background in constructive logic required to provide constructive criticism, as I saw one person here using a gaslighting argument:

Constructive logic is a weaker logic than classical logic, in which a statement A => B is modeled as a lambda expression in simple type theory. Propositional equality is A == B, consisting of two maps A => B and B => A. The reason A == B is technically an assumed position in logic, is that lambda expressions can capture variables from their environment. It means, A == B ... (read more)

Author here. This is based on research from implemented theorem proving. See the links in the post.

I apologize, but the links all go to pages written by you, so I don't count it as independent confirmation. Wikipedia has nothing on "path semantics". Google mostly returns things written by you; plus one paper with this title, but its content seems unrelated, so perhaps it is a coincidence. So, from my perspective, it just seems like something you made up. That is not necessarily a bad thing, you may have invented something useful, I have no idea. Some kind of peer review would be nice. Unfortunately, your posts here did not start a technical discussion. At this moment, my working hypothesis is that no one here understands this, but most people assume that someone else does.

Thank you! Post updated to include the definition.

The use of Chu spaces is very interesting. This is also a great introduction to Chu spaces.

I was able to formalize the example in the research automated theorem prover Avalog:

It is still very basic, but shows potential. Perhaps Avalog might be used to check some proofs about Cartesian frames.