Verifiable logical reasoning using GenAI

1 . A computer-implemented method comprising:

accessing a prompt that is associated with a logical reasoning problem;

generating one or more logical steps of a logical response based on the prompt by using a generative artificial intelligence (GenAI) model;

for each of the one or more logical steps of the logical response:

querying one or more theorem solvers using the logical response and the logical reasoning problem, wherein the one or more theorem solvers include proof checkers and theorem provers;

processing, using parallel execution of the proof checkers and the theorem provers, the one or more logical steps of the logical response to verify axioms or rules associated with each logical step of the one or more logical steps;

receiving, in response to the query, one or more feedback from the one or more theorem solvers corresponding to the logical response of the logical reasoning problem; and

modifying, in response to the one or more feedback, the logical response by regenerating the one or more logical steps:

determining that the logical response is complete and verified from the one or more theorem solvers; and

outputting, in response to determining that the logical response is complete and verified, the logical response on a user interface.

2 . The computer-implemented method of claim 1 , wherein the one or more theorem solvers include satisfiability (SAT) based theorem solvers.

3 . The computer-implemented method of claim 1 , wherein the one or more theorem solvers further include proof checkers.

4 . The computer-implemented method of claim 1 , wherein the prompt is generated by a user using the user interface.

5 . The computer-implemented method of claim 1 , wherein the GenAI model includes a retrieval-augmented generation (RAG) model, a fine-tuned transformer model, or a domain-specific model that is trained on domain-specific data.

6 . The computer-implemented method of claim 1 , wherein the one or more feedback from the one or more theorem solvers includes whether a logical step of the logical response is reachable based on a set of premises (or justification) and/or whether rules or axioms of natural deduction are correctly utilized.

7 . The computer-implemented method of claim 1 , wherein querying the one or more theorem solvers using the logical response and the logical reasoning problem further includes:

generating, for each of the one or more theorem solvers and based on the logical response, a set of logical statements, wherein the set of logical statements are in a format that is understandable by a corresponding theorem solver.

8 . A system comprising:

one or more data processors; and

a non-transitory computer readable storage medium containing instructions which, when executed on the one or more data processors, cause the one or more data processors to perform a set of operations including:

accessing a prompt that is associated with a logical reasoning problem;

generating one or more logical steps of a logical response based on the prompt by using a generative artificial intelligence (GenAI) model;

for each of the one or more logical steps of the logical response:

querying one or more theorem solvers using the logical response and the logical reasoning problem, wherein the one or more theorem solvers include proof checkers and theorem provers:

processing, using parallel execution of the proof checkers and the theorem provers, the one or more logical steps of the logical response to verify axioms or rules associated with each logical step of the one or more logical steps:

receiving, in response to the query, one or more feedback from the one or more theorem solvers corresponding to the logical response of the logical reasoning problem; and

modifying, in response to the one or more feedback, the logical response by regenerating the one or more logical steps;

determining that the logical response is complete and verified from the one or more theorem solvers; and

outputting, in response to determining that the logical response is complete and verified, the logical response on a user interface.

9 . The system of claim 8 , wherein the one or more theorem solvers include satisfiability (SAT) based theorem solvers.

10 . The system of claim 8 , wherein the one or more theorem solvers further include proof checkers.

11 . The system of claim 8 , wherein the prompt is generated by a user using the user interface.

12 . The system of claim 8 , wherein the GenAI model includes a retrieval-augmented generation (RAG) model, a fine-tuned transformer model, or a domain-specific model that is trained on domain-specific data.

13 . The system of claim 8 , wherein the one or more feedback from the one or more theorem solvers includes whether a logical step of the logical response is reachable based on a set of premises (or justification) and/or whether rules or axioms of natural deduction are correctly utilized.

14 . The system of claim 8 , wherein querying the one or more theorem solvers using the logical response and the logical reasoning problem further includes:

generating, for each of the one or more theorem solvers and based on the logical response, a set of logical statements, wherein the set of logical statements are in a format that is understandable by a corresponding theorem solver.

15 . A non-transitory machine-readable storage medium storing a computer-program product tangibly including instructions configured to cause one or more data processors to:

access, a prompt that is associated with a logical reasoning problem;

generate, one or more logical steps of a logical response based on the prompt by using a generative artificial intelligence (GenAI) model;

for each of the one or more logical steps of the logical response:

querying, one or more theorem solvers using the logical response and the logical reasoning problem; wherein the one or more theorem solvers include proof checkers and theorem provers;

processing, using parallel execution of the proof checkers and the theorem provers, the one or more logical steps of the logical response to verify axioms or rules associated with each logical step of the one or more logical steps;

receiving, in response to the query, one or more feedback from the one or more theorem solvers corresponding to the logical response of the logical reasoning problem; and

modifying, in response to the one or more feedback, the logical response by regenerating the one or more logical steps:

determine that the logical response is complete and verified from the one or more theorem solvers; and

output, in response to determining that the logical response is complete and verified, the logical response on a user interface.

16 . The computer-program product of claim 15 , wherein the one or more theorem solvers include satisfiability (SAT) based theorem solvers.

17 . The computer-program product of claim 15 , wherein the one or more theorem solvers further include proof checkers.

18 . The computer-program product of claim 15 , wherein the prompt is generated by a user using the user interface.

19 . The computer-program product of claim 15 , wherein the GenAI model includes a retrieval-augmented generation (RAG) model, a fine-tuned transformer model, or a domain-specific model that is trained on domain-specific data.

20 . The computer-program product of claim 15 , wherein the one or more feedback from the one or more theorem solvers includes whether a logical step of the logical response is reachable based on a set of premises (or justification) and/or whether rules or axioms of natural deduction are correctly utilized.