8 ms·

What do you think, how long until we can give conjectures to a specially trained LLM to come up with a proof?

by kleiba 3y ago

brap 3y ago
My uneducated hunch is that we’re just a few years away from “proof search” being a solved problem. But that’s only a part of mathematical research.
- prmph 3y ago
  I think you are much too optimistic. Proof verification, though still hard to automate, seems at least tractable. I'm not a mathematician by any means, but something tells me automated proof search, in the general case, would require solving the halting problem, which means it is impossible even in principle.
  - dumbo-octopus 3y ago
    In the general case, proof search is obviously impossible, for the reason you state. But the case need not be general. A proof search machine that takes in a theorem and outputs `"proof: ..." | "antiProof: ..." | "idk"` would be quite powerful indeed.
    - gpm 3y ago
      def decider(_): print("idk") Done ;) --- More seriously, the benchmark would be something along the lines of "and it is better at finding proofs than humans are", like how chess engines haven't solved chess, but they are so much better than humans that they always win in a competition between the two. There's no good reason to think that humans are capable of finding proofs that are hard to find algorithmically.
      - brap 3y ago
        >There's no good reason to think that humans are capable of finding proofs that are hard to find algorithmically That’s really all I was trying to say, not sure why I’m getting downvoted
      - dumbo-octopus 3y ago
        Clearly the prevalence of idk's in the output is the metric for determining power. As for the human-vs-computer, I think the most powerful solutions will be those that combine human and computer prowess, similar to how a Human+Stockfish beats Stockfish^. To that end I've been working on Lean search tools that keep a human firmly in the loop. Terence has actually called out a tool I helped make as being quite helpful in his work, which is rather neat. ^ I heard this to be true at some point, but cannot find any reference on it at the moment.
        gpm 3y ago
        > similar to how a Human+Stockfish beats Stockfish^ > ^ I heard this to be true at some point, but cannot find any reference on it at the moment. Known as centaur chess (amongst other things). It was certainly the case at one point. I strongly suspect that it isn't still the case, but it's hard to say for absolute certainty because it never developed a serious competitive community like engine and non-engine chess has. I can't find anyone listing any results post 2017 [1]. It was barely the case in 2017, and Stockfish has improved a lot since then [2]. [1] https://gwern.net/note/note#advanced-chess-obituary https://gwern.net/note/note#advanced-chess-obituary [2] E.g. here's someone running stockfish 14 (current from July 2 2021 - April 18 2022) against stockfish 8 (current from November 1 2016 to February 1 2018). Stockfish 14 won 61 games and drew 3: https://www.reddit.com/r/chess/comments/oov714/64_game_match_between_the_new_stockfish_14_and/ https://www.reddit.com/r/chess/comments/oov714/64_game_match... (PS: They don't document time controls and I'm not sure how scientific this test was, but it matches with what I would expect, so eh) Not to discourage you from your project with lean. At the very least I would expect there to be a transitional period, likely of decades, where computer+human is better than computer.
        zone411 3y ago
        In the 2022 Correspondence Chess Championship, humans hurt the performance of computers by themselves. I posted about this here: https://twitter.com/LechMazur/status/1721008768899555677 https://twitter.com/LechMazur/status/1721008768899555677
    - thaumasiotes 3y ago
      > "antiProof: ..." The standard terminology would be "counterexample".
  - dellamonica 3y ago
    It doesn't require anything like that. Math proofs are of NP complexity. If you had access to a non deterministic Turing machine you could enumerate all possible proofs of a given length and check them all in poly time. That does not say anything about LLMs though. Personally, I believe they could be quite helpful to mathematicians in a way similar to copilot for software programming.
    - explaininjs 3y ago
      > you could enumerate all possible proofs of a given length That does not help us with proof search as we do not know the target length.
      - bawolff 3y ago
        A proof longer than the size of the universe is also pretty useless and probably not something we need to worry about. Like i guess you are saying we couldn't really use such a machine to determine whether a certain conjecture just has a very long proof/disproof or is actually undecidable. Which sure, but umm i think that is the sort of problem most mathematicians would love to have. The real reason non-deterministic turing machines can't help us is that they dont actually exist.
      - dellamonica 3y ago
        Of course it would, you would enumerate lengths too. If the lengths need to be larger than polynomially bounded then we can be sure it would never be found by a human anyway.
        explaininjs 3y ago
        > If the lengths need to be larger than polynomially bounded then we can be sure it would never be found by a human anyway. We cannot, as a human might be able to intuitively devise proof that might be quite large in the target language but easily constructible in a separate one.
        3y ago
  - deleted 3y ago
    [deleted]
    - Ar-Curunir 3y ago
      Given that algorithm design is very much a field of mathematics, it’s in principle (and probably in practice) not too difficult to adapt the infrastructure you mentioned to support a workflow where you say “I want an algorithm that on input x computes y” (more formally, ofc), and the tool outputs exactly that for you
