4 ms·

I’ve been kicking around the idea of something like Lean (maybe even just Lean?) to rewrite news and other non-fiction articles, treating statements as theorems

• ants_everywhere 1y ago
  I don't know why you're getting downvoted because I think this is an interesting idea. Completely impossible but still interesting and fun to explore. But you don't need the power of Lean to do something like this. I would recommend starting with something like Prolog or RDF triples
  • ramses0 1y ago
    Basically [Citation Needed]
  • almostgotcaught 1y ago
    [flagged]
    • riku_iki 1y ago
      But such system exists, mostly implemented in prolog.
      • ants_everywhere 1y ago
        Does it actually?
        • kevindamm 1y ago
          The first thing this thread made me think of: https://cyc.com/ https://cyc.com/ It's been around for decades.. I'm sure there are other similar systems.
          • ants_everywhere 1y ago
            cool thanks for the link
            • riku_iki 1y ago
              there is also whole rdf/owl/semantic web ecosystem, with tons of companies/engines/datasets, mostly small.
        • adastra22 1y ago
          There are many variations, but I’m on mobile rn. (Is this the new Fermat’s last theorem?) But seriously, the idea of breaking claims into logic and using programming languages to check, compose, and verify claims is kinda the reason logical programming languages like prolog were invented.
    • ants_everywhere 1y ago
      Argument mining and automatic fact checking are things and there are actual products that do them. It seems reasonable to have some of those products implemented in a logic language.
      • im3w1l 1y ago
        I think a logic language is not a great fit, because it deals in absolute truths. Whereas news and non-fiction articles are more someone said something and they are usually reliable except in this particular domain where they can be a bit biased sometimes. Also the people they interviewed may have misremembered. Etc etc. You could argue that all such things could in principle be modelled in logical formulas but... it would be way more complicated than the stated model. On the other hand it's also unclear what the logical model actually adds. Usually logical formulas are used because they can be manipulated, and inferences can be drawn. But drawing logical inferences from sorta-kinda true statements can quickly become muddy and lead to false conclusions if you don't take into account the uncertainty of the statements.
        • poeticsilence 1y ago
          Plenty of logics with non-binary truth values...
        • ants_everywhere 1y ago
          The person suggesting it had simple heuristics like "this proposition was asserted by three sources". This has obvious flaws (e.g. I can cite three lying sources). But even on Wikipedia, there is no automatic checking that sources say what's claimed. So it wouldn't be useless despite having obvious flaws. But anyway, if you have heuristics like this you can make them propositions and do inference with them. Instead of thinking of it as "I've proved this false" or "the citations are correct" perhaps think of it more like a lint that runs against your code base and tells you whether you've done something that falls below expectations. A more natural way to model it would be something like a Bayesian system where you assign probabilities, build up a hierarchical model, and flow probabilities through the model. But there's something nice about a simpler system that doesn't pretend to do more than it can.
• magicalhippo 1y ago
  > I’ve been kicking around the idea of something like Lean (maybe even just Lean?) to rewrite news and other non-fiction articles, treating statements as theorems that need to be proven. I found I got much better at writing non-fiction after having math at uni. I would help proof-read essays and other hand-ins by my SO and sister, and apply similar rigor as you mention. Stuff like "you show C follows from B here, but you haven't actually given an argument for why B follows A, so you can't then claim C follows from A". It's tempting to say that with LLMs this seems like a plausible task to turn it into a program, but the hallucination issue puts a damper on that scheme.
  • deleted 1y ago
    [deleted]
  • refulgentis 1y ago
    A mild damper at best, RAG-based pipelines are mature now. Alas, things like this aren't logic proofs. It bothers me to my core when I see this idea. Sometimes at FAANG. Blissfully management learned to...not promote...them.
    • petesergeant 1y ago
      > A mild damper at best, RAG-based pipelines are mature now. I work with RAG pipelines all day, and the idea that hallucination isn't an ongoing major issue doesn't match my experience _at all_. Possibly a skill issue on my part, but, also on the part of everyone I ever talk to in the same space too.
  • TheOtherHobbes 1y ago
    There are rhetorical tricks which rely on this to be persuasive. You can say "Thing X is happening, so we should do Thing Y", and people will nod. If you're sneaky about it it will read like a logical conclusion when in fact X and Y are only loosely related contextually, and there is no logical chain at all. A standard political trick is to blame X on something emotive and irrelevant, and offer Y as a false solution which distracts from the real causes of the problem. This is used so often it's become a core driver of policy across multiple domains. Although it's very effective, it's a crude way to use this. There are more subtle ways - like using X to insinuate criticism of a target when Y is already self-evident. Point being, a lot of persuasive non-fiction, especially in politics, law, religion, and marketing, uses tricks like these. And many others. They work because they work in the domain of narrative logic - persuading through stories and parables with embedded emotional triggers and credible-sounding but fake explanations, where the bar of "That sounds plausible" is very low. LLMs already know some of this. You can ask ChatGPT to make any text more persuasive, and it will give you some ideas. You can also ask it to read a text, pull out the rhetorical tricks, and find the logical flaws. It won't do as good a job as someone who uses rhetoric for a living. But it will do a far better job than the average reader, who is completely unaware of rhetoric.
