7 ms·

Formal Reasoning [pdf]

146 points by Thom2503 11mo ago

amelius 11mo ago
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.
- 3abiton 11mo ago
  Essentially there is growing interest in the "formal" math community (combinatorics, mining, etc ..) to do exactly this.
- rramadass 11mo ago
  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/ 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 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 transform English declarative -> Imperative code - https://news.ycombinator.com/item?id=41549823 https://news.ycombinator.com/item?id=41549823
  - pjmlp 11mo ago
    As big Prolog fan, thanks for sharing those resources.
  - tannhaeuser 11mo ago
    There's also [1], containing further bibliography references along with practical applications in discrete planning. 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. [1]: https://quantumprolog.sgml.net/llm-demo/part1.html https://quantumprolog.sgml.net/llm-demo/part1.html
    - rramadass 11mo ago
      That is pretty neat!
- swagmoney1606 11mo ago
  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.
  - proof_by_vibes 11mo ago
    I'm of the opinion that formalization is the biggest bottleneck of current generation LLMs. However, I don't think that this necessarily suggests that LLMs don't benefit from formal methods. Given existing abstractions, Lean4's exceptional tooling allows for more efficient iteration with LLMs and requires less human supervision since Lean's language server provides specific and actionable feedback whenever the LLM makes a mistake. I've also noticed that LLMs can reason about code written in Lean4 far more effectively than in Python, despite Python having orders of magnitude more training data than Lean. Nonetheless, I concur that LLMs don't yet know how to translate a request stated in a prompt to a complete Lean4 interpretation. My practice so far has usually required me to first choose an existing reference file that is similar to my desired goals, and use this reference as "inspiration" for how the LLM should go about formalization.
  - numpy-thagoras 11mo ago
    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.
    - ajs1998 11mo ago
      Join the Lean Zulip. There are many people interested in this. https://leanprover.zulipchat.com/ https://leanprover.zulipchat.com/
- lou1306 11mo ago
  I think a big issue with this approach is that the initial and last steps are prone to sycophancy: the machine wants you to believe it's getting the job done, which may lead it to do something correct-looking over something correct. The middle steps (correct-by-construction transformations) do not need an LLM at all. It's what a certified compiler does. I think the way forward, for the immediate future, is to feed AI agents with a mixture of (hand-written) natural language and formal blueprints, then use as many mechanized analysis methods as possible on the generated code (from unit/regression testing to static analysis, and possibly more powerful software verification procedures). Potentially feed the output of these analyses back to the agents.
- zozbot234 11mo ago
  > 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. Linguists in the Richard Montague tradition have indeed attempted to use tools like formal logic, lambda calculus, continuations, monads, modalities etc. to try and understand the semantics of natural language in a way that's both logical/formal and compositional - i.e. accounting at least partially for the "deep" syntax of natural language itself, such that a fragment can be said to have a semantics of its own and the global semantics of a broader construction arises from "composing" these narrower semantics in a reasonably straightforward way. This is pretty much the same as trying to take the "let's translate natural language into formal logic" proof-of-concept exercises from a text like OP (or from your average logic textbook) seriously and extending them to natural language as a whole. It turns out that this is really, really hard, because natural language mixes multiple "modalities" together in what looks like a very ad-hoc way. We only barely have the tools in formal logic to try and replicate this, such as continuations, modalities and monads. (Linguists actually talk about many phenomena of this kind, talking about "modalities" is just one example that's both general enough to give a broad idea and happens to be straightforward enough on the logical side. You have quantification, intensionality, anaphora, scope, presupposition, modality proper, discourse-level inference, pragmatics, ellipsis, indexicals, speech acts, etc. etc. etc.) And because the semantics of natural language is both so general and so hard to pin down, it doesn't seem useful to "reason" about the logical semantics of natural languages so directly. You can of course use logical/mathematical modeling to address all sorts of problems, but this doesn't occur via a verbatim "translation" from some specific language utterance.
- wisnesky 11mo ago
  That's the approach we're taking to verify LLM-generated SQL code at http://sql.ai http://sql.ai.