- waynecochran 3y ago
  Neither RH nor P vs NP will succumb.
vakkermans 3y ago
Finding a proof is a search in a large space, akin to searching from abstractions to concretions. LLMs don’t do anything like this, and so you’re looking at the planning problem again. It’s not clear to me how framing this particular problem as a language problem is helpful in any case.
- thisismyswamp 3y ago
  Playing chess & go is also search in a large tree of moves leading to particular game states
  - pxeger1 3y ago
    But AlphaGo etc don’t use any kind of language-based AI, so LLMs (which this thread was about) are no good.
    - thisismyswamp 3y ago
      The next step seems to be applying past advances in reinforcement learning with modern transformer based models
      - mattsan 3y ago
        Which multiple teams are working on - OpenAI (Q*), and Meta just released a reinforcement learning framework
        npsomaratna 3y ago
        Could you point me towards Meta's reinforcement learning framework? I'd like to see how it stacks up against the OpenAI gym.
        mattsan 3y ago
        Sure thing - https://pearlagent.github.io/ https://pearlagent.github.io/ HN post here: https://news.ycombinator.com/item?id=38564526 https://news.ycombinator.com/item?id=38564526
deleted 3y ago
[deleted]
bawolff 3y ago
At the same level of success as a mathematician? Never. At the same level of success as your average high school graduate? Probably already can.
- kaba0 3y ago
  I assume an average high school graduate can solve a sudoku. LLMs are very interesting but anything “thinking”-related is not their strong suit.
  - bawolff 3y ago
    Solving sudoku is not really a proof. Like its a witness that a solution exists but i dont think that's really the thing most people mean by write a proof. LLMs are really good at cutting and pasting from the internet. That's the level i would expect from average high school student.
    - thaumasiotes 3y ago
      Solving sudoku is a pure exercise in proving what the solution is. But most sudoku tend to be unsatisfying in that you're forced to use trial and error. The more formal term would be "proof by cases": once your fun proving has reached its limits, you've shown that a particular cell must contain either 5 or 7. If you show that that cell containing a 5 will lead to a contradiction, you've created an impeccable proof that the cell contains a 7. The distinction you've stated would only come into play if the number of possible solutions to a puzzle differs from one; if there are no solutions, you have inconsistent premises and your proofs will be valid but not sound. If there are several solutions, then guessing and being right will, as you describe, create a proof that a solution exists, but it won't prove that that solution is unique or characterize what valid solutions are like, both of which are common mathematical goals.
auntienomen 3y ago
Open conjectures are usually solved by inventing new mathematical frameworks that embed the context of the existing question. Inventing new definitions is trivial, but there's no rules that constrain the space of moves. And inventing _interesting_ new definitions is extremely hard. I wouldn't bet on LLMs doing this ever.
- auntienomen 3y ago
  What would be nice is an LLM to aid in translation between mathematics and a theorem proving language like Lean. That might fuel a revolution in how mathematics is done.
