Back to results
US 12,748,791 B2Granted
Scalable generative AI-based tool infrastructure
AssigneeMicrosoft Technology Licensing, LLC
InventorsErik William Berg, Yash Jayesh Dagli, Amber Elisabeth Telfer Norris
Life of this patent
Estimating the term…
Abstract
Embodiments of the present disclosure include a formal verification method comprising a plurality of custom generative AI-based tools configured in a bottoms up methodology to generate formal verification code using an LLM. In another embodiment, the present disclosure includes a generative AI-based tool architecture comprising an index of code examples. A query from a user is used to retrieve code examples, and the query and code examples are sent to an LLM to generate code corresponding to the query.
Claims20
A method, comprising:
- receiving an input query from a user prompt;
- sending the input query to a large language model (LLM);
- receiving, from the LLM, an initial representation of the input query;
- performing, based on the initial representation, a lookup on an index storing a plurality of entries, wherein each of the plurality of entries in the index follows a domain specific code syntax, and performing the lookup comprises:
- retrieving, from the index, a plurality of relevant entries based on the initial representation;
- and
- ranking the plurality of relevant entries according to how each entry matches the input query;
- supplementing the input query with at least some of the plurality of relevant entries, including:
- determining that a token count of the input query plus a token count of the plurality of relevant entries exceeds an allowed token window of the LLM;
- selecting, from the plurality of relevant entries and in accordance with the ranking, a subset of the plurality of relevant entries such that a combined token count of the input query and the subset does not exceed the allowed token window of the LLM;
- and
- combining the input query and the subset of the plurality of relevant entries to generate a supplemented input query:
- sending the supplemented input query to the LLM;
- receiving, from the LLM, a response corresponding to the supplemented input query;
- and
- presenting the response on a graphical user interface.
13 more elements
A system comprising:
- one or more processors;
- a non-transitory computer-readable medium storing a program executable by the one or more processors, the program comprising sets of instructions for:
- receiving an input query from a user prompt;
- sending the input query to a large language model (LLM);
- receiving, from the LLM, an initial representation of the input query;
- performing, based on the initial representation, a lookup on an index storing a plurality of entries, wherein each of the plurality of entries in the index follows a domain specific code syntax, and performing the lookup comprises:
- retrieving, from the index, a plurality of relevant entries based on the initial representation;
- and
- ranking the plurality of relevant entries according to how each entry matches the input query;
- supplementing the input query with at least some of the plurality of relevant entries, including:
- determining that a token count of the input query plus a token count of the plurality of relevant entries exceeds an allowed token window of the LLM;
- selecting, from the plurality of relevant entries and in accordance with the ranking, a subset of the plurality of relevant entries such that a combined token count of the input query and the subset does not exceed the allowed token window of the LLM;
- and
- combining the input query and the subset of the plurality of relevant entries to generate a supplemented input query;
- sending the supplemented input query to the LLM;
- receiving, from the LLM, a response corresponding to the supplemented input query;
- and
- presenting the response on a graphical user interface.
15 more elements
A non-transitory computer-readable medium storing a program executable by one or more processors, the program comprising sets of instructions for:
- receiving an input query from a user prompt;
- sending the input query to a large language model (LLM);
- receiving, from the LLM, an initial representation of the input query;
- performing, based on the initial representation, a lookup on an index storing a plurality of entries, wherein each of the plurality of entries in the index follows a domain specific code syntax, and performing the lookup comprises:
- retrieving, from the index, a plurality of relevant entries based on the initial representation;
- and
- ranking the plurality of relevant entries according to how each entry matches the input query;
- supplementing the input query with at least some of the plurality of relevant entries, including:
- determining that a token count of the input query plus a token count of the plurality of relevant entries exceeds an allowed token window of the LLM;
- selecting, from the plurality of relevant entries and in accordance with the ranking, a subset of the plurality of relevant entries such that a combined token count of the input query and the subset does not exceed the allowed token window of the LLM;
- and
- combining the input query and the subset of the plurality of relevant entries to generate a supplemented input query;
- sending the supplemented input query to the LLM;
- receiving, from the LLM, a response corresponding to the supplemented input query;
- and
- presenting the response on a graphical user interface.
13 more elements
Dependencies are inferred from the claim text.