Large language model verification — Amazon Technologies, Inc. (US20250200392A1)

ABSTRACT

Abstract

Verifying large language model responses involves obtaining a query and its corresponding answer from a large language model. This conversational text is then fed into a second large language model, which translates the answer into first-order logic. The verification process uses an automated theorem prover. It checks the validity of this logic translation by determining the unsatisfiability of two scenarios: one where the negation of the logic translation and domain-specific logic formulas are combined, and another where the logic translation itself is combined with these formulas. Based on this analysis, the theorem prover ascertains whether the translated answer is valid, invalid, or neither. The final step is communicating this verification status through an appropriate output medium, such as a graphical user interface, a database, or a report, providing a structured and methodical approach to assessing the accuracy and reliability of language model responses.

Description

BACKGROUND

A large language model, or “LLM,” is a type of artificial intelligence system designed to understand, generate, and interact with human language. LLMs are based on a neural network architecture known as a transformer. Transformers enable LLMs to analyze and process vast amounts of text data. An LLM is “trained” through a process called machine learning, where a large corpus of text from various sources is input to the model. During training, the model learns patterns, language structures, and nuances, allowing it to generate coherent, contextually relevant responses. This learning process involves adjusting the internal parameters of the model to minimize the difference between its outputs and the expected results. Once trained, the model can perform a wide range of language-related tasks, such as answering questions, translating languages, summarizing texts, and creating content.

LLMs are known to “hallucinate.” Large Language Model (LLM) hallucinations refer to instances where these models generate incorrect, misleading, or nonsensical information while appearing confident and coherent. This phenomenon arises because LLMs don't truly “understand” content in the way humans do. Instead, they generate responses based on patterns learned from their training data. When an LLM encounters a query that falls outside its training or is ambiguous, it can produce responses that seem plausible but are factually inaccurate or completely fabricated. This issue is compounded by the model's lack of real-world awareness and inability to access or verify current information beyond its training cutoff. LLM hallucinations pose a challenge in applications where accuracy is crucial, as the model's authoritative tone can be misleading.

BRIEF DESCRIPTION OF THE DRAWINGS

The detailed description of certain embodiments of the invention below may be understood by reference to the following figures:

FIG. 1 illustrates a Large Language Model (LLM) verifier system that enhances the accuracy of the outputs of a vanilla LLM and includes a domain model creator subsystem and an answer verifier subsystem.

FIG. 2 illustrates the domain model creator subsystem and detailed operation thereof.

FIG. 3 illustrates the answer verifier subsystem and detailed operation thereof.

FIG. 4 illustrates an example conversation between a user and a large language model (LLM) agent.

FIG. 5 is flowchart of a method for selecting a desired translation of natural language to logic.

FIG. 6 illustrates three procedures implementing a scenario generation technique.

FIG. 7 is a flowchart of an enumerate models procedure of the scenario generation technique.

FIG. 8 is a flowchart of a minimize model procedure of the scenario generation technique.

FIG. 9 illustrates an example multi-tenant provider network environment in which the techniques disclosed herein for large language model (LLM) verification 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 large language model (LLM) verification 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 large language model (LLM) verification.

DETAILED DESCRIPTION

Disclosed herein are systems, methods, and non-transitory computer-readable media (generally, “techniques”) for large language model (LLM) verification. The techniques include verifying large language model responses by obtaining a query and its corresponding answer from a large language model. This conversational text is then fed into a second large language model, which translates the answer into first-order logic. The verification process uses an automated theorem prover. It checks the validity of this logic translation by determining the unsatisfiability of two scenarios: one where the negation of the logic translation and domain-specific logic formulas are combined, and another where the logic translation itself is combined with these formulas. Based on this analysis, the theorem prover ascertains whether the translated answer is valid, invalid, or neither. The final step is communicating this verification status through an appropriate output medium, such as a graphical user interface, a database, or a report, providing a structured and methodical approach to assessing the accuracy and reliability of language model responses.

The present disclosure includes a structured approach to verify responses generated by large language models. It begins by collecting a query and its answer from a primary large language model. This conversational exchange is then processed by a secondary large language model that translates the answer into first-order logic. This translation forms the basis of the verification process, which is conducted using an automated theorem prover. The theorem prover evaluates the logical validity by examining two distinct scenarios. In the first scenario, it checks the unsatisfiability of the negated logic translation in conjunction with domain-specific logic formulas. In the second, it assesses the unsatisfiability of the direct logic translation combined with the same set of formulas. This dual analysis allows the theorem prover to determine if the translated answer is valid, invalid, or indeterminate. Finally, the outcome of this verification is communicated through an output medium like a graphical user interface, a database, or a report. This approach ensures a rigorous and systematic evaluation of the accuracy and reliability of answers provided by language models, enhancing their credibility and utility in various applications.

As referenced in this description, large language models (LLMs) are advanced AI systems characterized by their deep learning techniques and vast training datasets. They are built using neural networks, specifically a type of architecture known as the Transformer, which is highly efficient in processing and generating sequential data like text. The “large” in their name refers not only to the size of their training data, encompassing diverse text sources, but also to the complexity of their neural network, often containing billions or even trillions of parameters. These parameters are fine-tuned during the training process, allowing the model to learn intricate patterns and nuances of language, including grammar, context, idioms, and even styles of writing. A useful feature of large language models is their ability to handle and generate contextually relevant text, making them adept at tasks like answering questions, composing texts, and translating languages. They achieve this through a mechanism known as attention, which enables the model to weigh different parts of the input text differently, thereby focusing on the most relevant parts to generate coherent and context-aware outputs.