kaba0 3y ago
For trivial stuff, it might be able to even now (but those can probably be solved algorithmically as well). For more complex stuff, they are not even scratching the surface, I would believe — LLMs can’t really do long, complex thoughts/inferences, which are essential for coming up with proofs, or even just to solve a sudoku (which they can’t do — no, writing a program (which was likely part of its training set) and executing that doesn’t count).
llwu 3y ago
I contributed a few trivial proofs to this project, and I tried enlisting GPT-4, Copilot, Moogle, and Morph Prover to help out (I did not try LLMStep or ReProver). Out of these: - GPT-4 answered maybe one or two questions about syntax - Copilot autocompleted maybe 0.5% - Moogle was helpful much more often but still often pointed to the wrong theorem in the right file; in most of those cases I could have just done go-to-def to get to the right file and scroll through it Note that these results are actually very good! And Terence Tao seems to have a positive opinion as well. But we're very far away from automatically proving conjectures IMO. I will say that Lean has great metaprogramming facilities to accept any type of AI innovation that might emerge. Currently I find the most helpful tactics to be `aesop?`, which is a classical search tactic that tries a bunch of substitutions and simplifications; and `exact?`, when you know there's a trivial proof but not sure of the name. But the UX for AI can be as simple as, for example, typing the `gptf` or `llmstep` tactic, and that is fully hooked into the Lean state (goals, hypotheses, etc). So there's a lot of opportunity for incremental progress in improving existing workflows (which consist of dispatching trivial manipulations with search/simplification tactics)
srcreigh 3y ago
It will never happen. Some open math problems are equivalent to the halting problem; and we know that finite computers can’t solve the halting problem.
- MaxBarraclough 3y ago
  That doesn't sound right, we already have automated theorem provers, as imperfect as they may be.
