OUTPUT PREFIX SPECIFICATION TRANSFORMERS

• US 20190324730A1
• Filed: 04/24/2018
• Published: 10/24/2019
• Est. Priority Date: 04/24/2018
• Status: Active Grant

• Current Assignee: Microsoft Technology Licensing LLC (Microsoft Corporation)
• Original Assignee: Microsoft Technology Licensing LLC (Microsoft Corporation)
• Inventors: Gulwani, Sumit, Udupa, Abhishek
• Granted Patent: US 10,635,414 B2
• Time in Patent Office: Days
• CPC Class Codes: G06F 40/16 Automatic learning of transformation rules, e.g. from examples
• CPC Class Codes: G06F 40/18 of spreadsheets form-filling G06F40/174
• CPC Class Codes: G06F 8/30 Creation or generation of source code
• CPC Class Codes: G06F 8/35 model driven
• CPC Class Codes: G06F 8/40 Transformation of program code

Abstract

Systems, methods, and computer-executable instructions for synthesizing programs using a prefix of an output. A specification of a task to synthesize a program in a domain specific language (DSL) is received. The specification includes an input and a corresponding prefix of the output. Programs for the task are synthesized. The synthesizing includes generating sub-goals based on the specification. Each of the synthesized programs include a solved subset of sub-goals and each sub-goal includes a symbol in the DSL. The symbol is transformed based on the DSL. The sub-goals are solved based on the transforming of the symbol using the input and the corresponding prefix of the output to generate the synthesized programs. The prefix of the output matches a prefix of an output from each of the plurality of synthesized programs.

Claims

1. A method for synthesizing programs using a prefix of an output, the method comprising operations performed using an electronic processor, the operations comprising:

receiving a specification of a task to synthesize a program in a domain specific language (DSL), wherein the specification comprises an input and a corresponding prefix of the output;

synthesizing a plurality of programs for the task, wherein the synthesizing comprises;

generating a plurality of sub-goals based on the specification, wherein each of the plurality of synthesized programs comprise a solved subset of the plurality of the sub-goals, and wherein a sub-goal comprises a symbol in the DSL;

transforming the symbol based on the DSL and the prefix of the output, and

solving the plurality of sub-goals based on the transforming of the symbol using the input and the corresponding prefix of the output to generate the plurality of synthesized programs, wherein the prefix of the output matches a prefix of an output from each of the plurality of synthesized programs.

2. The method of claim 1, further comprising:

ranking the plurality of synthesized programs; and

selecting a highest ranking synthesized program.

3. The method of claim 2, further comprising:

executing the highest ranking synthesized program on additional input to create additional output, wherein the additional input was not used for synthesizing the plurality of synthesized programs; and

providing the additional output.

4. The method of claim 3, further comprising:

receiving a corrective output prefix for a first input and a corresponding erroneous output, wherein the additional input comprises the first input, and wherein a first set of input and output examples precedes the first input in the additional data; and

selecting a new synthesized program from the plurality of synthesized programs, wherein a prefix of output from the new synthesized program using the first input matches the corrective output prefix.

5. The method of claim 4, wherein output from the new synthesized program is consistent with the input and the output in the first set of input and output examples that precedes the first input in the additional data.

6. The method of claim 4, further comprising executing the new synthesized program on a second set of input that follows the first input in the additional data.

7. The method of claim 1, further comprising:

receiving a second partial output to a corresponding second input;

executing the plurality of synthesized programs on the second input;

selecting output from executing the plurality of synthesized programs on the second input based on a prefix of the output matching the second partial output; and

displaying the selected output.

8. The method of claim 7, further comprising:

updating the specification by adding the second input and the second partial output to the specification as an input output example; and

synthesizing a second plurality of tasks based on the updated specification.

9. The method of claim 7, further comprising:

receiving a selection of a corrective output associated with a second synthesized program, wherein the corrective output is different from an output from a highest ranking synthesized program; and

executing the second synthesized program on additional input.