In this disclosure, familiarity with first-order logic is assumed. Formulas of a first-order language L are built using predicate symbols, function symbols, and constants from some given alphabet together with logical connectives, quantifiers, and variables. An expression (e.g., a term, literal, formula, etc.) is ground if it contains no variables. A propositional assignment is a mapping from ground atoms to the truth values 1 (true) and 0 (false). Accordingly, a set of ground formulas is propositionally satisfiable if there exists a propositional assignment that satisfies all formulas in the set under the usual semantics for the logical connectives. Assignments can be written as sequences of literals where a positive (negative) polarity of a literal indicates that the truth value 1 (0, respectively) is assigned to the literal's atom.

As referenced in this description, automated theorem provers are sophisticated computational tools designed to assist in or fully automate the process of proving mathematical theorems. At their core, they rely on formal logic and various algorithms to deduce truths from a set of axioms and rules of inference. These systems are built upon a foundation of symbolic logic, primarily using first-order or higher-order logic. The technical prowess of these provers lies in their ability to methodically explore the vast space of potential proofs, which is often too large and complex for manual navigation. They employ various strategies like resolution, term rewriting, and decision procedures for specific theories to efficiently manage this exploration. Some provers specialize in certain domains by incorporating relevant mathematical theories (like arithmetic or geometry), thereby enhancing their effectiveness in those areas. A useful aspect of automated theorem provers is their use of formal languages to ensure precision and unambiguity in representing mathematical statements. This precision is crucial for correctly interpreting the theorems and proofs.

As referenced in this description, an SMT (Satisfiability Modulo Theories) solver, as a type of automated theorem prover, is distinguished by its ability to determine the satisfiability of logical formulas within various mathematical theories. Technically, it extends the capabilities of a basic SAT (Boolean satisfiability) solver by incorporating domain-specific knowledge from theories like linear arithmetic, real numbers, bit-vectors, arrays, and function symbols with uninterpreted functions. This integration allows SMT solvers to handle a more expressive set of logical formulas than those limited to propositional logic.

A useful characteristic of SMT solvers is their use of decision procedures or theory solvers, specialized algorithms designed to handle formulas within a specific theory. These solvers can efficiently reason about the satisfiability of formulas by considering the semantics of the theories they involve. An SMT solver typically integrates multiple theory solvers, enabling it to work with formulas that span several theories simultaneously. This feature makes SMT solvers incredibly versatile and powerful, especially in applications like software verification, model checking, and constraint solving, where complex logical relationships need to be analyzed.

The effectiveness of an SMT solver largely depends on its ability to balance the generality of handling multiple theories with the efficiency of solving instances quickly. It achieves this through techniques like backtracking, theory combination, and heuristic-guided search.

As referenced in this description, SMT-LIB is a standard library for Satisfiability Modulo Theories (SMT), designed to facilitate the development, testing, and comparison of SMT solvers. It primarily consists of a large and growing collection of benchmark problems, expressed in a standardized input language. This language, also called SMT-LIB language, is a formal, computer-readable language specifically crafted for describing problems in various SMT theories like linear integer arithmetic, real arithmetic, bit-vectors, arrays, and uninterpreted functions. The language is rigorously defined, ensuring consistency and uniformity in the way SMT problems are specified, which is crucial for fair and accurate comparisons among different solvers.

One of the useful technical characteristics of SMT-LIB is its structured, yet flexible format. It allows for the clear definition of logic theories, the declaration of functions and types, and the specification of assertions (formulas) that need to be satisfied. This structured approach enables SMT solvers to parse and process these benchmarks uniformly. SMT-LIB also provides a common set of commands for solver interaction, making it easier to control and communicate with SMT solvers in a standardized way.

Example LLM Verification System

Referring now to FIG. 1 , a Large Language Model (LLM) verifier system 100 enhances the accuracy of the outputs of a “vanilla” LLM 102 . The vanilla LLM 102 can be a standard, general-purpose LLM used for basic language processing and interaction tasks. However, the techniques described herein can be implemented with a special-purpose LLM as a substitute for the vanilla LLM 102 where the special-purpose LLM is based on a vanilla LLM or a foundational LLM that has been fine-tuned or trained for a domain-specific task using, for example, retrieval augmented generation (RAG) techniques or other suitable LLM fine-tuning techniques.

The enhancement in accuracy is achieved by verifying the truthfulness of the key information that the vanilla LLM 102 provides in response to customer queries. The LLM verifier system 100 is designed with multiple interconnected networks, each contributing to this verification process. A multi-tenant provider network 104 , which includes an answer verifier system 106 , or “answer verifier 106 ,” acts as a primary checkpoint for validating responses. The answer verifier system 106 cross-references the vanilla LLM 102 's answers with trusted sources or logical framewor

BACKGROUND

A large language model, or “LLM,” is a type of artificial intelligence system designed to understand, generate, and interact with human language. LLMs are based on a neural network architecture known as a transformer. Transformers enable LLMs to analyze and process vast amounts of text data. An LLM is “trained” through a process called machine learning, where a large corpus of text from various sources is input to the model. During training, the model learns patterns, language structures, and nuances, allowing it to generate coherent, contextually relevant responses. This learning process involves adjusting the internal parameters of the model to minimize the difference between its outputs and the expected results. Once trained, the model can perform a wide range of language-related tasks, such as answering questions, translating languages, summarizing texts, and creating content.

LLMs are known to “hallucinate.” Large Language Model (LLM) hallucinations refer to instances where these models generate incorrect, misleading, or nonsensical information while appearing confident and coherent. This phenomenon arises because LLMs don't truly “understand” content in the way humans do. Instead, they generate responses based on patterns learned from their training data. When an LLM encounters a query that falls outside its training or is ambiguous, it can produce responses that seem plausible but are factually inaccurate or completely fabricated. This issue is compounded by the model's lack of real-world awareness and inability to access or verify current information beyond its training cutoff. LLM hallucinations pose a challenge in applications where accuracy is crucial, as the model's authoritative tone can be misleading.