• bjackman 1y ago
  I think it's quite rare that the most important beliefs you should derive from the news can be justified by a collection of absolute statements. I think you'd be better served by a tool for calculating chains of Bayesian reasoning. I've seen a tool that does this for numerical estimations.
  • lblume 1y ago
    Correct. The only way to not subject oneself to (economic) irrationality is to model your beliefs about the world using probabilities and using Bayes to update in light of new evidence.
• bubblyworld 1y ago
  Formalising natural language statements is a minefield of difficulties, for (imo) essentially the same reasons that writing code which interacts with the real world is so difficult. Concepts you take for granted like identity, time, causality... all of that stuff needs to be fleshed out carefully and precisely in the formalism for facts to be relatable to each other (or even expressible in the first place). Not to discourage you - it's a cool problem! OpenCog comes to mind as a project that tried to take this all the way, and there's a field devoted to this stuff in academia called KRR (knowledge representation and reasoning). The IJCAI journal is full of research on similar topics. (also see all the different logics philosophers use to formalise different kinds of argument involving time/modality/probability - there are a lot, but they aren't very "modular" and can't easily be mixed unless someone has solved that since I last looked into it)
  • eru 1y ago
    > Concepts you take for granted like identity, time, causality... all of that stuff needs to be fleshed out carefully and precisely in the formalism for facts to be relatable to each other (or even expressible in the first place). Yes, and different formalisations of identity apply in different contexts. Eg remember the famous line about not being able to step in the same river twice.
  • photonthug 1y ago
    > logics philosophers use .. aren't very "modular" and can't easily be mixed Not sure if the model-checking communities would agree with you there. For example CTL-star [0] mixes tree-logic and linear-temporal, then PCTL adds probability on top. Knowledge, belief, and strategy-logics are also mixed pretty freely in at least some model checkers. Using mixed combinations of different-flavored logic does seem to be going OK in practice, but I guess this works best when those diverse logics can all be reduced towards the same primitive data structures that you want to actually crunch (like binary decision diagrams, or whatever). If no primitive/fast/generic structure can really be shared between logics, then you may be stuck with some irreconcilable continuous-vs-discrete or deterministic-vs-probabilistic disconnect, and then require multiple model-checkers for different pieces of one problem. So even if mixing different flavors of logics is already routine.. there's lots of improvements to hope for if practically everything can be directly represented in one place like lean. Just like mathematicians don't worry much about switching back and forth from geometry/algebra, less friction between representations would be great. Speaking of CTL, shout out to Emerson[1], who won a Turing award. If he hadn't died recently, I think he'd be surprised to hear anyone suggest he was a philosopher instead of a computer scientist ;) [0]: https://en.wikipedia.org/wiki/CTL https://en.wikipedia.org/wiki/CTL* [1]: https://en.wikipedia.org/wiki/E._Allen_Emerson https://en.wikipedia.org/wiki/E._Allen_Emerson
• wredcoll 1y ago
  I think a more practical method would be to trace the provenance of a claim, in a way that lets you evaluate how likely it is for the person making it to actually know the facts. A simple scenario would be reading a news article about american politics. You see an unusual claim made, so you start tracing it and find that the journalist got it from person X who got it from person Y who got it from donald trump. Trump is famous for lying constantly, so unless there's a second source making the claim, you could disregard it with a high probability.
• CobrastanJorji 1y ago
  I think it'd be more interesting to map out entire trees of arguments about a topic. Start with something big, like "is there a God," then come up with all of the arguments for or against, then come up with all of the arguments against those arguments, then the counters to those arguments. Really explore it as a sort of debate space. Then bring in citations not as backing but for historical context: "Plato made this argument in such and such." The idea wouldn't be so much to decide a winner as to prevent us from going around in circles by making a map.
  • vntok 1y ago
    Kialo does this for online debates: https://www.kialo.com/ https://www.kialo.com/ An example tree for the statement "God exists": https://www.kialo.com/god-exists-3491?path=3491.0~3491.1 https://www.kialo.com/god-exists-3491?path=3491.0~3491.1
  • Scarblac 1y ago
    > Start with something big, like "is there a God," To do that you first need a definition of the concept God. And then you realize that all the people making arguments in the past were using their own unspoken and incompatible definitions.
• bufferoverflow 1y ago
  [dead]
• atomicnature 1y ago
  Proof != evidence. In evidence, we corroborate, collate, add more sources, weigh evidence, judge. Proof is a totally different process. Only in the mathematical do one prove something, everywhere else we build up evidence, corroborate, etc.