stephenlf 11mo ago
This is great reading and a great supplement to my limited education in math, comp sci, and formal logic.
- sn9 11mo ago
  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.
  - MarcelOlsz 11mo ago
    I've also had a lot of success with the Art Of Problem Solving text-books, the regular ones not the competition ones. As someone who's starting from the ground up with arithmetic.
    - sn9 11mo ago
      Yeah they're great too! I think of Math Academy as ideal for efficiently mastering subjects at a level slightly deeper than a typical education in a shorter amount of time, and AoPS is for taking your time to go much deeper into the topics. Doing them both is probably best, but doing one or the other would still work.
      - MarcelOlsz 11mo ago
        >I think of Math Academy as ideal for efficiently mastering subjects at a level slightly deeper than a typical education in a shorter amount of time, and AoPS is for taking your time to go much deeper into the topics. I've been searching hi and lo for the ultimate beginner resource and nothing comes close to AoPS for the exact reason you mentioned. I started with principia mathematica by bertrand russel because I thought math worked like a big tree all stemming from one trunk. Boy was that a bad move lol. I'd be reading some textbook and I have an infinite amount of why's that would block me on the most basic of things, tons of assumed knowledge. AoPS treats you like a caveman who first discovered fire, and then discovered their books, in that order. I'll give MathAcademy a go too, I heard lots of great things.
pron 11mo ago
> 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 means has become much simpler: it means mechanical. A formal language is one that can be precisely and accurately interpreted and manipulated by a machine. When we talk about "formal proofs" we don't mean precise proofs, official proofs, or proofs written by a mathematician. We mean proofs written in a language, and following a procedure, that can be mechanically checked (and by a fairly basic algorithm). While it is still a little colloquial, these days we can say that formal languages are those languages that can always be correctly interpreted by a computer. I think this captures the meaning of "formal" much more than saying these are "models of natural language".
- griffzhowl 11mo ago
  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 even thought about binary arithmetic being the most appropriate implementation), so the general idea probably goes back quite far Edit: Oh, I guess by "late 1930s" you're referring to Turing's 1936 paper where he defines Turing machines, rather than actual electronic computers. Still, understanding "formal" as "mechanical" predates it.
  - DougBTX 11mo ago
    Perhaps it has to be that way, the motivation to build a mechanical computer is based on the belief that computation can be mechanised.
    - DonaldPShimoda 11mo ago
tug2024 11mo ago
[dead]

146 points by Thom2503 11mo ago

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.

3abiton 11mo ago
Essentially there is growing interest in the "formal" math community (combinatorics, mining, etc ..) to do exactly this.
rramadass 11mo ago
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/ 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 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 transform English declarative -> Imperative code - https://news.ycombinator.com/item?id=41549823 https://news.ycombinator.com/item?id=41549823
- pjmlp 11mo ago
  As big Prolog fan, thanks for sharing those resources.
- tannhaeuser 11mo ago
  There's also [1], containing further bibliography references along with practical applications in discrete planning. 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. [1]: https://quantumprolog.sgml.net/llm-demo/part1.html https://quantumprolog.sgml.net/llm-demo/part1.html
  - rramadass 11mo ago
    That is pretty neat!
swagmoney1606 11mo ago
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.
- proof_by_vibes 11mo ago
  I'm of the opinion that formalization is the biggest bottleneck of current generation LLMs. However, I don't think that this necessarily suggests that LLMs don't benefit from formal methods. Given existing abstractions, Lean4's exceptional tooling allows for more efficient iteration with LLMs and requires less human supervision since Lean's language server provides specific and actionable feedback whenever the LLM makes a mistake. I've also noticed that LLMs can reason about code written in Lean4 far more effectively than in Python, despite Python having orders of magnitude more training data than Lean. Nonetheless, I concur that LLMs don't yet know how to translate a request stated in a prompt to a complete Lean4 interpretation. My practice so far has usually required me to first choose an existing reference file that is similar to my desired goals, and use this reference as "inspiration" for how the LLM should go about formalization.
- numpy-thagoras 11mo ago
  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.
  - ajs1998 11mo ago
    Join the Lean Zulip. There are many people interested in this. https://leanprover.zulipchat.com/ https://leanprover.zulipchat.com/