BRIEF DESCRIPTION OF THE DRAWINGS

The detailed description of certain embodiments of the invention below may be understood by reference to the following figures:

FIG. 1 illustrates a Large Language Model (LLM) verifier system that enhances the accuracy of the outputs of a vanilla LLM and includes a domain model creator subsystem and an answer verifier subsystem.

FIG. 2 illustrates the domain model creator subsystem and detailed operation thereof.

FIG. 3 illustrates the answer verifier subsystem and detailed operation thereof.

FIG. 4 illustrates an example conversation between a user and a large language model (LLM) agent.

FIG. 5 is flowchart of a method for selecting a desired translation of natural language to logic.

FIG. 6 illustrates three procedures implementing a scenario generation technique.

FIG. 7 is a flowchart of an enumerate models procedure of the scenario generation technique.

FIG. 8 is a flowchart of a minimize model procedure of the scenario generation technique.

FIG. 9 illustrates an example multi-tenant provider network environment in which the techniques disclosed herein for large language model (LLM) verification 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 large language model (LLM) verification 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 large language model (LLM) verification.

DETAILED DESCRIPTION

Disclosed herein are systems, methods, and non-transitory computer-readable media (generally, “techniques”) for large language model (LLM) verification. The techniques include verifying large language model responses by obtaining a query and its corresponding answer from a large language model. This conversational text is then fed into a second large language model, which translates the answer into first-order logic. The verification process uses an automated theorem prover. It checks the validity of this logic translation by determining the unsatisfiability of two scenarios: one where the negation of the logic translation and domain-specific logic formulas are combined, and another where the logic translation itself is combined with these formulas. Based on this analysis, the theorem prover ascertains whether the translated answer is valid, invalid, or neither. The final step is communicating this verification status through an appropriate output medium, such as a graphical user interface, a database, or a report, providing a structured and methodical approach to assessing the accuracy and reliability of language model responses.

The present disclosure includes a structured approach to verify responses generated by large language models. It begins by collecting a query and its answer from a primary large language model. This conversational exchange is then processed by a secondary large language model that translates the answer into first-order logic. This translation forms the basis of the verification process, which is conducted using an automated theorem prover. The theorem prover evaluates the logical validity by examining two distinct scenarios. In the first scenario, it checks the unsatisfiability of the negated logic translation in conjunction with domain-specific logic formulas. In the second, it assesses the unsatisfiability of the direct logic translation combined with the same set of formulas. This dual analysis allows the theorem prover to determine if the translated answer is valid, invalid, or indeterminate. Finally, the outcome of this verification is communicated through an output medium like a graphical user interface, a database, or a report. This approach ensures a rigorous and systematic evaluation of the accuracy and reliability of answers provided by language models, enhancing their credibility and utility in various applications.

As referenced in this description, large language models (LLMs) are advanced AI systems characterized by their deep learning techniques and vast training datasets. They are built using neural networks, specifically a type of architecture known as the Transformer, which is highly efficient in processing and generating sequential data like text. The “large” in their name refers not only to the size of their training data, encompassing diverse text sources, but also to the complexity of their neural network, often containing billions or even trillions of parameters. These parameters are fine-tuned during the training process, allowing the model to learn intricate patterns and nuances of language, including grammar, context, idioms, and even styles of writing. A useful feature of large language models is their ability to handle and generate contextually relevant text, making them adept at tasks like answering questions, composing texts, and translating languages. They achieve this through a mechanism known as attention, which enables the model to weigh different parts of the input text differently, thereby focusing on the most relevant parts to generate coherent and context-aware outputs.

In this disclosure, familiarity with first-order logic is assumed. Formulas of a first-order language L are built using predicate symbols, function symbols, and constants from some given alphabet together with logical connectives, quantifiers, and variables. An expression (e.g., a term, literal, formula, etc.) is ground if it contains no variables. A propositional assignment is a mapping from ground atoms to the truth values 1 (true) and 0 (false). Accordingly, a set of ground formulas is propositionally satisfiable if there exists a propositional assignment that satisfies all formulas in the set under the usual semantics for the logical connectives. Assignments can be written as sequences of literals where a positive (negative) polarity of a literal indicates that the truth value 1 (0, respectively) is assigned to the literal's atom.

As referenced in this description, automated theorem provers are sophisticated computational tools designed to assist in or fully automate the process of proving mathematical theorems. At their core, they rely on formal logic and various algorithms to deduce truths from a set of axioms and rules of inference. These systems are built upon a foundation of symbolic logic, primarily using first-order or higher-order logic. The technical prowess of these provers lies in their ability to methodically explore the vast space of potential proofs, which is often too large and complex for manual navigation. They employ various strategies like resolution, term rewriting, and decision procedures for specific theories to efficiently manage this exploration. Some provers specialize in certain domains by incorporating relevant mathematical theories (like arithmetic or geometry), thereby enhancing their effectiveness in those areas. A useful aspect of automated theorem provers is their use of formal languages to ensure precision and unambiguity in representing mathematical statements. This precision is crucial for correctly interpreting the theorems and proofs.

As referenced in this description, an SMT (Satisfiability Modulo Theories) solver, as a type of automated theorem prover, is distinguished by its ability to determine the satisfiability of logical formulas within various mathematical theories. Technically, it extends the capabilities of a basic SAT (Boolean satisfiability) solver by incorporating domain-specific knowledge from theories like linear arithmetic, real numbers, bit-vectors, arrays, and function symbols with uninterpreted functions. This integration allows SMT solvers to handle a more expressive set of logical formulas than those limited to propositional logic.

