Smooth interpretation
We present smooth interpretation, a method to systematically approximate numerical imperative programs by smooth mathematical functions. This approximation facilitates the use of numerical search techniques like gradient descent for program analysis and synthesis. The method extends to programs the...
| Main Authors: | , |
|---|---|
| Other Authors: | |
| Format: | Article |
| Language: | English |
| Published: |
Association for Computing Machinery (ACM)
2020
|
| Online Access: | https://hdl.handle.net/1721.1/124688 |
| _version_ | 1826188514352431104 |
|---|---|
| author | Chaudhuri, Swarat Solar Lezama, Armando |
| author2 | Massachusetts Institute of Technology. Department of Electrical Engineering and Computer Science |
| author_facet | Massachusetts Institute of Technology. Department of Electrical Engineering and Computer Science Chaudhuri, Swarat Solar Lezama, Armando |
| author_sort | Chaudhuri, Swarat |
| collection | MIT |
| description | We present smooth interpretation, a method to systematically approximate numerical imperative programs by smooth mathematical functions. This approximation facilitates the use of numerical search techniques like gradient descent for program analysis and synthesis. The method extends to programs the notion of Gaussian smoothing, a popular signal-processing technique that filters out noise and discontinuities from a signal by taking its convolution with a Gaussian function. In our setting, Gaussian smoothing executes a program according to a probabilistic semantics; the execution of program P on an input x after Gaussian smoothing can be summarized as follows: (1) Apply a Gaussian perturbation to x - the perturbed input is a random variable following a normal distribution with mean x. (2) Compute and return the expected output of P on this perturbed input. Computing the expectation explicitly would require the execution of P on all possible inputs, but smooth interpretation bypasses this requirement by using a form of symbolic execution to approximate the effect of Gaussian smoothing on P. The result is an efficient but approximate implementation of Gaussian smoothing of programs. Smooth interpretation has the effect of attenuating features of a program that impede numerical searches of its input space - for example, discontinuities resulting from conditional branches are replaced by continuous transitions. We apply smooth interpretation to the problem of synthesizing values of numerical control parameters in embedded control applications. This problem is naturally formulated as one of numerical optimization: the goal is to find parameter values that minimize the error between the resulting program and a programmer-provided behavioral specification. Solving this problem by directly applying numerical optimization techniques is often impractical due to the discontinuities in the error function. By eliminating these discontinuities, smooth interpretation makes it possible to search the parameter space efficiently by means of simple gradient descent. Our experiments demonstrate the value of this strategy in synthesizing parameters for several challenging programs, including models of an automated gear shift and a PID controller. © 2010 Presented at PLDI '10: ACM SIGPLAN Conference on Programming Language Design and Implementation, June 2010, Toronto, Ontario. |
| first_indexed | 2024-09-23T08:00:49Z |
| format | Article |
| id | mit-1721.1/124688 |
| institution | Massachusetts Institute of Technology |
| language | English |
| last_indexed | 2024-09-23T08:00:49Z |
| publishDate | 2020 |
| publisher | Association for Computing Machinery (ACM) |
| record_format | dspace |
| spelling | mit-1721.1/1246882022-09-30T01:42:21Z Smooth interpretation Chaudhuri, Swarat Solar Lezama, Armando Massachusetts Institute of Technology. Department of Electrical Engineering and Computer Science We present smooth interpretation, a method to systematically approximate numerical imperative programs by smooth mathematical functions. This approximation facilitates the use of numerical search techniques like gradient descent for program analysis and synthesis. The method extends to programs the notion of Gaussian smoothing, a popular signal-processing technique that filters out noise and discontinuities from a signal by taking its convolution with a Gaussian function. In our setting, Gaussian smoothing executes a program according to a probabilistic semantics; the execution of program P on an input x after Gaussian smoothing can be summarized as follows: (1) Apply a Gaussian perturbation to x - the perturbed input is a random variable following a normal distribution with mean x. (2) Compute and return the expected output of P on this perturbed input. Computing the expectation explicitly would require the execution of P on all possible inputs, but smooth interpretation bypasses this requirement by using a form of symbolic execution to approximate the effect of Gaussian smoothing on P. The result is an efficient but approximate implementation of Gaussian smoothing of programs. Smooth interpretation has the effect of attenuating features of a program that impede numerical searches of its input space - for example, discontinuities resulting from conditional branches are replaced by continuous transitions. We apply smooth interpretation to the problem of synthesizing values of numerical control parameters in embedded control applications. This problem is naturally formulated as one of numerical optimization: the goal is to find parameter values that minimize the error between the resulting program and a programmer-provided behavioral specification. Solving this problem by directly applying numerical optimization techniques is often impractical due to the discontinuities in the error function. By eliminating these discontinuities, smooth interpretation makes it possible to search the parameter space efficiently by means of simple gradient descent. Our experiments demonstrate the value of this strategy in synthesizing parameters for several challenging programs, including models of an automated gear shift and a PID controller. © 2010 Presented at PLDI '10: ACM SIGPLAN Conference on Programming Language Design and Implementation, June 2010, Toronto, Ontario. 2020-04-16T14:26:22Z 2020-04-16T14:26:22Z 2010-06 2019-07-10T12:56:21Z Article http://purl.org/eprint/type/ConferencePaper 978-1-4503-0019-3 https://hdl.handle.net/1721.1/124688 Chaudhuri, Swarat and Armando Solar Lezama, "Smooth interpretation." PLDI '10: Proceedings of the 31st ACM SIGPLAN Conference on Programming Language Design and Implementation (New York, N.Y.: Association for Computing Machinery, 2010): p. 279-97 doi 10.1145/1806596.1806629 ©2010 Author(s) en 10.1145/1806596.1806629 PLDI '10: Proceedings of the 31st ACM SIGPLAN Conference on Programming Language Design and Implementation Creative Commons Attribution-Noncommercial-Share Alike http://creativecommons.org/licenses/by-nc-sa/4.0/ application/pdf Association for Computing Machinery (ACM) MIT web domain |
| spellingShingle | Chaudhuri, Swarat Solar Lezama, Armando Smooth interpretation |
| title | Smooth interpretation |
| title_full | Smooth interpretation |
| title_fullStr | Smooth interpretation |
| title_full_unstemmed | Smooth interpretation |
| title_short | Smooth interpretation |
| title_sort | smooth interpretation |
| url | https://hdl.handle.net/1721.1/124688 |
| work_keys_str_mv | AT chaudhuriswarat smoothinterpretation AT solarlezamaarmando smoothinterpretation |