Skip to main content

Questions tagged [automated-theorem-proving]

For questions related to the automation of mathematical theorem proving, including rules systems, the acquisition of predicate logic and inference by deep networks, combinations of these, or novel new designs and supporting algorithms.

Filter by
Sorted by
Tagged with
0 votes
0 answers

How is pass@k metric defined for automated theorem provers if we have a verifier?

The pass@k metric was proposed to measure the percentage of successful code samples (, but it has also been used in automated theorem proving such as
user131379's user avatar
4 votes
0 answers

How feasible is it to automate Theorem Proving via Reinforcement Learning?

Theorem proving is basically a turn-based game with perfect information: you start from a given gamestate (a proposition) and make moves that lead to other valid gamestates. A piece of software can ...
Blue Nebula's user avatar
3 votes
1 answer

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

This is a rather soft question. Some people believe that GPT-style models can eventually solve very complex math problems if the models are large enough, but I'm skeptical about this. Suppose the GPT ...
Soha's user avatar
  • 31
3 votes
1 answer

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

As a student of numerical analysis, I can see how mathematical analysis involved in making a language program specifically in the convergence analysis of an approximation method. But, while chatting ...
Messi Lio's user avatar
  • 133
2 votes
1 answer

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

LLMs like GPT-3 have been shown capable of outputting highly complex code. Sadly, actually using them to replace a programmer's job has two major caveats: LLMs are notoriously bad at producing ...
MaiaVictor's user avatar
18 votes
1 answer

Why is automated theorem proving so hard?

The problem of automated theorem proving (ATP) seems to be very similar to playing board games (e.g. chess, go, etc.): it can also be naturally stated as a problem of a decision tree traversal. ...
Ivan Ivanov's user avatar
2 votes
2 answers

Can a computer make a proof by induction?

Can a computer solve the following problem, i.e. make a proof by induction? And why? Prove by induction that $$\sum_{k=1}^nk^3=\left(\frac{n(n+1)}{2}\right)^2, \, \, \, \forall n\in\mathbb N .$$ I'm ...
DIEGO JAURE's user avatar
6 votes
1 answer

Has reinforcement learning been used to prove mathematical theorems?

Coq exists, and there are other similar projects out there. Further, Reinforcement Learning has made splashes in the domain of playing games (a la Deepmind & OpenAI and other less well-known ...
Frank Bryce's user avatar
2 votes
1 answer

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

From what I've figured (a) converting mathematical theorems and proofs from English to formal logic is a straightforward job for mathematicians with sufficient background, except that it takes time. ...
ghosts_in_the_code's user avatar
1 vote
1 answer

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

I would love to know if an AI model could come up with certain theories of the old like Pythagoras' theorem, Euclid's formulations, Newton's gravity, Einstein's theories if provided and trained with ...
katipra's user avatar
  • 41
1 vote
1 answer

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

When will it be possible to give a computer program a bunch of assumptions and ask it if a certain statement is true or false, giving a proof or a counterexample respectively?
Siddhartha's user avatar
30 votes
4 answers

Can neural networks be used to prove conjectures?

Imagine I have a list (in a computer-readable form) of all problems (or statements) and proofs that math relies on. Could I train a neural network in such a way that, for example, I enter a problem ...
Max Mustermann Junior's user avatar
1 vote
1 answer

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

Being by no means an expert in the field, I do however know of solvers such as Z3 that can generate a correct program, provided you can express your constraints as a set of logical rules, such as here....
Raoul's user avatar
  • 121