6 ms·

I think the interface of LLM with formalized languages is really the future. Because here you can formally verify every statement and deal with hallucinations.

raincole 2y ago
It's obviously not the future (outside of mathematics research). The whole LLM boom we've seen in the past two years comes from one single fact: peopel don't need to learn a new language to use it.
- seizethecheese 2y ago
  Both comments can be right. People don’t need to know HTML to use the internet.
- nickpsecurity 2y ago
  Natural language -> Formal Language with LLM-assisted tactics/functions -> traditional tools (eg provers/planners) -> expert-readable outputs -> layperson-readable results. I can imagine many uses for flows where LLM’s can implement the outer layers above.
Groxx 2y ago
The difficulty then will be figuring out if the proof is relevant to what you want, or simply a proof of 1=1 in disguise.
est 2y ago
> formalized languages is really the future Hmm, maybe it's time for symbolism to shine?
samweb3 2y ago
I am building Memelang (memelang.net) to help with this as well. I'd love your thoughts if you have a moment!
- thesz 2y ago
  You are building an SQL in disguise. First, you need to encode "memes" and relations between them at scale. This is not a language problem, it is data handling problem. Second, at some point of time you will need to query memes and relations between them, again, at scale. While expression of queries is a language problem, an implementation will heavily use what SQL engines does use. And you need to look at Cyc: https://en.wikipedia.org/wiki/Cyc https://en.wikipedia.org/wiki/Cyc It does what you are toing do for 40 (forty) years now.
  - jamilton 2y ago
    The PHP implementation works by converting it to SQL, so I'm sure they're aware.
- meindnoch 2y ago
  Looks like an incomplete Prolog.
- chvid 2y ago
  Maybe include a section titled 'how is this different from and how is it related to' ie. relational algebra?
nybsjytm 2y ago
If this were the case, I don't see why we'd need to wait for an AI company to make a breakthrough in math research. The key issue instead is how to encode 'real-life' statements in a formal language - which to me seems like a ludicrous problem, just complete magical thinking. For example, how might an arbitrary statement like "Scholars believe that professional competence of a teacher is a prerequisite for improving the quality of the educational process in preschools" be put in a lean-like language? What about "The theoretical basis of the October Revolution lay in a development of Marxism, but this development occurred through three successive rounds of theoretical debate"? Or have I totally misunderstood what people mean when they say that developments in automatic theorem proving will solve LLM's hallucination problem?
- nine_k 2y ago
  You can't talk about formally verifiable truthiness until you solve epistemology. This can be achieved formally in mathematics, with known principal limitations. Here strict theorem-proving, Lean-style, is viable. It can also be achieved informally and in a fragments way in barely-mathematical disciplines, like biology, linguistics, and even history. We have chains of logical conclusions that do not follow strictly, but with various probabilistic limitations, and under modal logic of sorts. Several contradictory chains follow under the different (modal) assumptions / hypotheses, and often both should be considered. This is where probabilistic models like LLMs could work together with formal logic tools and huge databases of facts and observations, being the proverbial astute reader. In some more relaxed semi-disciplines, like sociology, psychology, or philosophy, we have a hodgepodge of contradictory, poorly defined notions and hand-wavy reasoning (I don't speak about Wittgenstein here, but more about Freud, Foucault, Derrida, etc.) Here, I think, the current crop of LLMs is applicable most directly, with few augmentations. Still a much, much wider window of context might be required to make it actually productive, by the standards of the field.
  - nybsjytm 2y ago
    Hmmm I think even in something very nominally nearby like theoretical physics, there's very little that's similar to theorem proving. I don't see how AlphaProof could be a stepping stone to anything like what you're describing. Generally, I think many people who haven't studied mathematics don't realize how huge the gulf is between "being logical/reasonable" and applying mathematical logic as in a complicated proof. Neither is really of any help for the other. I think this is actually the orthodox position among mathematicians; it's mostly people who might have taken an undergraduate math class or two who might think of one as a gateway to the other. (However there are certainly some basic commonalities between the two. For example, the converse error is important to understand in both.)