A useful characteristic of SMT solvers is their use of decision procedures or theory solvers, specialized algorithms designed to handle formulas within a specific theory. These solvers can efficiently reason about the satisfiability of formulas by considering the semantics of the theories they involve. An SMT solver typically integrates multiple theory solvers, enabling it to work with formulas that span several theories simultaneously. This feature makes SMT solvers incredibly versatile and powerful, especially in applications like software verification, model checking, and constraint solving, where complex logical relationships need to be analyzed.

The effectiveness of an SMT solver largely depends on its ability to balance the generality of handling multiple theories with the efficiency of solving instances quickly. It achieves this through techniques like backtracking, theory combination, and heuristic-guided search.

As referenced in this description, SMT-LIB is a standard library for Satisfiability Modulo Theories (SMT), designed to facilitate the development, testing, and comparison of SMT solvers. It primarily consists of a large and growing collection of benchmark problems, expressed in a standardized input language. This language, also called SMT-LIB language, is a formal, computer-readable language specifically crafted for describing problems in various SMT theories like linear integer arithmetic, real arithmetic, bit-vectors, arrays, and uninterpreted functions. The language is rigorously defined, ensuring consistency and uniformity in the way SMT problems are specified, which is crucial for fair and accurate comparisons among different solvers.

One of the useful technical characteristics of SMT-LIB is its structured, yet flexible format. It allows for the clear definition of logic theories, the declaration of functions and types, and the specification of assertions (formulas) that need to be satisfied. This structured approach enables SMT solvers to parse and process these benchmarks uniformly. SMT-LIB also provides a common set of commands for solver interaction, making it easier to control and communicate with SMT solvers in a standardized way.

Example LLM Verification System

Referring now to FIG. 1 , a Large Language Model (LLM) verifier system 100 enhances the accuracy of the outputs of a “vanilla” LLM 102 . The vanilla LLM 102 can be a standard, general-purpose LLM used for basic language processing and interaction tasks. However, the techniques described herein can be implemented with a special-purpose LLM as a substitute for the vanilla LLM 102 where the special-purpose LLM is based on a vanilla LLM or a foundational LLM that has been fine-tuned or trained for a domain-specific task using, for example, retrieval augmented generation (RAG) techniques or other suitable LLM fine-tuning techniques.

The enhancement in accuracy is achieved by verifying the truthfulness of the key information that the vanilla LLM 102 provides in response to customer queries. The LLM verifier system 100 is designed with multiple interconnected networks, each contributing to this verification process. A multi-tenant provider network 104 , which includes an answer verifier system 106 , or “answer verifier 106 ,” acts as a primary checkpoint for validating responses. The answer verifier system 106 cross-references the vanilla LLM 102 's answers with trusted sources or logical frameworks, ensuring that the information is not only coherent but also factually correct. Meanwhile, domain expert data network 108 , which encompasses a logic-trained LLM 110 , a domain expert 112 , and a set of documents 114 , offers specialized oversight.

Ensuring the accuracy of certain types of information generated by the vanilla LLM 102 is important. This is especially true for data that is critically sensitive, high-stakes, or foundational to subsequent decision-making processes. In such scenarios, it is important to minimize or mitigate what are known as “LLM hallucinations” by the vanilla LLM 102 . An LLM hallucination occurs when the model generates responses that are confidently presented but factually incorrect or nonsensical. This can be particularly problematic when dealing with sensitive or critical information where accuracy is non-negotiable. To address this, the LLM verifier system 100 employs rigorous verification mechanisms, such as cross-referencing with trusted data sources, logical consistency checks, and specialized domain expertise, to ensure that the outputs from the vanilla LLM 102 are not only plausible but also factually accurate. This layered approach to verification is useful to maintaining the integrity and reliability of subsequent decision making, especially in scenarios where incorrect information could lead to significant consequences.

The LLM verifier system 100 serves as a “source of truth” for critical domains, striking a balance between automation and human curation. The LLM verifier system 100 is designed to automate the process of verifying the accuracy and reliability of information generated by the vanilla LLM 102 , especially in areas where precision is paramount. The automated aspect is facilitated by advanced algorithms and logical models within the LLM verifier system 100 , which cross-check the vanilla LLM 102 's outputs against a robust database of verified information and domain-specific knowledge. This process ensures that the responses are not only contextually relevant but also factually correct. However, there may be an element of human curation involved as well. The domain expert 112 oversees and refines the LLM verified system 100 's outputs, particularly in complex or nuanced areas where human judgement is crucial. This combination of automated verification with expert oversight enables the LLM verifier system 100 to function as a reliable and authoritative source in critical domains, providing customers with confidence in the accuracy and integrity of the information they receive.

In operation, a domain model creator system 116 , or just “ DMC 116 ,” accepts as input the set of documents 114 containing critical information. These documents 114 are not just random assortments of information; they are carefully selected and contain critical information pertinent to the domain or subject matter at hand. For example, the documents 114 can pertain to laws, rules, regulations, or health and safety, etc. For example, these documents 114 may include detailed information about laws, encompassing statutes, legal precedents, and legislative texts. They could also cover various rules and regulations that govern industry practices, corporate behavior, or public policies. Additionally, these documents 114 might encompass data related to health and safety, such as medical guidelines, public health protocols, safety standards in manufacturing, or environmental protection regulations.