10. A system for synthesizing programs using a prefix of an output, the system comprising:

a program synthesizer configured to;

receive a specification of a task to synthesize a program in a domain specific language (DSL), wherein the specification comprises an input and a corresponding prefix of the output;

synthesize a plurality of programs for the task, wherein to synthesize the program synthesizer is further configured to;

generate a plurality of sub-goals based on the specification, wherein each of the plurality of synthesized programs comprise a solved subset of the plurality of the sub-goals, and wherein a sub-goal comprises a symbol in the DSL;

transform the symbol based on the DSL; and

solve the plurality of sub-goals based on the transformation of the symbol using the input and the corresponding prefix of the output to generate the plurality of synthesized programs, wherein the prefix of the output matches a prefix of an output from each of the plurality of synthesized programs.

11. The system of claim 10, further comprising a ranker configured to:

rank the plurality of synthesized programs; and

select a highest ranking synthesized program.

12. The system of claim 11, further comprising an electronic processor configured to:

execute the highest ranking synthesized program on additional input to create additional output, wherein the additional input was not used for synthesizing the plurality of synthesized programs; and

provide the additional output.

13. The system of claim 12, wherein the electronic processor is further configured to:

receive a corrective output prefix for a first input and a corresponding erroneous output, wherein the additional input comprises the first input, and wherein a first set of input and output examples precedes the first input in the additional data; and

select a new synthesized program from the plurality of synthesized programs, wherein a prefix of output from the new synthesized program using the first input matches the corrective output prefix.

14. The system of claim 13, wherein output from the new synthesized program is consistent with the input and the output in the first set of input and output examples that precedes the first input in the additional data.

15. The system of claim 10, wherein the program synthesizer is further configured to:

receive a second partial output to a corresponding second input;

execute the plurality of synthesized programs on the second input;

select output from executing the plurality of synthesized programs on the second input based on a prefix of the output matching the second partial output; and

provide the selected output.

16. The system of claim 15, wherein the program synthesizer is further configured to:

receive a selection of a corrective output associated with a second synthesized program, wherein the corrective output is different from an output from a highest ranking synthesized program; and

execute the second synthesized program on additional input.

17. A computer-readable storage medium storing computer-executable instructions for synthesizing programs using a prefix of an output, the stored instructions comprising:

instructions to receive a specification of a task to synthesize a program in a domain specific language (DSL), wherein the specification comprises an input and a corresponding prefix of the output;

instructions to synthesize a plurality of programs for the task, wherein the instructions to synthesize the program comprise;

instructions to generate a plurality of sub-goals based on the specification, wherein each of the plurality of synthesized programs comprise a solved subset of the plurality of the sub-goals, and wherein a sub-goal comprises a symbol in the DSL;

instructions to transform the symbol based on the DSL; and

instructions to solve the plurality of sub-goals based on the transformation of the symbol using the input and the corresponding prefix of the output to generate the plurality of synthesized programs, wherein the prefix of the output matches a prefix of an output from each of the plurality of synthesized programs.

18. The computer-readable storage medium of claim 17, wherein the instructions further comprise:

instructions to execute the highest ranking synthesized program on additional input to create additional output, wherein the additional input was not used for synthesizing the plurality of synthesized programs; and

instructions to provide the additional output.

19. The computer-readable storage medium of claim 18, wherein the instructions further comprise:

instructions to receive a corrective output prefix for a first input and a corresponding erroneous output, wherein the additional input comprises the first input, and wherein a first set of input and output examples precedes the first input in the additional data; and

instructions to select a new synthesized program from the plurality of synthesized programs, wherein a prefix of output from the new synthesized program using the first input matches the corrective output prefix.

20. The computer-readable storage medium of claim 17, wherein the instructions further comprise:

instructions to receive a second partial output to a corresponding second input;

instructions to execute the plurality of synthesized programs on the second input;

select output from executing the plurality of synthesized programs on the second input based on a prefix of the output matching the second partial output; and

instructions to provide the selected output.