21–30 of 34 posts
Since LLMs are great at coding but bad at logic, maybe an approach like this can bridge the gap? So first let it translate natural language to a formal language, from there allow it to use a logic engine to make verifiable transformations (correctness-preserving), and finally translate back to natural language.
> Formal languages are basically laboratory-sized versions, or models, of natural languages. I can understand why a hundred years ago explaining what formal is (in the context of formal languages) could have been difficult. You had to say that it means something whose form can be manipulated without "understanding", or by rules that pertain to form rather than meaning. But since the late 1930s explaining what formal…
Undecidable languages are formal languages, too, even though there's no Turing machine that can accurately determine for any string whether it is part of the language or not. A formal language is a set of finite-length sequences (called "words") of symbols from another set (called the "alphabet"). It's essentially a very crude approximation of some strings of letters in an alphabetic writing system forming words in a…
While my explanation of "formal" is meant to be introductory and not entirely precise, that some problem tackled by an algorithm is undecidable does not mean that that problem isn't precisely interpretable by the computer. A Python interpreter doesn't terminate for all inputs (and therefore doesn't decide halting), yet it does interpret all of its inputs precisely.
> Formal languages are basically laboratory-sized versions, or models, of natural languages. I can understand why a hundred years ago explaining what formal is (in the context of formal languages) could have been difficult. You had to say that it means something whose form can be manipulated without "understanding", or by rules that pertain to form rather than meaning. But since the late 1930s explaining what formal…
Use of the word "mechanical" to describe formal reasoning predates computers. Here's the first sentence of Godel's 1931 On formally undecidable propositions... "The development of mathematics in the direction of greater exactness has—as is well known—led to large tracts of it becoming formalized, so that proofs can be carried out according to a few mechanical rules." Leibniz had discussed calculating machines (and ev…
Leibniz spoke of "automatons" and dreamt of some sort of "thoughtless" reasoning, but I don't know if he had the right building blocks to even think of mechanisation as we could since the 19th century. E.g. here's how Leibniz tries to justify the utility of formal reasoning: "Our thoughts are for the most part what I call ‘blind thoughts’. I mean that they are empty of perception and sensibility, and consist in the wholly unaided use of symbols... We often reason in words, with the object itself virtually absent from our mind."
So he definitely had the right concept - which is why formal logic is so old - but not the right language that most people would intuitively understand today.
Since LLMs are great at coding but bad at logic, maybe an approach like this can bridge the gap? So first let it translate natural language to a formal language, from there allow it to use a logic engine to make verifiable transformations (correctness-preserving), and finally translate back to natural language.
People are already using Prolog for this; 1) A series of excellent and detailed blog posts by Eugene Asahara Prolog in the LLM Era - https://eugeneasahara.com/category/prolog-in-the-llm-era/ 2) Previous HN discussion Use Prolog to improve LLM's reasoning - https://news.ycombinator.com/item?id=41831735 3) User "bytebach" gives a nice example of using Prolog as an intermediate DSL in the prompt to an LLM so as to trans…
Prolog is quite popular and successful as a target for LLMs. And it's no accident considering Prolog was introduced to represent natural language statements in (predicate) logic.
Earlier quoted context omitted.
I've been strapping different LLM based setups to Lean 4 with a variety of different prompting methods. My biggest conclusion here is that LLMs are worse at formalizing than humans are. Additionally, for Lean 4 specifically, I don't think there's enough training data.
Yeah, we really need LLMs to work swimmingly with Lean 4. It is currently hot garbage and it does not understand proof composition, exploring proof extensions, lemma search, etc. It does not explore an open-ended node to a mathematical knowledge graph by substituting various options. I'd happily work with someone on a conversational theorem prover, if anyone's up for it.
Earlier quoted context omitted.
Use of the word "mechanical" to describe formal reasoning predates computers. Here's the first sentence of Godel's 1931 On formally undecidable propositions... "The development of mathematics in the direction of greater exactness has—as is well known—led to large tracts of it becoming formalized, so that proofs can be carried out according to a few mechanical rules." Leibniz had discussed calculating machines (and ev…
Yes, by Godel's time the notion of "calculability" was already at least intuitively grasped, and it was then that "formal" was understood to mean mechanical. Turing made the connection rigorous. Leibniz spoke of "automatons" and dreamt of some sort of "thoughtless" reasoning, but I don't know if he had the right building blocks to even think of mechanisation as we could since the 19th century. E.g. here's how Leibniz…
This is great reading and a great supplement to my limited education in math, comp sci, and formal logic.
This is great reading and a great supplement to my limited education in math, comp sci, and formal logic.
You should check out Math Academy. It'll give you as much math background as any engineering student and they aim to provide the equivalent of a full undergrad math degree in the next few years.
> Formal languages are basically laboratory-sized versions, or models, of natural languages. I can understand why a hundred years ago explaining what formal is (in the context of formal languages) could have been difficult. You had to say that it means something whose form can be manipulated without "understanding", or by rules that pertain to form rather than meaning. But since the late 1930s explaining what formal…
Earlier quoted context omitted.
Undecidable languages are formal languages, too, even though there's no Turing machine that can accurately determine for any string whether it is part of the language or not. A formal language is a set of finite-length sequences (called "words") of symbols from another set (called the "alphabet"). It's essentially a very crude approximation of some strings of letters in an alphabetic writing system forming words in a…
You're talking about formal languages in the context of computer science. Formal languages in the context of logic predate computer science (or could be said to be a direct precursor to computer science). These logic languages are also trivially decidable in the computer-science sense of formal languages, i.e. their set of strings is easily decidable. When we talk of decidability in those languages we ususally mean t…
If you accept some axiomatic assumptions about infinite sets (that are common in mathematics; I'm not sure exactly what the weakest required axiom is for this), then you can even believe that there are infinite languages that have no finite description at all, very much akin to the commonplace claim that there are real numbers that have no finite description at all. There are formulations of mathematics in which this is not true, but most mathematicians seemingly work in formulations in which it is true.
I even expect that we can probably prove this directly using the powerset operation and diagonalization, which doesn't require particularly strong assumptions about infinities.