lou1306 11mo ago
I think a big issue with this approach is that the initial and last steps are prone to sycophancy: the machine wants you to believe it's getting the job done, which may lead it to do something correct-looking over something correct. The middle steps (correct-by-construction transformations) do not need an LLM at all. It's what a certified compiler does. I think the way forward, for the immediate future, is to feed AI agents with a mixture of (hand-written) natural language and formal blueprints, then use as many mechanized analysis methods as possible on the generated code (from unit/regression testing to static analysis, and possibly more powerful software verification procedures). Potentially feed the output of these analyses back to the agents.
zozbot234 11mo ago
> 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. Linguists in the Richard Montague tradition have indeed attempted to use tools like formal logic, lambda calculus, continuations, monads, modalities etc. to try and understand the semantics of natural language in a way that's both logical/formal and compositional - i.e. accounting at least partially for the "deep" syntax of natural language itself, such that a fragment can be said to have a semantics of its own and the global semantics of a broader construction arises from "composing" these narrower semantics in a reasonably straightforward way. This is pretty much the same as trying to take the "let's translate natural language into formal logic" proof-of-concept exercises from a text like OP (or from your average logic textbook) seriously and extending them to natural language as a whole. It turns out that this is really, really hard, because natural language mixes multiple "modalities" together in what looks like a very ad-hoc way. We only barely have the tools in formal logic to try and replicate this, such as continuations, modalities and monads. (Linguists actually talk about many phenomena of this kind, talking about "modalities" is just one example that's both general enough to give a broad idea and happens to be straightforward enough on the logical side. You have quantification, intensionality, anaphora, scope, presupposition, modality proper, discourse-level inference, pragmatics, ellipsis, indexicals, speech acts, etc. etc. etc.) And because the semantics of natural language is both so general and so hard to pin down, it doesn't seem useful to "reason" about the logical semantics of natural languages so directly. You can of course use logical/mathematical modeling to address all sorts of problems, but this doesn't occur via a verbatim "translation" from some specific language utterance.
wisnesky 11mo ago
That's the approach we're taking to verify LLM-generated SQL code at http://sql.ai http://sql.ai.

stephenlf 11mo ago

This is great reading and a great supplement to my limited education in math, comp sci, and formal logic.

sn9 11mo ago
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.
- MarcelOlsz 11mo ago
  I've also had a lot of success with the Art Of Problem Solving text-books, the regular ones not the competition ones. As someone who's starting from the ground up with arithmetic.
  - sn9 11mo ago
    Yeah they're great too! I think of Math Academy as ideal for efficiently mastering subjects at a level slightly deeper than a typical education in a shorter amount of time, and AoPS is for taking your time to go much deeper into the topics. Doing them both is probably best, but doing one or the other would still work.
    - MarcelOlsz 11mo ago
      >I think of Math Academy as ideal for efficiently mastering subjects at a level slightly deeper than a typical education in a shorter amount of time, and AoPS is for taking your time to go much deeper into the topics. I've been searching hi and lo for the ultimate beginner resource and nothing comes close to AoPS for the exact reason you mentioned. I started with principia mathematica by bertrand russel because I thought math worked like a big tree all stemming from one trunk. Boy was that a bad move lol. I'd be reading some textbook and I have an infinite amount of why's that would block me on the most basic of things, tons of assumed knowledge. AoPS treats you like a caveman who first discovered fire, and then discovered their books, in that order. I'll give MathAcademy a go too, I heard lots of great things.

pron 11mo ago

> 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 means has become much simpler: it means mechanical. A formal language is one that can be precisely and accurately interpreted and manipulated by a machine. When we talk about "formal proofs" we don't mean precise proofs, official proofs, or proofs written by a mathematician. We mean proofs written in a language, and following a procedure, that can be mechanically checked (and by a fairly basic algorithm). While it is still a little colloquial, these days we can say that formal languages are those languages that can always be correctly interpreted by a computer. I think this captures the meaning of "formal" much more than saying these are "models of natural language".

griffzhowl 11mo ago
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 even thought about binary arithmetic being the most appropriate implementation), so the general idea probably goes back quite far Edit: Oh, I guess by "late 1930s" you're referring to Turing's 1936 paper where he defines Turing machines, rather than actual electronic computers. Still, understanding "formal" as "mechanical" predates it.
- DougBTX 11mo ago
  Perhaps it has to be that way, the motivation to build a mechanical computer is based on the belief that computation can be mechanised.
  - DonaldPShimoda 11mo ago

tug2024 11mo ago

[dead]