This presentation details the design of a type-directed fuzzer for TVM Relay that creates programs by recursively generating and solving type relations. Part of this work entailed formalizing Relay’s type relations, which were deliberately left opaque to the type system in the initial presentation of Relay. We include approaches that, like past work, encode Relay typing rules (along with type relations) in a logical solver domain and use that to generate valid types, as well as a “sampling” approach that is able to randomly generate valid solutions to individual type relations without a solver and use those to generate complete programs. Such an approach could be employed to easily and largely automatically extend the current testing for Relay while also serving as an executable specification.