steego 3y ago
Check out this paper: https://leandojo.org/ https://leandojo.org/ People have already trained models to assist suggestion tactics. They then linked it up to ChatGPT to interactively solve proofs. In this scenario, ChatGPT asks the model for tactic suggestions, applies it to the proof and uses the feedback from Lean to then proceed with the next step. FYI, The programmatic interface to Lean was written by an OpenAI employee who was on the Lean team a few years ago. Also, check out Lean’s roadmap. They aspire to position Lean to becoming a target for LLMs because it has been designed for verification from the ground up. As math and compsci nerds contribute to mathlib, all of those proofs are also building up a huge corpus that will likely be leveraged for both verification and optimization. If AI can make verification a lot easier, then we’re likely going to see verification change programming similarly to the way it changed electronics.
- staunton 3y ago
  > it has been designed for verification from the ground up. It has a lot of places where you assume things work in a certain way and a lot of ways to assume it (and you can prove `false` if any of those assumptions aren't correct). I'd say it's a lot more geared towards formalizing math than verification. There's some more things, e.g., the `Expression -> C-code` "compiler" isn't verified and neither is the C-compiler. Those could be fixed with some work (that nobody is working on currently, as far as I can tell). But the first issue seems pervasive. I don't think Lean will become a standard tool for software verification or significantly advance the discipline. Of course, I'd love to be wrong.
  - zozbot234 3y ago
    If the foundations are workable (and they seems to be, though IIRC there is a quotienting construct that's quite ad hoc and that people have complained about), the fact that you can additionally "assume" other things is fairly irrelevant, these are no different than extra axioms.
    - staunton 3y ago
      It's not useful to prove that "your program does what you want, provided the following 10000 functions implemented in C do what we assumed they do". Almost certainly at least one of them doesn't. There isn't even a straightforward (let alone verified) way to list all assumptions of this type for some proof (you can print the axioms that a definition depends on, but that's not the same thing). It's possible to prove `false` in Lean using functions you'd normally use to make pretty much any useful program.
golly_ned 3y ago
Recent work on combining LLMs with theorem provers with promising initial results: https://paperswithcode.com/paper/linc-a-neurosymbolic-approach-for-logical https://paperswithcode.com/paper/linc-a-neurosymbolic-approa... > Logical reasoning, i.e., deductively inferring the truth value of a conclusion from a set of premises, is an important task for artificial intelligence with wide potential impacts on science, mathematics, and society. While many prompting-based strategies have been proposed to enable Large Language Models (LLMs) to do such reasoning more effectively, they still appear unsatisfactory, often failing in subtle and unpredictable ways. In this work, we investigate the validity of instead reformulating such tasks as modular neurosymbolic programming, which we call LINC: Logical Inference via Neurosymbolic Computation. In LINC, the LLM acts as a semantic parser, translating premises and conclusions from natural language to expressions in first-order logic. These expressions are then offloaded to an external theorem prover, which symbolically performs deductive inference. Leveraging this approach, we observe significant performance gains on FOLIO and a balanced subset of ProofWriter for three different models in nearly all experimental conditions we evaluate. On ProofWriter, augmenting the comparatively small open-source StarCoder+ (15.5B parameters) with LINC even outperforms GPT-3.5 and GPT-4 with Chain-of-Thought (CoT) prompting by an absolute 38% and 10%, respectively. When used with GPT-4, LINC scores 26% higher than CoT on ProofWriter while performing comparatively on FOLIO. Further analysis reveals that although both methods on average succeed roughly equally often on this dataset, they exhibit distinct and complementary failure modes. We thus provide promising evidence for how logical reasoning over natural language can be tackled through jointly leveraging LLMs alongside symbolic provers. All corresponding code is publicly available at https://github.com/benlipkin/linc https://github.com/benlipkin/linc
- cubefox 3y ago
  But "theorem provers" don't prove anything, they just check existing proofs for validity. That's a much less demanding task than coming up with a proof in the first place.

What do you think, how long until we can give conjectures to a specially trained LLM to come up with a proof?

by kleiba 3y ago

What do you think, how long until we can give conjectures to a specially trained LLM to come up with a proof?

brap 3y ago

My uneducated hunch is that we’re just a few years away from “proof search” being a solved problem. But that’s only a part of mathematical research.

prmph 3y ago
I think you are much too optimistic. Proof verification, though still hard to automate, seems at least tractable. I'm not a mathematician by any means, but something tells me automated proof search, in the general case, would require solving the halting problem, which means it is impossible even in principle.
- dumbo-octopus 3y ago
  In the general case, proof search is obviously impossible, for the reason you state. But the case need not be general. A proof search machine that takes in a theorem and outputs `"proof: ..." | "antiProof: ..." | "idk"` would be quite powerful indeed.
  - gpm 3y ago
    def decider(_): print("idk") Done ;) --- More seriously, the benchmark would be something along the lines of "and it is better at finding proofs than humans are", like how chess engines haven't solved chess, but they are so much better than humans that they always win in a competition between the two. There's no good reason to think that humans are capable of finding proofs that are hard to find algorithmically.
    - brap 3y ago
      >There's no good reason to think that humans are capable of finding proofs that are hard to find algorithmically That’s really all I was trying to say, not sure why I’m getting downvoted
    - dumbo-octopus 3y ago
      Clearly the prevalence of idk's in the output is the metric for determining power. As for the human-vs-computer, I think the most powerful solutions will be those that combine human and computer prowess, similar to how a Human+Stockfish beats Stockfish^. To that end I've been working on Lean search tools that keep a human firmly in the loop. Terence has actually called out a tool I helped make as being quite helpful in his work, which is rather neat. ^ I heard this to be true at some point, but cannot find any reference on it at the moment.
      - gpm 3y ago
        > similar to how a Human+Stockfish beats Stockfish^ > ^ I heard this to be true at some point, but cannot find any reference on it at the moment. Known as centaur chess (amongst other things). It was certainly the case at one point. I strongly suspect that it isn't still the case, but it's hard to say for absolute certainty because it never developed a serious competitive community like engine and non-engine chess has. I can't find anyone listing any results post 2017 [1]. It was barely the case in 2017, and Stockfish has improved a lot since then [2]. [1] https://gwern.net/note/note#advanced-chess-obituary https://gwern.net/note/note#advanced-chess-obituary [2] E.g. here's someone running stockfish 14 (current from July 2 2021 - April 18 2022) against stockfish 8 (current from November 1 2016 to February 1 2018). Stockfish 14 won 61 games and drew 3: https://www.reddit.com/r/chess/comments/oov714/64_game_match_between_the_new_stockfish_14_and/ https://www.reddit.com/r/chess/comments/oov714/64_game_match... (PS: They don't document time controls and I'm not sure how scientific this test was, but it matches with what I would expect, so eh) Not to discourage you from your project with lean. At the very least I would expect there to be a transitional period, likely of decades, where computer+human is better than computer.
        zone411 3y ago
        In the 2022 Correspondence Chess Championship, humans hurt the performance of computers by themselves. I posted about this here: https://twitter.com/LechMazur/status/1721008768899555677 https://twitter.com/LechMazur/status/1721008768899555677
  - thaumasiotes 3y ago
    > "antiProof: ..." The standard terminology would be "counterexample".