aaron695 2y ago
[dead]
thesz 2y ago
So, you looking for Cyc [1], practically. [1] https://en.wikipedia.org/wiki/Cyc https://en.wikipedia.org/wiki/Cyc
- auggierose 2y ago
  Does Cyc have proofs?
  - cess11 2y ago
    In a sense, yes, since it has a foundation in Prolog style facts and rules, and supposedly can output its reasoning.
    - auggierose 2y ago
      Ok, sounds like in principle you could have proofs, but in practice, you don't? Are there any checks for the consistency of all facts?
      - cess11 2y ago
        How could there be? Gödel gets in the way.
        auggierose 2y ago
        In most interactive theorem provers the check is simple: you single out the axioms you believe, and all other stuff you do is guaranteed to preserve consistency. That works in an ITP system because there are only a few axioms. If Cyc has 100000 axioms/facts, then that's a problem.
        thesz 2y ago
        If axioms, facts and rules have types, these types can guide choice.
tucnak 2y ago
Grammar sampling has been around for months, and remained largely unexplored. Don't fall into the common trap of thinking in a fixed language, rather think about a superset of possible languages (grammars) and how they could evolve from one another. I bet, if there's a breakthrough, it's probably in "differential grammars," or whatever it would be called: plug that into the backtracking sampler, & you have your System 2.
gosub100 2y ago
Ok so Claude says that the Riemann hypothesis is proven and gives you 1200 pages of math symbols backing it up. Now what? You probably say "now a human can verify it" but what if the humans are wrong? What is the source of truth?
- Turneyboy 2y ago
  The nice thing about formal verification is exactly that. You have a separate tool that's very much like a compiler that can check those 1200 pages and tell you that it's true. The source of truth here is the code we wrote for the formal verification system.
  - gosub100 2y ago
    Could formal verification prove the nexus between the Taniyama-Shimura conjecture and Fermat's last theorem? I don't claim to know what the former is, but I am skeptical that a system that can only validate what we already know would have any luck with sudden leaps between disparate corners of the field. Or worse, what if we had this verification 30 years ago, Wiles gets excited thinking he proved a 300 year old mystery, only to be told by the algorithm, "sorry son, this code doesn't verify. Try again next time!"
    - falcor84 2y ago
      > "sorry son, this code doesn't verify. Try again next time!" But that's not how it works; rather it tells you about the specific issue with a particular step in the proof, which you then debug, as you would with code that isn't compiling (or not passing some static analysis test).

raincole 2y ago

It's obviously not the future (outside of mathematics research). The whole LLM boom we've seen in the past two years comes from one single fact: peopel don't need to learn a new language to use it.

seizethecheese 2y ago
Both comments can be right. People don’t need to know HTML to use the internet.
nickpsecurity 2y ago
Natural language -> Formal Language with LLM-assisted tactics/functions -> traditional tools (eg provers/planners) -> expert-readable outputs -> layperson-readable results. I can imagine many uses for flows where LLM’s can implement the outer layers above.

Groxx 2y ago

The difficulty then will be figuring out if the proof is relevant to what you want, or simply a proof of 1=1 in disguise.

est 2y ago

> formalized languages is really the future Hmm, maybe it's time for symbolism to shine?

samweb3 2y ago

I am building Memelang (memelang.net) to help with this as well. I'd love your thoughts if you have a moment!

thesz 2y ago
You are building an SQL in disguise. First, you need to encode "memes" and relations between them at scale. This is not a language problem, it is data handling problem. Second, at some point of time you will need to query memes and relations between them, again, at scale. While expression of queries is a language problem, an implementation will heavily use what SQL engines does use. And you need to look at Cyc: https://en.wikipedia.org/wiki/Cyc https://en.wikipedia.org/wiki/Cyc It does what you are toing do for 40 (forty) years now.
- jamilton 2y ago
  The PHP implementation works by converting it to SQL, so I'm sure they're aware.
meindnoch 2y ago
Looks like an incomplete Prolog.
chvid 2y ago
Maybe include a section titled 'how is this different from and how is it related to' ie. relational algebra?

nybsjytm 2y ago

If this were the case, I don't see why we'd need to wait for an AI company to make a breakthrough in math research. The key issue instead is how to encode 'real-life' statements in a formal language - which to me seems like a ludicrous problem, just complete magical thinking. For example, how might an arbitrary statement like "Scholars believe that professional competence of a teacher is a prerequisite for improving the quality of the educational process in preschools" be put in a lean-like language? What about "The theoretical basis of the October Revolution lay in a development of Marxism, but this development occurred through three successive rounds of theoretical debate"? Or have I totally misunderstood what people mean when they say that developments in automatic theorem proving will solve LLM's hallucination problem?