The DMC 116 uses the documents 114 to create a domain model in logic (referred to as “ domain logic model 118 ”) that is used by the answer verifier 106 to verify responses generated by the vanilla LLM 102 to prompts submitted to the vanilla LLM 102 by a customer 120 . The domain logic model 118 is specifically tailored to enhance the functionality of the vanilla LLM 102 . When the customer 120 submits prompts to the vanilla LLM 102 , it generates responses based on its general knowledge and algorithms. However, the accuracy and relevance of these responses, especially in specialized or complex domains, may not always be optimal. This is where the domain logic model 118 created by the DMC 116 becomes useful. It acts as a verifier or a benchmark against which the responses from the vanilla LLM 102 are evaluated. The logic model 118 , informed and structured by the critical information in the documents 114 , embodies a logical and domain-specific understanding. This allows it to assess the vanilla LLM 102 's responses for their accuracy and alignment with the specialized knowledge encapsulated in the domain logic model 118 . Essentially, the DMC 116 , in conjunction with the domain logic model 118 and the answer verifier 106 , imparts an additional layer of expertise and validation to the outputs of the vanilla LLM 102 , ensuring that the information provided to the customer 120 is not only generated by advanced AI algorithms but is also vetted against the robust, logically constructed domain logic model 118 .

To verify responses generated by the vanilla LLM 102 against domain logic model 118 , the responses are transformed into formal logic for accuracy. This means that the responses, initially in a natural language format, are converted into a structured, logical form. This transformation is useful to assessing the accuracy of the responses. By expressing the responses in the language of formal logic, it becomes possible to rigorously compare them against the established principles and rules encapsulated in the domain logic model 118 . The domain logic model 118 acts as a benchmark, embodying the specific logical constructs and knowledge pertinent to the domain in question. Therefore, when the vanilla LLM 102 's responses are converted into this formal logical structure, it allows for a systematic and precise evaluation. This process ensures that the responses not only seem plausible in natural language but also adhere to the stringent criteria of logical coherence and factual accuracy as defined by the domain logic model 118 . This verification step is useful for maintaining the integrity and reliability of the vanilla LLM 102 's outputs, especially in scenarios where precision and correctness are paramount.

The DMC 116 creates the domain logic model 118 from the documents 114 with the aid of a logic-trained LLM 110 . The logic-trained LLM 110 can be a vanilla or generic LLM that has been fined-tuned or enhanced using retrieval augmented generation (RAG) techniques. The logic-trained LLM 110 is trained on logical syntax, and examples of rules specified in the documents 114 converted to logic. The logic-trained LLM 110 starts as a vanilla or generic LLM, which is then fine-tuned or enhanced through the application of Retrieval Augmented Generation (RAG) techniques. These techniques enable the logic-trained LLM 110 to incorporate and leverage external information effectively, enhancing its capability to process and understand complex data. An aspect of the logic-trained LLM 110 is its training regimen; it is specifically trained on logical syntax and examples of rules that are extracted from the set of documents 114 . These rules and related information from the documents are converted into a formal logic structure as part of the training process. This specialized training ensures that the logic-trained LLM 110 has a robust understanding of logical constructs and is adept at handling and interpreting information in a logically coherent manner. Consequently, when the DMC 116 employs this logic-trained LLM 110 to assist in creating the domain logic model 118 , it benefits from the logic-trained LLM 110 's enhanced ability to process and integrate complex, rule-based information. This results in the formation of a highly sophisticated and accurate domain logic model 118 , which is then used to verify and validate responses in specific domain contexts, ensuring their logical soundness and adherence to the specialized knowledge encapsulated in the documents.

In some embodiments, the domain expert 112 uses the logic-trained LLM 110 through a series of pre-built prompt templates to derive the domain logic model 118 in a logic specification format from the set of documents 114 . In this scenario, the domain expert 112 utilizes the logic-trained LLM 110 , but rather than engaging in an open-ended or ad-hoc interaction, they use a series of pre-built prompt templates. These templates are designed to systematically extract and process information from the set of documents 114 in a highly structured and efficient manner. The pre-built prompts guide the interaction with the logic-trained LLM 110 , ensuring that the queries and commands are precisely aligned with the goal of deriving the domain logic model 118 . The logic-trained LLM 110 , with its enhanced capabilities in understanding and applying logical constructs, interprets and analyzes the contents of the documents 114 under the framework provided by these templates. This process results in the transformation of the information in the documents 114 into a logic specification format, which essentially means converting the data into a structured, formal logic representation. This representation is what constitutes the domain logic model 118 . By using pre-built prompt templates, the domain expert 112 can effectively harness the advanced capabilities of the logic-trained LLM 110 , ensuring that the derived domain logic model 118 is both accurate and highly tailored to the specific requirements of the domain as represented in the documents 114 .

The output from the DMC 116 is the formal domain logic model 118 expressed in formal logic for use with automated solver. The formal logic expression allows the domain logic model 118 to be utilized with an automated solver. An automated solver refers to a system or tool capable of processing logical expressions and solving logical problems or queries. By expressing the domain logic model in formal logic, the DMC 116 ensures that this model can be seamlessly integrated with such solvers. This integration is useful because it enables the automated application of the domain logic model 118 in various operations, such as verifying the accuracy of responses generated by other systems like the vanilla LLM 102 . The formal logic format provides a structured, rule-based framework that can be systematically interpreted and manipulated by the solver.

In some embodiments, the DMC 116 is equipped with the capability to generate the domain logic model 118 in a fully automated manner, independent of direct guidance or input from the domain expert 112 . In these scenarios, the DMC 116 relies on its advanced algorithms and possibly pre-programmed criteria to process and interpret the set of documents 114 on its own. It extracts pertinent information, converts it into a structured logic format, and constructs the domain logic model 118 without the need for step-by-step oversight or instructions from the domain expert 112 . This automated process of domain logic model 118 creation enhances efficiency, as it reduces the reliance on human intervention and accelerates the domain logic model 118 development cycle.

