LARGE LANGUAGE MODEL VERIFICATION

Application No. 18/541,988

• Filed: Dec 15, 2023
• Examiner: EL-HAGE HASSAN, ABDALLAH A
• Assignee: Amazon Technologies Inc.
• OA Round: 1 (Non-Final)

Office Action

DETAILED ACTION
Notice of Pre-AIA or AIA Status
The present application, filed on or after March 16, 2013 is being examined under the first inventor to file provisions of the AIA .
Status of the Application
This action is a first action on the merits in response to the application filed on 12/15/2023.
Status of Claims
Claims 1-20 filed on 12/15/2023 are currently pending and have been examined in this application.
Information Disclosure Statement
The information disclosure statements (IDS) submitted on 12/19/2024 and on 07/02/20235 are in compliance with the provisions of 37 CFR 1.97. Accordingly, the information disclosure statements are being considered by the examiner.
Claim Rejections - 35 USC § 103
The following is a quotation of 35 U.S.C. 103 which forms the basis for all obviousness rejections set forth in this Office action:
A patent for a claimed invention may not be obtained, notwithstanding that the claimed invention is not identically disclosed as set forth in section 102, if the differences between the claimed invention and the prior art are such that the claimed invention as a whole would have been obvious before the effective filing date of the claimed invention to a person having ordinary skill in the art to which the claimed invention pertains. Patentability shall not be negated by the manner in which the invention was made.

