[Submitted on 18 Apr 2024 (v1), last revised 3 Mar 2025 (this version, v2)]
Abstract:Translating natural language into formal language such as First-Order Logic (FOL) is a foundational challenge in NLP with wide-ranging applications in automated reasoning, misinformation tracking, and knowledge validation. In this paper, we introduce Natural Language to First-Order Logic (NL2FOL), a framework to autoformalize natural language to F
23 Comments
rahimnathwani
The paper links the code repo: https://github.com/lovishchopra/NL2FOL
But I don't see a pretrained model in there, so I'm not sure what to pass as `your_nli_model_name`:
FloorEgg
Not familiar with FOL as a formalism, and would love to see this in action. I feel like it's a big part of the solution to propaganda.
The other part seems to be values obfuscation, and I wonder if this would help with that too.
If Joe says that nails are bad, it can mean very different things if Joe builds houses for a living and prefers screws, or if Joe is anti development and thinks everyone should live in mud huts.
Propaganda will often cast a whole narrative that can be logically consistent, but entirely misrepresents a person or people's values (their motivations and the patterns that explain their actions), and there will be logical fallacies at the boundaries of the narrative.
We need systems that can detect logical fallacies, as well as value system inconsistencies.
ColinWright
It was Gottfried Leibniz who envisaged the end of philosophic disputes, replacing argument with calculation.
"if controversies were to arise, there would be no more need of disputation between two philosophers than between two calculators. For it would suffice for them to take their pencils in their hands and to sit down at the abacus, and say to each other (and if they so wish also to a friend called to help): Let us calculate."
languagehacker
It sounds like the data set they use is designed to teach what logical fallacies are, which makes sense that it would do fine with it. I doubt this would do well against real-world language with things like structural ambiguity, anaphoric resolution, and dubious intent.
MortyWaves
Trolls that knowingly engage in bad arguments with flawed logic are going to be in shambles.
mike_hearn
Love the idea in theory and would like such a tool to exist, but the use cases they present aren't convincing. This would be useful in much more specific cases like drafting contracts, laws or technical documentation: places where unusually precise language without corner cases is mutually desired by everyone, and the set of fallacies that occur is small and specific.
This paper doesn't target such use cases. Instead it's trying to tackle "pop misinformation" type claims, mostly related to climate change. Unfortunately the Logic and LogicClimate datasets that the paper are using as a benchmark have serious problems that should disqualify them from being considered a benchmark. If we check the paper that introduced them, Jin et al open by asserting that "She is the best because she is better than anyone else" is an example of circular reasoning. It's actually a tautology. Then they try again with "Global warming doesn’t exist because the earth is not getting warmer" which is also not circular reasoning, it's another tautological restatement (you may say it's false, but disagreement over facts isn't a disagreement over logic – if either clause is true so is the other). Circular reasoning often involves a mis-definition and would be something like this real-world example from a few years ago:
1. A positive test is means you have COVID.
2. Having COVID is defined as having a positive test.
Their second example is "Extreme weather-related deaths in the U.S. have decreased by more than 98% over the last 100 years … Global warming saves lives" which they classed as "false causality" (they mean non-sequitur). My experience has been that climate skeptics are surprisingly logical so this would be an odd statement for them to make, and indeed if we check the original Washington Times op-ed then we find Jin et al are engaging in malicious quoting. It actually says:
> "Contrary to sensational media reports, extreme weather-related deaths in the U.S. have decreased more than 98% over the last 100 years. Twenty times as many people die from cold as from heat, according to a worldwide review of 74 million temperature-related deaths by Dr. Antonio Gasparrini and a team of physicians. Global warming saves lives."
The saves lives claim is based on cold being more dangerous than heat. Warmer weather = fewer deaths from cold isn't a logical fallacy, which is why they had to delete that part to make their example. It might sound like a weird or disingenuous argument to you, but it's logical in the sense that an SMT solver would approve of it. If you disagree it's probably due to prior beliefs e.g. that perhaps extreme weather has increased even as society got orders of magnitude better at reducing the impacts, or perhaps the positive effects of warmer air on the elderly are offset by other effects of climate change, or that the future will be different to the past due to compounding effects. Such rebuttals aren't identifications of a logical fallacy though, just of different priors that could maybe be addressed with additional rounds of debate.
analog31
Doesn't Goedel's Theorem forbid building a logic checker?
nico
Is this just another form of the same concept behind smart contracts?
zozbot234
I'm pretty sure that the semantics of natural language are a lot more complex than can be accounted for by these seemingly very ad-hoc translations into comparatively straightforward FOL formulas, as are given in this paper. A common approach for the understanding of NL semantics from a strictly formal POV is Montague semantics https://en.wikipedia.org/wiki/Montague_grammar https://plato.stanford.edu/entries/montague-semantics/ – even a cursory look at these references is enough to clarify the level of complexity that's involved. Very loosely speaking one generally has to work with multiple "modalities" at the same time each of which, when understood from the POV of ordinary FOL, introduces its own separate notion of abstract "possible worlds" (representing, e.g. an agent's set of beliefs) and ways in which these "worlds" can relate to one another. More complex cases will usually degenerate in some sort of very generic "game semantics" https://en.wikipedia.org/wiki/Game_semantics https://plato.stanford.edu/entries/logic-games/ where any given use of natural language is merely seen as a "game" (in the abstract strategic, game-theoretical sense) with its own set of possibly very ad-hoc 'rules'. The philosopher Ludwig Wittgenstein https://en.wikipedia.org/wiki/Ludwig_Wittgenstein https://plato.stanford.edu/entries/wittgenstein/ gave quite a good description of both of these approaches (from a very naïve approach based on a supposedly straightforward translation to some kind of abstract logic, to a far richer one based on notions of strategies and games) to a "formal" understanding of natural language, throughout his extensive philosophical inquiry.
Which is to say, I'm not sure how this paper's results are generally expected to be all that useful in practice.
pixelpoet
Oh man, where was this back in the 90s arguing with proto-trolls on IRC and usenet who shamelessly moved goalposts, stawmanned, appealed to authority, resorted to ad hominem, …
Imagine if you could click on a stupid internet discussion thread and make it give you a Lean proof of each argument where possible :D This thing would be hated even more than, say, vaccines, by the same sorts of people who deliberately choose to not understand things.
shortrounddev2
I believe this is something Immanuel Kant tried to do in the 18th century
qgin
I don't know how much potential this has to solve propaganda / bad faith arguments because you can just say "that logic program is biased" and handwave the entire thing away.
But you could imagine a role for this in arbitration or legal settings.
giardini
Prolog has always had DCGs (Definite Clause Grammars) that allow you to write rules that resemble natural language grammar structures to parse and generate English sentences:
https://www.metalevel.at/prolog/dcg
svnt
This is already something that e.g. Claude 3.7 Sonnet appears to be able to do very well, with the added benefit of explaining why if you let it — what is the benefit of this model?:
> "Sometimes flu vaccines don't work; therefore vaccines are useless." – Hasty generalization
> "Every time I wash my car, it rains. Me washing my car has a definite effect on the weather." – Post hoc, ergo propter hoc
> "Everyone should like coffee: 95% of teachers do!" – Appeal to popularity and hasty generalization
> "I don't want to give up my car, so I don't think I can support fighting climate change." – False dilemma
EigenLord
This is very cool and definitely a step in the right direction, however, the question remains where exactly this formalizing module should be placed in the stack. As an external api, it's clear that the model is not "thinking" in these logical terms, it just provides a translation step. I'd argue it would be better placed during inference test-time compute (as seen in these so-called reasoning models). Better yet, this formalizing step would happen at a lower level entirely, internal to the model, but that would probably require totally new architectures.
Geee
Yes, this is exactly what I've been dreaming about. It might finally be possible to beat the bullshit asymmetry law, i.e. Brandolini's law: "The amount of energy needed to refute bullshit is an order of magnitude bigger than to produce it."
If LLMs can debunk bullshit as easily as it's generated, the world will instantly turn into a better place.
Bad ideas which sound good are the root of all evil.
tiberius_p
First order logic can only detect formal logic fallacies. Informal logic fallacies like ad hominem, strawman, red herring, etc. are cast in language. They can't me defined and resolved mathematically. The model should be fine tuned with examples of these informal fallacies and counter-arguments to them. Even so it won't be able to detect them in all cases, but it will at least have some knowledge about them and how to reply to them. This knowledge could be further be refined with in context learning and other prompt engineering strategies.
hackandthink
[dead]
sergix
https://xkcd.com/2610/
booleandilemma
This is a threat to my company's product managers.
CJefferson
Turning English into logic basically requires understanding the language and context.
I’d you are told “we will go to the zoo or swimming pool tomorrow, if it is windy or rainy”, most readers would know the first or is exclusive (we aren’t going to both), while the second is inclusive (we will go if it is windy, rainy, or both).
This is annoying when teaching logic, from experience.
talles
The entire analytic philosophy movement is nowhere to be seen in the paper (?)
grandempire
It’s a nerd fantasy to imagine argumentation is a logical formula, and by memorizing all the bad forms you will win arguments and detect falsehood.