Even in scenarios where the DMC 116 demonstrates the capability to autonomously generate a complete and accurate domain logic model 118 from the set of documents 114 , there may still be instances where intervention or verification by the domain expert 112 is necessary. This need arises particularly in cases where the source documents 114 themselves present ambiguities or inconsistencies. While the DMC 116 is equipped with sophisticated algorithms to process and translate document content into the domain logic model 118 , its ability to resolve inherent ambiguities or contradictions in the source documents 114 is inherently limited. In such situations, the nuanced understanding and interpretative skills of a human expert can be used. The domain expert 112 can review the domain logic model 118 to identify and rectify any issues that stem from unclear or conflicting information in the documents 114 . This human oversight ensures that the final domain logic model 118 accurately reflects the intended meanings and stipulations of the source material, maintaining the integrity and reliability of the domain logic model 118 . Thus, while the DMC 116 offers significant automation and efficiency in domain logic model 118 creation, the expertise and judgment of the domain expert 112 may be needed to ensure the highest quality and accuracy of the final domain logic model 118 , especially in complex or nuanced domains.

The domain logic model 118 is evaluated to ensure its completeness and consistency. This evaluation is carried out using a trusted solver 122 which could be, for example, a Satisfiability Modulo Theories (SMT) solver. A function of the trusted solver 122 is to generate various scenarios that are either allowed or disallowed by the rules and stipulations defined in the domain logic model 118 . These scenarios serve as test cases or examples that reflect the logical outcomes derived from the domain logic model 118 's parameters. The domain expert 112 then examines these scenarios to assess their correctness and alignment with the intended logic and knowledge of the domain. This process is useful for verifying that the domain logic model 118 not only adheres to the formal logical structures but also accurately represents the real-world rules and conditions of the domain it is intended to simulate. By analyzing the scenarios generated by the trusted solver 122 , the domain expert 112 can identify any inconsistencies, gaps, or errors in the domain logic model 118 . This scrutiny helps in refining the domain logic model 118 , ensuring that it is both logically sound and practically relevant. The use of an SMT solver or similar tools in this process adds a layer of rigorous, systematic testing that might be challenging to achieve through manual review alone, thereby enhancing the overall robustness and reliability of the domain logic model 118 .

The evaluation process described, involving the use of the trusted solver 122 to test the domain logic model 118 , offers a benefit in terms of identifying inconsistencies and ambiguities within the informal documents 114 used to construct the domain logic model 118 . When the domain logic model 118 is subjected to this form of rigorous analysis, the scenarios generated by the trusted solver 122 can reveal discrepancies and unclear elements that may not have been apparent during the domain logic model 118 's initial construction. These inconsistencies might stem from the informal nature of the source documents 114 , which could contain imprecise language, contradictory information, or incomplete details. By applying the structured, logical framework of the domain logic model 118 in a practical, scenario-based test, these issues are brought to light. This process allows for a more thorough understanding of the limitations and potential areas of improvement in the source documents 114 . As a result, it not only enhances the accuracy and reliability of the domain logic model 118 itself but also provides valuable insights into the quality and clarity of the underlying documents 114 . This feedback loop is useful for refining both the domain logic model 118 and the source material 114 , ensuring that the final product is robust and truly representative of the domain it aims to encapsulate.

The DMC 116 can be used beyond its role in the LLM verified system 100 , functioning as a stand-alone system to assist a customer 120 in various industries. Businesses and organizations often grapple with the challenge of translating their complex, domain-specific logic—such as, for example, authentication and authorization policies, intricate tax rules, network readability parameters, or railroad design guidelines—into structured, formal models that can be utilized for various purposes, including verification and decision-making. The DMC 116 can play a useful role in this transformation process. By leveraging its advanced capabilities to process and understand complex sets of information, the DMC 116 can systematically convert the often informal, nuanced business logic into a formal <figure-callout id="118" label="domain l

CLAIMS

Claims ( 20 )

What is claimed is:

1 . 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; 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.

2 . The method of claim 1 , 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.

3 . The method of claim 1 ,

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.

4 . A method for large language model verification comprising:

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; 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 an automated theorem prover 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 an automated theorem prover 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.

5 . The method of claim 4 , 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.

6 . 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 all of the plurality of first-order logic translations; and selecting the first-order logic translation from the non-overlapping set.

7 . 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.

8 . The method of claim 4 , further comprising:

converting a set of natural language text documents into the set of first-order logic formulas of the domain logic model.

9 . The method of claim 4 , 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.

10 . The method of claim 4 , 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.

11 . The method of claim 4 , wherein:

the first query comprises is unsatisfiable; the second query is satisfiable; the indication output indicates that the answer is valid.

12 . The method of claim 4 , further comprising:

the first query is satisfiable; the second query is unsatisfiable; the indication output indicates that the answer is invalid.

13 . The method of claim 4 , 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.

14 . A system comprising:

a first one or more programmable electronic devices to implement an automated theorem prover; and a second one or more programmable electronic devices to implement a large language model verification system, the large language model verification system comprising instructions which when executed cause the large language model verification system to perform: 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; 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 an automated theorem prover 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 an automated theorem prover 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.

15 . The system of claim 14 , wherein the large language model verification system further comprises instructions which when executed cause the large language model verification system to perform:

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.

16 . The system of claim 15 , 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.

17 . The system of claim 15 , 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.

18 . The system of claim 14 , wherein the large language model verification system further comprises instructions which when executed cause the large language model verification system to perform:

converting a set of natural language text documents into the set of first-order logic formulas of the domain logic model.