• jeffhuys 1y ago
  Look at Arguman, now defunct, but you can probably find some good videos/screenshots. Basically crowd-sourced statements, rebuttals, agreements, etc, in a nice interface. We need that nowadays.
  • vntok 1y ago
    There's Kialo: https://www.kialo.com/ https://www.kialo.com/
• atoav 1y ago
  As a programmer who has studied philosophy: This is the approach I take more or less in my head when reading articles, however the problem is the ambiguity of natural language. E.g. lets say the statement is about a presidents promise to end a conflict within 24 hours after coming into office. One could get to a conclusion pretty quickly when the conflict hasn't been ended after 24 hours when they entered the office. But what does "end the conflict" mean exactly? If the conflict ended how long does it need to remain ended to achieve the label "ended"? What if said president has a history that recontextualizes the meaning of that seemingly simple claim because he is known to define the word "ended" a little different than the rest of us, do you now judge by his or by our definition? What if the conflict is ended but there is a small nest of conflict remaining, after which size do we consider the conflict going on? I know some of that has official definitions, but not everything has. In the end a lot of that will require interpretation and which definition to chose. But yeah I support your idea, just spelling it out and having a machine-readable chain of thought might help already.
  • renox 1y ago
    Bah, the answer is easy: words should be used with their most common definition, everything else is a lie. If you want to use a word 'differently' then you need to do so explicitly.
• fancy_pantser 1y ago
  Claimify from MS research aims in this direction. There's a paper and video explainer from a few months ago. https://www.microsoft.com/en-us/research/blog/claimify-extracting-high-quality-claims-from-language-model-outputs/ https://www.microsoft.com/en-us/research/blog/claimify-extra...
• Tainnor 1y ago
  I think for that kind of thing, Prolog would be sufficient. Lean is more powerful, but it requires you to supply proofs - Prolog can just automatically run inferences. (Although I wouldn't be surprised if somebody had already recreated something like Prolog in Lean with a tactic that does more or less what the Prolog interpreter does)
• t_mann 1y ago
  Careful, such an approach could easily end up giving an aura of logical objectivity to arbitrarily radical and nonsensical ideas. The political views of one of the fathers of modern logic may serve as a cautionary tale [0]. [0] https://en.m.wikipedia.org/wiki/Gottlob_Frege#Political_views_and_antisemitism https://en.m.wikipedia.org/wiki/Gottlob_Frege#Political_view...
• poulpy123 1y ago
  News and non-fiction articles are not math and cannot be treated as math. At best you could build a tool that check the most glaring contradictions (like a typo changing a number), and I'm not even sure it can be consistent without building a software that understand language. At worse you would build a tool that spit bullshit that millions of people would treat as gospel
• guyomes 1y ago
  For the form, you might be interested in Ethica, by Spinoza [1]. On the other hand, for fact checking, the key concept seems to be trust in sources rather than logical consistency. [1]: https://en.wikipedia.org/wiki/Spinoza%27s_Ethics https://en.wikipedia.org/wiki/Spinoza%27s_Ethics
• rossant 1y ago
  This might be interesting to you: https://en.m.wikipedia.org/wiki/Stephen_Toulmin#The_Toulmin_Model_of_Argument https://en.m.wikipedia.org/wiki/Stephen_Toulmin#The_Toulmin_...
• BlarfMcFlarf 1y ago
  What about proven facts that get disproven? Is there room to rethink your priors?
• viraptor 1y ago
  Check out https://argdown.org/ https://argdown.org/ for the much simpler version of that idea. No proofs, just supporting/conflicting evidence and arguments. But that's hard enough to consistently produce as it is.
• michael1999 1y ago
  I think you could just use lean, and progressively elaborate the inference graph. But you might find a historical/journalistic/investigative angle more profitable. I heard a software product pitch from a small law practice who were outside investigators for abuse/policy-violation claims in a unionized workforce. They had a solid procedure: start with the main event. Interview all witnesses, and identify other interesting events. Then cross-reference all witnesses against all alleged/interesting events. That gives you a full matrix to identify who is a reliable witness, what sort of motivations are in play, and what stories are being told, patterns of behaviour, etc. Their final report might actually focus on another event entirely that had better evidence around it. In that sort of historical investigation, a single obviously false claim undermines all claims from that witness. Pure logic doesn't have that bi-directionality of inference. Sometimes your sources just flat out lie! That's half the work. The key difference is between a full matrix of claims vs sources/evidence, while good math is all about carefully plotting a sparse inference graph that traverses the space. What is called "penetrating minimalism" in math is called "cherry picking" in history or journalism. We passed on the pitch. Didn't see how it scaled to a product worth building, but their process was appealing. Much better than the an internal popularity-contest or witch-hunt. Probably better than the average police investigation too.