- dellamonica 3y ago
  It doesn't require anything like that. Math proofs are of NP complexity. If you had access to a non deterministic Turing machine you could enumerate all possible proofs of a given length and check them all in poly time. That does not say anything about LLMs though. Personally, I believe they could be quite helpful to mathematicians in a way similar to copilot for software programming.
  - explaininjs 3y ago
    > you could enumerate all possible proofs of a given length That does not help us with proof search as we do not know the target length.
    - bawolff 3y ago
      A proof longer than the size of the universe is also pretty useless and probably not something we need to worry about. Like i guess you are saying we couldn't really use such a machine to determine whether a certain conjecture just has a very long proof/disproof or is actually undecidable. Which sure, but umm i think that is the sort of problem most mathematicians would love to have. The real reason non-deterministic turing machines can't help us is that they dont actually exist.
    - dellamonica 3y ago
      Of course it would, you would enumerate lengths too. If the lengths need to be larger than polynomially bounded then we can be sure it would never be found by a human anyway.
      - explaininjs 3y ago
        > If the lengths need to be larger than polynomially bounded then we can be sure it would never be found by a human anyway. We cannot, as a human might be able to intuitively devise proof that might be quite large in the target language but easily constructible in a separate one.
        3y ago
- deleted 3y ago
  [deleted]
  - Ar-Curunir 3y ago
    Given that algorithm design is very much a field of mathematics, it’s in principle (and probably in practice) not too difficult to adapt the infrastructure you mentioned to support a workflow where you say “I want an algorithm that on input x computes y” (more formally, ofc), and the tool outputs exactly that for you
waynecochran 3y ago
Neither RH nor P vs NP will succumb.

vakkermans 3y ago

Finding a proof is a search in a large space, akin to searching from abstractions to concretions. LLMs don’t do anything like this, and so you’re looking at the planning problem again. It’s not clear to me how framing this particular problem as a language problem is helpful in any case.

thisismyswamp 3y ago
Playing chess & go is also search in a large tree of moves leading to particular game states
- pxeger1 3y ago
  But AlphaGo etc don’t use any kind of language-based AI, so LLMs (which this thread was about) are no good.
  - thisismyswamp 3y ago
    The next step seems to be applying past advances in reinforcement learning with modern transformer based models
    - mattsan 3y ago
      Which multiple teams are working on - OpenAI (Q*), and Meta just released a reinforcement learning framework
      - npsomaratna 3y ago
        Could you point me towards Meta's reinforcement learning framework? I'd like to see how it stacks up against the OpenAI gym.
        mattsan 3y ago
        Sure thing - https://pearlagent.github.io/ https://pearlagent.github.io/ HN post here: https://news.ycombinator.com/item?id=38564526 https://news.ycombinator.com/item?id=38564526