19 . The system of claim 14 , wherein the large language model verification system further comprises instructions which when executed cause the large language model verification system to perform:

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.

20 . The system of claim 14 , wherein the large language model verification system further comprises instructions which when executed cause the large language model verification system to perform:

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.

US18/541,988

2023-12-15

2023-12-15

Large language model verification

Pending

US20250200392A1

( en )

Priority Applications (3)

Application Number

Priority Date

Filing Date

Title

US18/541,988

US20250200392A1

( en )

2023-12-15

2023-12-15

Large language model verification

PCT/US2024/059886

WO2025128894A1

( en )

2023-12-15

2024-12-12

Large language model verification

CN202480079544.3A

CN122439157A

( en )

2023-12-15

2024-12-12

Large language model verification

Applications Claiming Priority (1)

Application Number

Priority Date

Filing Date

Title

US18/541,988

US20250200392A1

( en )

2023-12-15

2023-12-15

Large language model verification

Publications (1)

Publication Number

Publication Date

US20250200392A1

true

US20250200392A1 ( en )

2025-06-19

Family

ID=94284128

Family Applications (1)

Application Number

Title

Priority Date

Filing Date

US18/541,988

Pending

US20250200392A1

( en )

2023-12-15

2023-12-15

Large language model verification

Country Status (3)

Country

Link

US

( 1 )

US20250200392A1

( en )

CN

( 1 )

CN122439157A

( en )

WO

( 1 )

WO2025128894A1

( en )

Cited By (12)

* Cited by examiner, † Cited by third party

Publication number

Priority date

Publication date

Assignee

Title

US20250217393A1

( en )

*

2023-12-29

2025-07-03

Cx360, Inc.

Artificial Intelligence Queries with Multiple Constraints

US20250265411A1

( en )

*

2024-02-21

2025-08-21

Kyndryl, Inc.

Multi-cloud generative artificial intelligence arbitrage, orchestration, and accuracy validation

CN120782339A

( en )

*

2025-09-10

2025-10-14

江苏国信数智服务有限公司

Full-link data difference matching and quality dispute processing method

CN120780918A

( en )

*

2025-09-10

2025-10-14

四川大学

Multi-agent-based fact checking method and system, storage medium and electronic equipment

CN120973884A

( en )

*

2025-09-04

2025-11-18

北京电子数智科技有限责任公司

Legal information analysis methods and systems, computer devices, media, and products

US12499387B2

( en )

2024-03-08

2025-12-16

Seekr Technologies Inc.

Question answer (QA) pair generation using agentic workflow system and method that aligns artificial intelligence model with domain-specific principles

CN121390259A

( en )

*

2025-09-30

2026-01-23

武汉理工大学

Battery material field data processing method based on large language model and related equipment

CN121480504A

( en )

*

2025-11-07

2026-02-06

南京邮电大学

A method and system for evaluating large language models and optimizing prompt words based on RDFS ontology.

CN121501985A

( en )

*

2026-01-14

2026-02-10

长沙理工大学

Intelligent Review System for Institutional Conflict Points Based on Knowledge Graphs and Large Language Models

US12567270B1

( en )

*

2025-08-28

2026-03-03

Squint, Inc.

On-demand state verification using digital image processing and artificial intelligence

CN122021489A

( en )

*

2026-04-13

2026-05-12

复旦大学

DRC design rule positive and negative example automatic generation method based on large language model and formal verification

US12705250B2

( en )

*

2025-01-31

2026-08-11

Oracle International Corporation

Verifiable logical reasoning using GenAI

Families Citing this family (5)

* Cited by examiner, † Cited by third party

Publication number

Priority date

Publication date

Assignee

Title

US20240403566A1

( en )

*

2023-06-05

2024-12-05

AIble Inc.

Flexible artificial intelligence based system with prompt enhancement

US12651116B2

( en )

*

2024-01-26

2026-06-09

Qualcomm Incorporated

Selective parameter-efficient fine-tuning for large-scale models

US12608543B2

( en )

*

2024-05-13

2026-04-21

Nvidia Corporation

Generating virtual sensor parameters using large language models for synthetic data generation

US12670325B2

( en )

*

2024-08-14

2026-06-30

Ivalua Sas

Use of large language model in source-to-pay platform

CN121436106A

( en )

*

2025-12-31

2026-01-30

浙江大学

A formalized automatic theorem proof method based on large language models

Family Cites Families (1)

* Cited by examiner, † Cited by third party

Publication number

Priority date

Publication date

Assignee

Title

US12067362B2

( en )

*

2021-08-24

2024-08-20

Unlikely Artificial Intelligence Limited

Computer implemented methods for the automated analysis or use of data, including use of a large language model

2023

2023-12-15

US

US18/541,988

patent/US20250200392A1/en

active

Pending

2024

2024-12-12

WO

PCT/US2024/059886

patent/WO2025128894A1/en

active

Pending

2024-12-12

CN

CN202480079544.3A

patent/CN122439157A/en

active

Pending

Cited By (13)

* Cited by examiner, † Cited by third party

Publication number

Priority date

Publication date

Assignee

Title

US20250217393A1

( en )

*

2023-12-29

2025-07-03

Cx360, Inc.

Artificial Intelligence Queries with Multiple Constraints

US20250265411A1

( en )

*

2024-02-21

2025-08-21

Kyndryl, Inc.

Multi-cloud generative artificial intelligence arbitrage, orchestration, and accuracy validation

US12499387B2

( en )

2024-03-08

2025-12-16

Seekr Technologies Inc.

Question answer (QA) pair generation using agentic workflow system and method that aligns artificial intelligence model with domain-specific principles

US12579475B2