nine_k 2y ago
You can't talk about formally verifiable truthiness until you solve epistemology. This can be achieved formally in mathematics, with known principal limitations. Here strict theorem-proving, Lean-style, is viable. It can also be achieved informally and in a fragments way in barely-mathematical disciplines, like biology, linguistics, and even history. We have chains of logical conclusions that do not follow strictly, but with various probabilistic limitations, and under modal logic of sorts. Several contradictory chains follow under the different (modal) assumptions / hypotheses, and often both should be considered. This is where probabilistic models like LLMs could work together with formal logic tools and huge databases of facts and observations, being the proverbial astute reader. In some more relaxed semi-disciplines, like sociology, psychology, or philosophy, we have a hodgepodge of contradictory, poorly defined notions and hand-wavy reasoning (I don't speak about Wittgenstein here, but more about Freud, Foucault, Derrida, etc.) Here, I think, the current crop of LLMs is applicable most directly, with few augmentations. Still a much, much wider window of context might be required to make it actually productive, by the standards of the field.
- nybsjytm 2y ago
  Hmmm I think even in something very nominally nearby like theoretical physics, there's very little that's similar to theorem proving. I don't see how AlphaProof could be a stepping stone to anything like what you're describing. Generally, I think many people who haven't studied mathematics don't realize how huge the gulf is between "being logical/reasonable" and applying mathematical logic as in a complicated proof. Neither is really of any help for the other. I think this is actually the orthodox position among mathematicians; it's mostly people who might have taken an undergraduate math class or two who might think of one as a gateway to the other. (However there are certainly some basic commonalities between the two. For example, the converse error is important to understand in both.)

aaron695 2y ago

[dead]

thesz 2y ago

So, you looking for Cyc [1], practically. [1] https://en.wikipedia.org/wiki/Cyc https://en.wikipedia.org/wiki/Cyc

auggierose 2y ago
Does Cyc have proofs?
- cess11 2y ago
  In a sense, yes, since it has a foundation in Prolog style facts and rules, and supposedly can output its reasoning.
  - auggierose 2y ago
    Ok, sounds like in principle you could have proofs, but in practice, you don't? Are there any checks for the consistency of all facts?
    - cess11 2y ago
      How could there be? Gödel gets in the way.
      - auggierose 2y ago
        In most interactive theorem provers the check is simple: you single out the axioms you believe, and all other stuff you do is guaranteed to preserve consistency. That works in an ITP system because there are only a few axioms. If Cyc has 100000 axioms/facts, then that's a problem.
        thesz 2y ago
        If axioms, facts and rules have types, these types can guide choice.

tucnak 2y ago

Grammar sampling has been around for months, and remained largely unexplored. Don't fall into the common trap of thinking in a fixed language, rather think about a superset of possible languages (grammars) and how they could evolve from one another. I bet, if there's a breakthrough, it's probably in "differential grammars," or whatever it would be called: plug that into the backtracking sampler, & you have your System 2.

gosub100 2y ago

Ok so Claude says that the Riemann hypothesis is proven and gives you 1200 pages of math symbols backing it up. Now what? You probably say "now a human can verify it" but what if the humans are wrong? What is the source of truth?

Turneyboy 2y ago
The nice thing about formal verification is exactly that. You have a separate tool that's very much like a compiler that can check those 1200 pages and tell you that it's true. The source of truth here is the code we wrote for the formal verification system.
- gosub100 2y ago
  Could formal verification prove the nexus between the Taniyama-Shimura conjecture and Fermat's last theorem? I don't claim to know what the former is, but I am skeptical that a system that can only validate what we already know would have any luck with sudden leaps between disparate corners of the field. Or worse, what if we had this verification 30 years ago, Wiles gets excited thinking he proved a 300 year old mystery, only to be told by the algorithm, "sorry son, this code doesn't verify. Try again next time!"
  - falcor84 2y ago
    > "sorry son, this code doesn't verify. Try again next time!" But that's not how it works; rather it tells you about the specific issue with a particular step in the proof, which you then debug, as you would with code that isn't compiling (or not passing some static analysis test).