9 votes

Can neural networks be used to prove conjectures?

Not in such straight forward way as described, but neural networks are successfully applied to guide the search of proof. There are automated theorem provers. What they do look roughly like this: Get ...
Arqwer's user avatar
  • 191
8 votes

Can neural networks be used to prove conjectures?

Your idea may be feasible in general, but a neural network is probably the wrong high level tool to use to explore this problem. A neural network's strength is in finding internal representations ...
Neil Slater's user avatar
  • 32.1k
6 votes

Can neural networks be used to prove conjectures?

It's possible, but probably not a good idea. Logical proof is one of the oldest areas of AI, and there are purpose-built techniques that don't need to be trained, and that are more reliable than a ...
John Doucette's user avatar
5 votes
Accepted

Has reinforcement learning been used to prove mathematical theorems?

Artificial Intelligence for Theorem Proving is an active research area as witnessed by the existence of the AITP conference and of many publications on the topic. Some papers are mentioned in this ...
Zimm i48's user avatar
  • 166
4 votes

Why is automated theorem proving so hard?

There are two ways to look at the problem, one in terms of logic and the other in terms of psychology. To get any -start- on automation of mathematics, you need to formalize the part you want. It has ...
Mitch's user avatar
  • 141
3 votes
Accepted

Would it be possible to involve a proof assistant in the process of training a LLM?

Your post has links with: An article by Stephen Wolfram [ https://writings.stephenwolfram.com/2023/01/wolframalpha-as-the-way-to-bring-computational-knowledge-superpowers-to-chatgpt/ ], stating that ...
OlivierB's user avatar
3 votes

Can a computer make a proof by induction?

There are programming languages that allow you to verify a proof by induction. For example, I used Coq, but I'm sure there are also others.
IAmUser's user avatar
  • 51
3 votes

Is beam search the actual obstacle that prevents GPT-style models from doing sophisticated math reasoning?

I think that recently it has been a very interesting topic of conversation using LLMs for planning in the context of reasoning or for the case you mentioned for mathematical proving. Specially with ...
Cesar Ruiz's user avatar
2 votes
Accepted

What exactly is the future of mathematical analysis that can be dealt with AI (especially in the automated theorem proving)?

There are many elements to be considered. To argue the answer, we can use mathematical logic reasoning. Let us assume a propositional logic (PL) context without loss of generality. First, we rephrase ...
Eduard's user avatar
  • 211
2 votes
Accepted

Can a computer make a proof by induction?

It is possible for some classes of problems. For instance, WolframAlpha can generate an induction proof to the problem posed in the question. According to the author of this proof generator, he built ...
shamisen's user avatar
  • 136
2 votes
Accepted

Is there a system that automatically designs a set of rules from the examples?

This is an active research topic. Consider reading J.Pitrat's Artificial Beings, the conscience of a conscious machine book This Understanding machine learning book old Lenat's papers on Eurisko. ...
Basile Starynkevitch's user avatar
2 votes

When will we have computer programs that can compose mathematical proofs?

Arguably we have had this since 1957, with the General Problem Solver. However, it is a thorny problem, and like so much in AI, it works fine in toy domains (like the Towers of Hanoi problem), but ...
Oliver Mason's user avatar
  • 5,387
1 vote

What are the challenges faced by using NLP to convert mathematical texts into formal logic?

I can see several challenges, and the list below is not exhaustive: i. The main problem is how to model a problem of translating a language test into a formal language. It will probably be something ...
Raphael Augusto's user avatar
1 vote

Can AI come up with scientific theories of past when provided with sufficient data available at that time?

Yes. Some good examples of this are Lipson's work using evolutionary models, and Wu & Tegmark's work on a theory-based life-long learner, and Iten et al.'s work with deep neural networks. There ...
John Doucette's user avatar
1 vote

Can neural networks be used to prove conjectures?

I've published an article with the corresponding new method based on the generative grammars of first-order theories: Thoughts on generative grammars and their use in automated theorem proving based ...
Rebel Yell's user avatar

Only top scored, non community-wiki answers of a minimum length are eligible