The factual inquiries set forth in Graham v. John Deere Co., 383 U.S. 1, 148 USPQ 459 (1966), that are applied for establishing a background for determining obviousness under 35 U.S.C. 103 are summarized as follows:
1. Determining the scope and contents of the prior art.
2. Ascertaining the differences between the prior art and the claims at issue.
3. Resolving the level of ordinary skill in the pertinent art.
4. Considering objective evidence present in the application indicating obviousness or non-obviousness.
In the event the determination of the status of the application as subject to AIA 35 U.S.C. 102 and 103 (or as subject to pre-AIA 35 U.S.C. 102 and 103) is incorrect, any correction of the statutory basis for the rejection will not be considered a new ground of rejection if the prior art relied upon, and the rationale supporting the rejection, would be the same under either status.
Claims 1-20 are rejected under 35 U.S.C. 103 as being un-patentable over Sumit Kumar Jha (NEURO SYMBOLIC REASONING FOR PLANNING: COUNTEREXAMPLE GUIDED INDUCTIVE SYNTHESIS USING LARGE LANGUAGE MODELS AND SATISFIABILITY SOLVING), Computer Science Department, Florida International University, 28 Sep 2023.
Regarding claim 1. Sumit teaches A method comprising: converting a set of natural language text documents into a domain logic model, the domain logic model comprising a set of first-order logic formulas; enumerating a set of models of a first-order logic formula of the set of first-order logic formulas of the domain logic model; minimizing a particular model of the set of models to yield a minimized model that replaces the particular model in the set of models; translating the set of models comprising the minimized model to a set of natural-language texts; providing the set of natural-language texts in a graphical user interface; obtaining a conversational text, the conversational text comprising a query of a first large language model and an answer generated by the first large language model in response to the query; [Sumit, Abstract teaches “Our method allows the user to communicate the planning problem in natural language; even the formulation of queries to SMT solvers is automatically generated from natural language. Thus, the proposed technique can enable non-expert users to describe their problems in natural language, and the combination of LLMs and SMT solvers can produce provably correct solutions” wherein converting a set of natural language text documents into a domain logic model and minimizing model to a set of natural-language texts. Wherein formulation of queries to SMT solvers is automatically generated from natural language is equivalent to providing the set of natural-language texts in a graphical user interface; obtaining a conversational text, the conversational text comprising a query of a first large language model and an answer generated by the first large language model in response to the query. Also see Abstract “Generative large language models (LLMs) with instruct training such as GPT-4 can follow human provided instruction prompts and generate human-like responses to these prompts”]
Sumit does not specifically teach, however, using the conversational text to obtain a first-order logic translation of the answer from a second large language model; determining whether the first-order logic translation of the answer is valid based on using a satisfiability modulo theories solver to determine whether a first query comprising a negation of the first-order logic translation of the answer is unsatisfiable; and determining whether the first-order logic translation of the answer is invalid based on using a satisfiability modulo theories solver to determine whether a second query comprising the first-order logic translation of the answer is unsatisfiable; and outputting an indication of whether the answer is valid, invalid, or neither valid nor invalid to a graphical user interface, a database, or a report, relate to steps of an algorithm to determine if text predicted by one mathematical model (i.e. an LLM) are considered valid according to verification rules defines in terms of another mathematical model (i.e. a theorem prover) using a formal mathematical representation of the answer (first-order logic) which has been generated by a mathematical model. Predicting text (i.e. as an answer or a continuation of a conversation) does not serve a technical purpose since the effect of the predicted text only manifests itself in the mind of the person looking at the text. The distinguishing algorithm does not serve a specific technical purpose and cannot contribute to the invention's technical character because the distinguishing algorithm can be executed on a wide variety of general-purpose hardware. As a result, skilled person in the art would implement the distinguishing algorithm in the context of closest prior art Sumit and arrive at the subject matter of claim 1 without exercising any inventive skill.
Regarding claim 2. further comprising: using the conversational text to obtain a plurality of first-order logic translations of the answer from one or more large language models; wherein the plurality of first-order logic translations comprises the first-order logic translation; and wherein the one or more large language models comprises the first large language model; partitioning the plurality of first-order logic translations of the answer based on logical equivalence with respect to the set of first order logical formulas of the domain logic model into one or more non-overlapping sets of the plurality of first-order logic translations; and selecting the first-order logical translation of the answer from the one or more non-overlapping sets of the plurality of first-order logical translations. The features of claim 2 are directed to further mathematical processing of converting text to first order logic and converting text to produce predicted text do not add technical contribution to the subject matter of claim 1.
Regarding claim 3. Sumit teaches translating the set of natural-language statements into a plurality of first-order logic formulas; and using a satisfiability modulo theories solver to extract an unsatisfiable core formula from the plurality of first-order logic formulas; translating the unsatisfiable core formula to a natura-language text; and providing the natural-language text in a graphical user interface [Sumit, Abstract teaches “We posit that we can use the satisfiability modulo theory (SMT) solvers as deductive reasoning engines to analyze the generated solutions from the LLMs, produce counterexamples when the solutions are incorrect” wherein extract an unsatisfiable core formula from the plurality of first-order logic formulas].
Regarding claim 4, the claim recites analogous limitations to claim 1 above, and is therefore rejected on the same premise. Claim 1 is a method claim while claim 4 is directed to a system which is anticipated by Sumit Abstract.
Regarding claims 5-6. further comprising: using the conversational text to obtain a plurality of first-order logic translations of the answer from one or more large language models; wherein the plurality of first-order logic translations comprises the first-order logic translation; and wherein the one or more large language models comprises the first large language model; partitioning the plurality of first-order logic translations of the answer based on logical equivalence with respect to the set of first order logical formulas of the domain logic model into one or more non-overlapping sets of the plurality of first-order logic translations; and selecting the first-order logical translation of the answer from the one or more non-overlapping sets of the plurality of first-order logical translations. wherein selecting the first-order logical translation of the answer from the one or more non-overlapping sets of the plurality of first-order logical translations is based on: identifying a non-overlapping set of the one or more non-overlapping sets that comprises all of the plurality of first-order logic translations; and selecting the first-order logic translation from the non-overlapping set. Converting the text of documents into first order logic is a further step in a mathematical algorithm for text prediction which does not make a further technical contribution. Processing mathematical models and using the outcome to generate text to be presented does not serve a technical purpose and does not make a further technical contribution to the claimed invention.
Regarding claims 7-10. The method of claim 5, wherein selecting the first-order logical translation of the answer from the one or more non-overlapping sets of the plurality of first-order logical translations is based on: identifying a non-overlapping set of the one or more non-overlapping sets that comprises more than half of the plurality of first-order logic translations; and selecting the first-order logic translation from the non-overlapping set. Further comprising: converting a set of natural language text documents into the set of first-order logic formulas of the domain logic model. Further comprising: enumerating a set of models of a first-order logic formula of the set of first-order logic formulas of the domain logic model; minimizing a particular model of the set of models to yield a minimized model that replaces the particular model in the set of models; translating the set of models comprising the minimized model to a set of natural-language texts; and providing the set of natural-language texts in a graphical user interface. Further comprising: translating a set of natural-language statements into a plurality of first-order logic formulas; and using an automated theorem prover to extract an unsatisfiable core formula from the plurality of first-order logic formulas; translating the unsatisfiable core formula to a natura-language text; and providing the natural-language text in a graphical user interface. The limitations in claim 7-10 are further directed to mathematical processing of text to produce predicted text and are not considered to make a further technical contribution.
Regarding claims 11-13. wherein: the first query comprises is unsatisfiable; the second query is satisfiable; the indication output indicates that the answer is valid; further comprising: the first query is satisfiable; the second query is unsatisfiable; the indication output indicates that the answer is invalid; further comprising: the first query is satisfiable; the second query is satisfiable; and the indication output indicates that the answer is neither valid nor invalid. The limitations in claim 11-13 are further directed to mathematical processing of text to produce present predicted text are not considered to make a further technical contribution.
Regarding claim 14, the claim recites analogous limitations to claim 1 above, and is therefore rejected on the same premise. Claim 1 is a method claim while claim 14 is directed to a system which is anticipated by Sumit Abstract.
Regarding claims 15-20, claims 15-20 recite substantially similar limitations as claim 2 and 6-10, respectively; therefore, claims 15-20 are rejected with the same rationale, reasoning, and motivation provided above for claims 2 and 6-10.
Conclusion
The following prior arts made of record and not relied upon are considered pertinent to applicant's disclosure.
Sheinin (US 12086559 B2) teaches A computer system extracts clauses using machine translation. An input sentence in a source language is translated into a translated sentence in a target language using a trained machine translation model, wherein the trained machine translation model inserts a grammatical indicator into a position of the translated sentence that identifies a dependent clause. The input sentence and the translated sentence are aligned to determine a position in the input sentence that corresponds to the position of the grammatical indicator in the translated sentence. The dependent clause is extracted, in the source language, from the input sentence based on the determined position in the input sentence. Embodiments of the present invention further include a method and program product for clause extraction using machine translation in substantially the same manner described above
Bayless et al. (US 20250111192 A1) teaches A computer-implemented method for a knowledge-graph service to generate a knowledge graph using a large language model (LLM), the computer-implemented method comprising: generating a formal-language query that is usable to retrieve a formal-language answer from the knowledge graph; querying, by a query engine associated with the knowledge-graph service, the knowledge graph to identify the answer to the formal-language query; determining, by the query engine, that the formal-language answer to the formal-language query is not included in the knowledge graph; identifying a portion of the knowledge graph that includes information that is relevant to the formal-language query; generating a prompt for the LLM to determine the formal-language answer to the formal-language query, the prompt including the portion of the knowledge graph and the formal-language query; providing the LLM with the prompt to determine the formal-language answer to the formal-language query; receiving the formal-language answer as an output from the LLM; and adding, to the knowledge graph, the formal-language answer for the formal-language query
Any inquiry concerning this communication from the examiner should be directed to Abdallah El-Hagehassan whose contact information is [phone] and [e-mail] The examiner can normally be reached on Monday- Friday 8 am to 5 pm.
If attempts to reach the examiner by telephone are unsuccessful, the examiner’s supervisor, Rutao Wu can be reached on [phone]. The fax phone number for the organization where this application or proceeding is assigned is [phone].
Information regarding the status of an application may be obtained from the patent application information retrieval (PAIR) system. Status information of published applications may be obtained from either private PAIR or public PAIR. Status information of unpublished applications is available through private PAIR only. For more information about the PAIR system, see http://pair-direct.uspto.gov. Should you have any questions on access to the private PAIR system, contact the electronic business center (EBC) at [phone] (toll-free). If you would like assistance from a USPTO customer service representative or access to the automated information system, call [phone] (in US or Canada) or [phone].
/ABDALLAH A EL-HAGE HASSAN/
Primary Examiner, Art Unit 3623

Prosecution Timeline

• Dec 15, 2023: Application Filed
• Jun 03, 2026: Non-Final Rejection mailed — §103 (current)