US-20260127386-A1 - LANGUAGE MODEL THEORY SOLVERS

US20260127386A1US 20260127386 A1US20260127386 A1US 20260127386A1US-20260127386-A1

Abstract

Techniques for processing a natural language query using an SMT solver that includes an LLM. The LLM processes the query text to formalize constraint text into pseudo code, which is processed by an SAT solver to determine logical atoms and propositional model for solving the query. The LLM then acts as a theory solver within the SMT solver to process the logical atoms and determine a valid solution for the natural language query.

Inventors

Umberto Maria Tomasini
Luca Zancato
Alessandro Achille
Stefano Soatto
Aditya Sharad Golatkar
Greg Ver Steeg
Wei Xia

Assignees

AMAZON TECHNOLOGIES, INC.

Dates

Publication Date: 20260507
Application Date: 20241213

Claims (20)

1 . A computer-implemented method comprising: receiving a natural language query requesting a first output; processing the natural language query using a large language model (LLM) to determine: a first logical representation of a first constraint of the natural language query, the first constraint corresponding to a first variable, and a second logical representation of a second constraint of the natural language query, the second constraint corresponding to a second variable; processing the first logical representation and the second logical representation to determine that a potential solution to the natural language query exists that satisfies both the first constraint and the second constraint; determining a logical statement representing the natural language query including the first constraint and the second constraint, wherein the logical statement comprises the first variable and the second variable; processing the logical statement to determine a first natural language representation of the logical statement; determining a first prompt including the first natural language representation; and processing the first prompt using the LLM to determine output text responsive to the natural language query, the output text including a first value for the first variable and a second value for the second variable.
2 . The computer-implemented method of claim 1 , wherein: determining the logical statement comprises processing the first logical representation and the second logical representation using a satisfiability modulo theory solver component to determine the logical statement.
3 . The computer-implemented method of claim 2 , wherein: determining that a potential solution to the natural language query exists comprises processing the first logical representation and the second logical representation using the satisfiability modulo theory solver component to determine that at least one potential first value exists for the first variable and at least one potential second value exists for the second variable such that the logical statement is satisfied.
4 . The computer-implemented method of claim 1 , further comprising: determining a domain corresponding to the natural language query; determining first data corresponding to the domain, the first data relevant for responding to the natural language query; and determining the first prompt further including a natural language representation of the first data.
5 . A computer-implemented method comprising: receiving a natural language input requesting a first output based on a first constraint; determining a first conditional statement corresponding to the first constraint and a first variable associated with the first constraint; determining a first prompt including the natural language input, the first conditional statement and a first request to determine at least a first value for the first variable, wherein the first value satisfies the first conditional statement; processing, using a first language model, the first prompt to generate at least the first value; and causing presentation of the first value in response to the natural language input.
6 . The computer-implemented method of claim 5 , further comprising: determining a second prompt including the natural language input and a second request to generate at least one conditional statement for determining at least one value for the first output; and processing, using a second language model, the second prompt to generate the first conditional statement.
7 . The computer-implemented method of claim 5 , further comprising: determining a second prompt including the natural language input, and a second request to generate at least one variable relevant for determining at least one value for the first output based on the first constraint; and processing, using a second language model, the second prompt to generate the first variable.
8 . The computer-implemented method of claim 5 , further comprising: determining that the natural language input corresponds to a type of conditional statement; and based on the natural language input corresponding to the type of conditional statement, using a component configured to process a constraint satisfaction problem to determine the first conditional statement.
9 . The computer-implemented method of claim 5 , further comprising: processing, using the first language model, the first prompt to generate at least the first value and a confidence value corresponding to the first value; based on the confidence value satisfying a condition, determining a second conditional statement corresponding to the first constraint and the first variable; determining a second prompt including the natural language input, the second conditional statement, the first value and a second request to determine at least a second value for the first variable, wherein the second value is different than the first value; and processing, using the first language model, the second prompt to generate at least the second value.
10 . The computer-implemented method of claim 5 , further comprising: determining a domain corresponding to the natural language input; determining data corresponding to the domain and relevant for responding to the natural language input; and determining at least the first variable based on the data.
11 . The computer-implemented method of claim 5 , further comprising: determining context data corresponding to the natural language input; and determining the first conditional statement based on the context data.
12 . The computer-implemented method of claim 5 , further comprising: determining data relevant for processing the natural language input; and determining the first prompt to further include the data.
13 . A system comprising: at least one processor; and at least one memory including instructions that, when executed by the at least one processor, cause the system to: receive a natural language input requesting a first output based on a first constraint; determine a first conditional statement corresponding to the first constraint and a first variable associated with the first constraint; determine a first prompt including the natural language input, the first conditional statement and a first request to determine at least a first value for the first variable, wherein the first value satisfies the first conditional statement; process, using a first language model, the first prompt to generate at least the first value; and cause presentation of the first value in response to the natural language input.
14 . The system of claim 13 , wherein the at least one memory includes further instructions that, when executed by the at least one processor, further cause the system to: determine a second prompt including the natural language input and a second request to generate at least one conditional statement for determining at least one value for the first output; and process, using a second language model, the second prompt to generate the first conditional statement.
15 . The system of claim 13 , wherein the at least one memory includes further instructions that, when executed by the at least one processor, further cause the system to: determine a second prompt including the natural language input, and a second request to generate at least one variable relevant for determining at least one value for the first output based on the first constraint; and process, using a second language model, the second prompt to generate the first variable.
16 . The system of claim 13 , wherein the at least one memory includes further instructions that, when executed by the at least one processor, further cause the system to: determine that the natural language input corresponds to a type of conditional statement; and based on the natural language input corresponding to the type of conditional statement, use a component configured to process a constraint satisfaction problem to determine the first conditional statement.
17 . The system of claim 13 , wherein the at least one memory includes further instructions that, when executed by the at least one processor, further cause the system to: process, using the first language model, the first prompt to generate at least the first value and a confidence value corresponding to the first value; based on the confidence value satisfying a condition, determine a second conditional statement corresponding to the first constraint and the first variable; determine a second prompt including the natural language input, the second conditional statement, the first value and a second request to determine at least a second value for the first variable, wherein the second value is different than the first value; and process, using the first language model, the second prompt to generate at least the second value.
18 . The system of claim 13 , wherein the at least one memory includes further instructions that, when executed by the at least one processor, further cause the system to: determine a domain corresponding to the natural language input; determine data corresponding to the domain and relevant for responding to the natural language input; and determine at least the first variable based on the data.
19 . The system of claim 13 , wherein the at least one memory includes further instructions that, when executed by the at least one processor, further cause the system to: determine context data corresponding to the natural language input; and determine the first conditional statement based on the context data.
20 . The system of claim 13 , wherein the at least one memory includes further instructions that, when executed by the at least one processor, further cause the system to: determine data relevant for processing the natural language input; and determine the first prompt to further include the data.

