US 11,790,263 B2
Program synthesis using annotations based on enumeration patterns
Futoshi Iwama, Tokyo (JP); Takaaki Tateishi, Yamato (JP); and Shin Saito, Sagamihara (JP)
Assigned to INTERNATIONAL BUSINESS MACHINES CORPORATION, Armonk, NY (US)
Filed by INTERNATIONAL BUSINESS MACHINES CORPORATION, Armonk, NY (US)
Filed on Feb. 25, 2019, as Appl. No. 16/284,371.
Prior Publication US 2020/0272935 A1, Aug. 27, 2020
Int. Cl. G06N 20/00 (2019.01); G06N 5/02 (2023.01)
CPC G06N 20/00 (2019.01) [G06N 5/02 (2013.01)] 19 Claims
OG exemplary drawing
 
1. A system for computer program synthesis using annotations based on enumeration patterns, comprising:
a memory device for storing program code;
at least one processor device operatively coupled to the memory device and configured to execute program code stored on the memory device to:
obtain a set of annotated terms including one or more terms each annotated with a stored, partial enumeration pattern;
translate problem text into logical expressions including a set of external predicates in a formal specification using natural language processing, the formal specification including a set of rules associated with a set of external predicates;
determine whether enumerating elements of an external predicate from the set of external predicates satisfies the stored, partial enumeration pattern, annotate the external predicate responsive to a determination that enumerating elements of the external predicate satisfies the stored, partial enumeration pattern, and store relations between two or more external predicates from the set of external predicates; and
generate a computer program by converting the logical expressions into computable terms by synthesizing one or more terms satisfying the set of rules of the formal specification based on the set of annotated terms using existing terms, the synthesizing the one or more terms satisfying the set of rules comprising:
assigning each predicate P in the formal specification with a term T annotated with an enumeration pattern using the predicate P to obtain a term combination, and checking that the term combination satisfies a logical formula by using enumeration patterns annotated to the assigned terms;
generating first realization statements by assigning realization types and terms to each predicate P based on an interpretation procedure, the interpretation procedure comprising applying one or more interpretation rules defining how to infer the first realization statements; and generating second realization statements by merging literals or realization statements for literals in each rule of the set of rules based on the interpretation procedure; and wherein
the one or more interpretation rules in the interpretation procedure include an interpretation rule V-V for generating two possible realization statements.