Abstract
Numbers are one of the most widely used data type in programming languages. Number transformations like formatting and rounding present a challenge even for experienced programmers as they find it difficult to remember different number format strings supported by different programming languages. These transformations present an even bigger challenge for end-users of spreadsheet systems like Microsoft Excel where providing such custom format strings is beyond their expertise. In our extensive case study of help forums of many programming languages and Excel, we found that both programmers and end-users struggle with these number transformations, but are able to easily express their intent using input-output examples.
In this paper, we present a framework that can learn such number transformations from very few input-output examples. We first describe an expressive number transformation language that can model these transformations, and then present an inductive synthesis algorithm that can learn all expressions in this language that are consistent with a given set of examples. We also present a ranking scheme of these expressions that enables efficient learning of the desired transformation from very few examples. By combining our inductive synthesis algorithm for number transformations with an inductive synthesis algorithm for syntactic string transformations, we are able to obtain an inductive synthesis algorithm for manipulating data types that have numbers as a constituent sub-type such as date, unit, and time. We have implemented our algorithms as an Excel add-in and have evaluated it successfully over several benchmarks obtained from the help forums and the Excel product team.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Bryant, R.E.: Graph-based algorithms for boolean function manipulation. IEEE Trans. Computers 35(8), 677–691 (1986)
Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: POPL (1977)
Cypher, A. (ed.): Watch What I Do – Programming by Demonstration. MIT Press (1993)
Gualtieri, M.: Deputize end-user developers to deliver business agility and reduce costs. Forrester Report for Application Development and Program Management Professionals (April 2009)
Gulwani, S.: Dimensions in program synthesis. In: PPDP (2010)
Gulwani, S.: Automating string processing in spreadsheets using input-output examples. In: POPL (2011)
Gulwani, S.: Synthesis from examples. In: WAMBSE (Workshop on Advances in Model-Based Software Engineering) Special Issue, Infosys Labs Briefings, vol. 10(2) (2012)
Gulwani, S., Harris, W.R., Singh, R.: Spreadsheet data manipulation using examples. Communications of the ACM (to appear, 2012)
Gulwani, S., Jha, S., Tiwari, A., Venkatesan, R.: Synthesis of loop-free programs. In: PLDI (2011)
Gulwani, S., Korthikanti, V.A., Tiwari, A.: Synthesizing geometry constructions. In: PLDI, pp. 50–61 (2011)
Gvero, T., Kuncak, V., Piskac, R.: Interactive Synthesis of Code Snippets. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 418–423. Springer, Heidelberg (2011)
Harris, W.R., Gulwani, S.: Spreadsheet table transformations from examples. In: PLDI, pp. 317–328 (2011)
Itzhaky, S., Gulwani, S., Immerman, N., Sagiv, M.: A simple inductive synthesis methodology and its applications. In: OOPSLA (2010)
Jha, S., Gulwani, S., Seshia, S., Tiwari, A.: Oracle-guided component-based program synthesis. In: ICSE (2010)
Kandel, S., Paepcke, A., Hellerstein, J., Heer, J.: Wrangler: Interactive visual specification of data transformation scripts. In: CHI (2011)
Lau, T.: Why PBD systems fail: Lessons learned for usable AI. In: CHI Workshop on Usable AI (2008)
Lau, T., Wolfman, S., Domingos, P., Weld, D.: Programming by demonstration using version space algebra. Machine Learning 53(1-2), 111–156 (2003)
Miller, R.C., Myers, B.A.: Interactive simultaneous editing of multiple text regions. In: USENIX Annual Technical Conference (2001)
Perelman, D., Gulwani, S., Ball, T., Grossman, D.: Type-directed completion of partial expressions. In: PLDI (2012)
Scaffidi, C., Myers, B.A., Shaw, M.: Topes: reusable abstractions for validating data. In: ICSE, pp. 1–10 (2008)
Singh, R., Gulwani, S.: Learning Semantic String Transformations from Examples. PVLDB 5(8), 740–751 (2012), http://vldb.org/pvldp/vol5/p740_rishabhsingh_vldp2012.pdf
Singh, R., Gulwani, S.: Synthesizing number transformations from input-output examples. Technical Report MSR-TR-2012-42 (April 2012)
Singh, R., Gulwani, S., Rajamani, S.: Automatically generating algebra problems. In: AAAI (to appear, 2012)
Singh, R., Solar-Lezama, A.: Synthesizing data structure manipulations from storyboards. In: SIGSOFT FSE, pp. 289–299 (2011)
Solar-Lezama, A., Jones, C.G., BodÃk, R.: Sketching concurrent data structures. In: PLDI, pp. 136–148 (2008)
Solar-Lezama, A., Rabbah, R.M., BodÃk, R., Ebcioglu, K.: Programming by sketching for bit-streaming programs. In: PLDI, pp. 281–294 (2005)
Srivastava, S., Gulwani, S., Chaudhuri, S., Foster, J.S.: Path-based inductive synthesis for program inversion. In: PLDI (2011)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Singh, R., Gulwani, S. (2012). Synthesizing Number Transformations from Input-Output Examples. In: Madhusudan, P., Seshia, S.A. (eds) Computer Aided Verification. CAV 2012. Lecture Notes in Computer Science, vol 7358. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-31424-7_44
Download citation
DOI: https://doi.org/10.1007/978-3-642-31424-7_44
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-31423-0
Online ISBN: 978-3-642-31424-7
eBook Packages: Computer ScienceComputer Science (R0)