( en )

*

2024-03-08

2026-03-17

Seekr Technologies Inc.

Artificial intelligence model generated using agentic workflow system and method for artificial intelligence model aligned with domain-specific principles

US12705250B2

( en )

*

2025-01-31

2026-08-11

Oracle International Corporation

Verifiable logical reasoning using GenAI

US12567270B1

( en )

*

2025-08-28

2026-03-03

Squint, Inc.

On-demand state verification using digital image processing and artificial intelligence

CN120973884A

( en )

*

2025-09-04

2025-11-18

北京电子数智科技有限责任公司

Legal information analysis methods and systems, computer devices, media, and products

CN120780918A

( en )

*

2025-09-10

2025-10-14

四川大学

Multi-agent-based fact checking method and system, storage medium and electronic equipment

CN120782339A

( en )

*

2025-09-10

2025-10-14

江苏国信数智服务有限公司

Full-link data difference matching and quality dispute processing method

CN121390259A

( en )

*

2025-09-30

2026-01-23

武汉理工大学

Battery material field data processing method based on large language model and related equipment

CN121480504A

( en )

*

2025-11-07

2026-02-06

南京邮电大学

A method and system for evaluating large language models and optimizing prompt words based on RDFS ontology.

CN121501985A

( en )

*

2026-01-14

2026-02-10

长沙理工大学

Intelligent Review System for Institutional Conflict Points Based on Knowledge Graphs and Large Language Models

CN122021489A

( en )

*

2026-04-13

2026-05-12

复旦大学

DRC design rule positive and negative example automatic generation method based on large language model and formal verification

Also Published As

Publication number

Publication date

CN122439157A

( en )

2026-07-21

WO2025128894A1

( en )

2025-06-19

Similar Documents

Publication

Publication Date

Title

WO2025128894A1

( en )

2025-06-19

Large language model verification

He et al.

2025

Large language models for eda: Future or mirage?

Wang et al.

2025

Intent-driven network management with multi-agent llms: The confucius framework

Duan et al.

2025

The development of a digital twin concept system

KR20220031522A

( en )

2022-03-11

Process to combine semantic descriptions of digital twins with knowledge graphs

Busch et al.

2023

ChatGPT in the loop: a natural language extension for domain-specific modeling languages

CN110659029B

( en )

2023-03-24

Generating semantic flow graph representing computer program

Winston et al.

2025

A taxonomy of failures in tool-augmented LLMs

Serrano et al.

2013

Data mining agent conversations: A qualitative approach to multiagent systems analysis

WO2025064639A1

( en )

2025-03-27

Platform-enabled orchestration and optimization of digital workflows

Tauscher et al.

2021

A modular graph transformation rule set for IFC‐to‐CityGML conversion

Moezkarimi et al.

2025

Harnessing chatgpt for model transformation in software architecture: From uml state diagrams to rebeca models for formal verification

Bandlamudi et al.

2024

Framework to enable and test conversational assistant for APIs and RPAs

El-Gohary et al.

2011

Merging architectural, engineering, and construction ontologies

Sen et al.

2011

A protocol to formalise function verbs to support conservation-based model checking

Lawniczak et al.

2025

Reasoning with epistemic rights and duties: Automating a dynamic logic of the right to know in LogiKEy

JP2026009021A

( en )

2026-01-19

Method, system, and computer program for attributing source code, and method and system for enhancing source code verification (Code verification and attribution using semantic analysis)

Moscato et al.

2014

Dynamite: A tool for the verification of alloy models based on PVS

Pileggi et al.

2018

Ontology in software engineering

CN114175016B

( en )

2025-11-04

Extracting meaning from text

Handa et al.

2025

Test Case Generation using Graph-based Deep Learning Methods

Bowles et al.

2017

Correct composition of dephased behavioural models

Weidmann

2021

Fault-Tolerant Consistency Management in Model-Driven Engineering

US20260127386A1

( en )

2026-05-07

Language model theory solvers

Lin et al.

2013

OntCheck: An Ontology‐Driven Static Correctness Checking Tool for Component‐Based Models

Legal Events

Date

Code

Title

Description

2024-02-02

STPP

Information on status: patent application and granting procedure in general

Free format text : DOCKETED NEW CASE - READY FOR EXAMINATION

2024-07-16

AS

Assignment

Owner name : AMAZON TECHNOLOGIES, INC., WASHINGTON

Free format text : ASSIGNMENT OF ASSIGNORS INTEREST;ASSIGNORS:WHALEN, MICHAEL WILLIAM;KIESL-REITER, BENJAMIN;LABAI, NADIA;AND OTHERS;SIGNING DATES FROM 20231213 TO 20240712;REEL/FRAME:067996/0062

2026-05-31

STPP

Information on status: patent application and granting procedure in general

Free format text : NON FINAL ACTION COUNTED, NOT YET MAILED

2026-06-03

STPP

Information on status: patent application and granting procedure in general

Free format text : NON FINAL ACTION MAILED

Related documents

• The Hallucination Regime: When Coherence Replaces Reality#96642
• N0042125F0127 — AMAZON WEB SERVICES, INC. — Department of Defense ($48,126,561)#601701
• Proceedings of the 2025 International Conference on Educational Technology and Management Information Systems (ETMIS 2025) / edited by A. Y. M. Atiquil Islam, Maizatul Hayati binti Mohamad Yatim, Harwati Hashim, Madihah Bt. S. Abd. Aziz#1165612
• Heterogeneous Structured Pruning Under Resource Constraints for Hardware-Efficient Large Language Models#1327031
• N6523624F0453 — AMAZON WEB SERVICES, INC. — Department of Defense ($94,751,464)#601388