[HN Gopher] Formal Reasoning [pdf]
___________________________________________________________________
Formal Reasoning [pdf]
Author : Thom2503
Score : 110 points
Date : 2025-10-26 12:03 UTC (10 hours ago)
(HTM) web link (cs.ru.nl)
(TXT) w3m dump (cs.ru.nl)
| amelius wrote:
| 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 wrote:
| Essentially there is growing interest in the "formal" math
| community (combinatorics, mining, etc ..) to do exactly this.
| rramadass wrote:
| 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 transform
| English declarative -> Imperative code -
| https://news.ycombinator.com/item?id=41549823
| pjmlp wrote:
| As big Prolog fan, thanks for sharing those resources.
| tannhaeuser wrote:
| 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
| swagmoney1606 wrote:
| 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 wrote:
| 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 wrote:
| 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 wrote:
| Join the Lean Zulip. There are many people interested in
| this.
|
| https://leanprover.zulipchat.com/
| lou1306 wrote:
| 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 wrote:
| > 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 wrote:
| That's the approach we're taking to verify LLM-generated SQL
| code at http://sql.ai.
| stephenlf wrote:
| This is great reading and a great supplement to my limited
| education in math, comp sci, and formal logic.
| sn9 wrote:
| 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.
| pron wrote:
| > 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 wrote:
| 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 wrote:
| 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 wrote:
| It's not a "belief"; that's what computability _is_. This
| definition is the whole point of the work by Church and
| Turing that resulted in the lambda calculus and the Turing
| machine, respectively.
| pron wrote:
| 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 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.
| griffzhowl wrote:
| Leibniz even invented a calculating machine. I didn't know
| he'd actually built one
|
| https://en.wikipedia.org/wiki/Calculus_ratiocinator
| rramadass wrote:
| Well said.
|
| Also i highly recommend everybody to read the great logician
| Alfred Tarski's classic book _Introduction to Logic: And to the
| Methodology of Deductive Sciences_ to really understand
| "Logic" which is what Formal Reasoning is based on.
| chrisweekly wrote:
| Agreed. Also, I feel strongly that logic should be part of
| the core curriculum in liberal arts colleges if not high
| school. I took a Logic class as an undergrad, in a course
| that covered Sentential, Predicate, and Aristotelian
| (syllogistic) Logic, then became a paid tutor the next
| semester. It was profoundly useful, and applicable to nearly
| every other field of study. So many otherwise well-educated
| people frequently fall prey to common logical fallacies,
| likely because their grasp of logic is strictly intuitive and
| implicit.
| yorwba wrote:
| 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
| natural language, while other combinations are just nonsense.
|
| For a given formal language, there don't necessarily have to be
| any rules governing the words of the language, though the
| languages used for writing formal proofs are typically more
| well-behaved.
| pron wrote:
| 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 the decidability of whether a statement is
| provable or not (using the language's inference rules).
|
| 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.
___________________________________________________________________
(page generated 2025-10-26 23:00 UTC)