deleted 3y ago

[deleted]

bawolff 3y ago

At the same level of success as a mathematician? Never. At the same level of success as your average high school graduate? Probably already can.

kaba0 3y ago
I assume an average high school graduate can solve a sudoku. LLMs are very interesting but anything “thinking”-related is not their strong suit.
- bawolff 3y ago
  Solving sudoku is not really a proof. Like its a witness that a solution exists but i dont think that's really the thing most people mean by write a proof. LLMs are really good at cutting and pasting from the internet. That's the level i would expect from average high school student.
  - thaumasiotes 3y ago
    Solving sudoku is a pure exercise in proving what the solution is. But most sudoku tend to be unsatisfying in that you're forced to use trial and error. The more formal term would be "proof by cases": once your fun proving has reached its limits, you've shown that a particular cell must contain either 5 or 7. If you show that that cell containing a 5 will lead to a contradiction, you've created an impeccable proof that the cell contains a 7. The distinction you've stated would only come into play if the number of possible solutions to a puzzle differs from one; if there are no solutions, you have inconsistent premises and your proofs will be valid but not sound. If there are several solutions, then guessing and being right will, as you describe, create a proof that a solution exists, but it won't prove that that solution is unique or characterize what valid solutions are like, both of which are common mathematical goals.

auntienomen 3y ago

Open conjectures are usually solved by inventing new mathematical frameworks that embed the context of the existing question. Inventing new definitions is trivial, but there's no rules that constrain the space of moves. And inventing _interesting_ new definitions is extremely hard. I wouldn't bet on LLMs doing this ever.

auntienomen 3y ago
What would be nice is an LLM to aid in translation between mathematics and a theorem proving language like Lean. That might fuel a revolution in how mathematics is done.

kaba0 3y ago

For trivial stuff, it might be able to even now (but those can probably be solved algorithmically as well). For more complex stuff, they are not even scratching the surface, I would believe — LLMs can’t really do long, complex thoughts/inferences, which are essential for coming up with proofs, or even just to solve a sudoku (which they can’t do — no, writing a program (which was likely part of its training set) and executing that doesn’t count).

llwu 3y ago

I contributed a few trivial proofs to this project, and I tried enlisting GPT-4, Copilot, Moogle, and Morph Prover to help out (I did not try LLMStep or ReProver). Out of these: - GPT-4 answered maybe one or two questions about syntax - Copilot autocompleted maybe 0.5% - Moogle was helpful much more often but still often pointed to the wrong theorem in the right file; in most of those cases I could have just done go-to-def to get to the right file and scroll through it Note that these results are actually very good! And Terence Tao seems to have a positive opinion as well. But we're very far away from automatically proving conjectures IMO. I will say that Lean has great metaprogramming facilities to accept any type of AI innovation that might emerge. Currently I find the most helpful tactics to be `aesop?`, which is a classical search tactic that tries a bunch of substitutions and simplifications; and `exact?`, when you know there's a trivial proof but not sure of the name. But the UX for AI can be as simple as, for example, typing the `gptf` or `llmstep` tactic, and that is fully hooked into the Lean state (goals, hypotheses, etc). So there's a lot of opportunity for incremental progress in improving existing workflows (which consist of dispatching trivial manipulations with search/simplification tactics)

srcreigh 3y ago

It will never happen. Some open math problems are equivalent to the halting problem; and we know that finite computers can’t solve the halting problem.

MaxBarraclough 3y ago
That doesn't sound right, we already have automated theorem provers, as imperfect as they may be.

steego 3y ago