Description

CROSS-REFERENCE TO RELATED APPLICATIONS This application claims the benefit of priority under 35 U.S.C. § 119 (e) to Provisional U.S. Application No. 63/715,193, filed Nov. 1, 2024, entitled “LANGUAGE MODEL THEORY SOLVERS”, in the names of Umberto Maria Tomasini, et al. The contents of the foregoing application is hereby incorporated herein by reference in its entirety. BACKGROUND A solver is a software engine that can apply logical reasoning to answer a question. For example, a solver may determine whether a given formula or logical expression is satisfiable (“SAT”) or unsatisfiable (“UNSAT”). In a Boolean satisfiability problem, a logical expression is said to be SAT if the variables of the logical expression can be replaced by the values TRUE or FALSE in such a way that the logical expression equates to TRUE; if not, the problem is UNSAT. In mathematical logic, a formula is said to be SAT if values (e.g., numbers) can be assigned to the variables and/or interpretations assigned to functions and constants to make the formula TRUE. Multiple solvers may be implemented in a portfolio such that a central manager can send the same problem to multiple solvers. The solvers may attempt to solve the problem and return a result to the central manager, which may send the result to the requesting system or user. BRIEF DESCRIPTION OF THE DRAWINGS The detailed description of certain embodiments of the invention are understood with reference to the following figures: FIGS. 1A-1B illustrate a system and a method for language model theory solvers, according to an embodiment. FIG. 2 is a flowchart of a sub-method for using a user input and a language model generated answer to determine one or more input variable constraints and one or more output variable constraints, according to an embodiment. FIG. 3 is a flowchart of a sub-method to generate sets of formal logic constraints, according to an embodiment. FIG. 4 is a flowchart of a sub-method for selecting a particular formal logic constraint(s) for validating the language model generated answer to a user input, according to an embodiment. FIG. 5 is a flowchart of a sub-method for performing a satisfiability check of the particular formal logic constraint(s) under the one or more constraints, according to an embodiment. FIG. 6 is a flowchart of a sub-method for using a language model as a theory solver, according to an embodiment. FIG. 7 is a conceptual diagram illustrating example components of a system configured to use a language model to determine a response to a user input, according to embodiments of the present disclosure. FIG. 8 is a conceptual diagram illustrating example processing of the system configured to use a language model, according to embodiments of the present disclosure. FIG. 9 illustrates an example multi-tenant provider network environment in which the techniques disclosed herein for language model theory solvers may be implemented. FIG. 10 is a block diagram of an example multi-tenant provider network that provides a storage service and a hardware virtualization service to customers and in which the techniques disclosed herein for language model theory solvers may be implemented. FIG. 11 illustrates an example of a programmable electronic device that processes and manipulates data to perform tasks and calculations disclosed herein for language model theory solvers. FIG. 12 illustrates an example transformer model architecture that may be used in an implementation of a language model, according to some embodiments of the present disclosure. DETAILED DESCRIPTION Some techniques to perform automated reasoning on language-based tasks employ formal solvers. These solvers may require a formalization of the task, which can be rather cumbersome and sometimes unfeasible for natural language queries. A solver is a software engine that can apply logical reasoning to answer a question. A solver may implement one or more algorithms to solve a problem such as a Boolean satisfiability problem. An algorithm may specify a search procedure for exploring a space of possible variable assignments. In some cases, the algorithm may reduce the search space by using a backtracking and/or backjumping technique for building candidate solutions and abandoning a candidate if the candidate cannot possibly be completed to a valid solution, where backtracking may refer to going up one level in the search tree when the candidate is eliminated, and backjumping may refer to going up two or more levels. Solver types in common usage may include local-search, conflict-driven clause learning (CDCL), and look-ahead. Solvers may be used in, for example, mathematics to assist in proving mathematical theorems, software verification to check whether a program performs to specification, hardware verification to check whether a finite-state system performs to specification, and operations research to solve optimization and scheduling problems. Solvers may be implemented in cloud computing archi