Check out this paper: https://leandojo.org/ https://leandojo.org/ People have already trained models to assist suggestion tactics. They then linked it up to ChatGPT to interactively solve proofs. In this scenario, ChatGPT asks the model for tactic suggestions, applies it to the proof and uses the feedback from Lean to then proceed with the next step. FYI, The programmatic interface to Lean was written by an OpenAI employee who was on the Lean team a few years ago. Also, check out Lean’s roadmap. They aspire to position Lean to becoming a target for LLMs because it has been designed for verification from the ground up. As math and compsci nerds contribute to mathlib, all of those proofs are also building up a huge corpus that will likely be leveraged for both verification and optimization. If AI can make verification a lot easier, then we’re likely going to see verification change programming similarly to the way it changed electronics.

staunton 3y ago
> it has been designed for verification from the ground up. It has a lot of places where you assume things work in a certain way and a lot of ways to assume it (and you can prove `false` if any of those assumptions aren't correct). I'd say it's a lot more geared towards formalizing math than verification. There's some more things, e.g., the `Expression -> C-code` "compiler" isn't verified and neither is the C-compiler. Those could be fixed with some work (that nobody is working on currently, as far as I can tell). But the first issue seems pervasive. I don't think Lean will become a standard tool for software verification or significantly advance the discipline. Of course, I'd love to be wrong.
- zozbot234 3y ago
  If the foundations are workable (and they seems to be, though IIRC there is a quotienting construct that's quite ad hoc and that people have complained about), the fact that you can additionally "assume" other things is fairly irrelevant, these are no different than extra axioms.
  - staunton 3y ago
    It's not useful to prove that "your program does what you want, provided the following 10000 functions implemented in C do what we assumed they do". Almost certainly at least one of them doesn't. There isn't even a straightforward (let alone verified) way to list all assumptions of this type for some proof (you can print the axioms that a definition depends on, but that's not the same thing). It's possible to prove `false` in Lean using functions you'd normally use to make pretty much any useful program.

golly_ned 3y ago

Recent work on combining LLMs with theorem provers with promising initial results: https://paperswithcode.com/paper/linc-a-neurosymbolic-approach-for-logical https://paperswithcode.com/paper/linc-a-neurosymbolic-approa... > Logical reasoning, i.e., deductively inferring the truth value of a conclusion from a set of premises, is an important task for artificial intelligence with wide potential impacts on science, mathematics, and society. While many prompting-based strategies have been proposed to enable Large Language Models (LLMs) to do such reasoning more effectively, they still appear unsatisfactory, often failing in subtle and unpredictable ways. In this work, we investigate the validity of instead reformulating such tasks as modular neurosymbolic programming, which we call LINC: Logical Inference via Neurosymbolic Computation. In LINC, the LLM acts as a semantic parser, translating premises and conclusions from natural language to expressions in first-order logic. These expressions are then offloaded to an external theorem prover, which symbolically performs deductive inference. Leveraging this approach, we observe significant performance gains on FOLIO and a balanced subset of ProofWriter for three different models in nearly all experimental conditions we evaluate. On ProofWriter, augmenting the comparatively small open-source StarCoder+ (15.5B parameters) with LINC even outperforms GPT-3.5 and GPT-4 with Chain-of-Thought (CoT) prompting by an absolute 38% and 10%, respectively. When used with GPT-4, LINC scores 26% higher than CoT on ProofWriter while performing comparatively on FOLIO. Further analysis reveals that although both methods on average succeed roughly equally often on this dataset, they exhibit distinct and complementary failure modes. We thus provide promising evidence for how logical reasoning over natural language can be tackled through jointly leveraging LLMs alongside symbolic provers. All corresponding code is publicly available at https://github.com/benlipkin/linc https://github.com/benlipkin/linc

cubefox 3y ago
But "theorem provers" don't prove anything, they just check existing proofs for validity. That's a much less demanding task than coming up with a proof in the first place.