SHF: Medium: Collaborative Research: Marrying program analysis and numerical search

SHF：媒介：协作研究：结合程序分析和数值搜索

• 批准号: 1161775
• 负责人: Armando Solar-Lezama
• 金额: $ 60万
• 依托单位: Massachusetts Institute of Technology
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 2012
• 资助国家: 美国
• 起止时间: 2012-09-01 至 2016-08-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1161775&HistoricalAwards=false
• 关键词: SHF; Medium; Collaborative; Research; Marrying

This research project explores ways to solve optimization problems where the targets of optimization are programs containing general-purpose control and data constructs. Such optimization questions arise often in the everyday practice of software engineering. While it may seem that standard optimization packages could solve these problems, it is often not so. White-box optimization approaches like linear programming are ruled out here because they only permit very restricted classes of objective functions. Black-box optimization techniques like gradient descent and Nelder-Mead search are applicable in principle, but they work well only in relatively smooth search spaces, and due to arbitrarily nested branches and loops, even simple programs can have highly irregular, ill-conditioned behavior.The central insight guiding this project is that program analysis techniques from the field of formal reasoning about programs can work together with blackbox optimization toolkits, and make it possible to solve many more problems of the above sort than are currently possible. Ultimately, the project will produce a unified system for optimizing programs that can leverage flexible combinations of optimization techniques and program analysis strategies. As numerous real-world problems faced in the development of everyday software are optimization problems, this system will offer a new range of capabilities to the end programmer. In addition, the research will foster synergy between two different research areas customarily housed in different academic departments.

该研究项目探讨了解决优化问题的方法，其中优化目标是包含通用控制和数据构建的程序。这种优化问题经常在软件工程的日常练习中出现。虽然标准优化软件包似乎可以解决这些问题，但通常不是这样。在这里排除了诸如线性编程之类的白盒优化方法，因为它们仅允许非常有限的目标功能类别。黑盒优化技术原则上适用于梯度下降和Nelder-Mead搜索，但它们仅在相对平稳的搜索空间中效果很好，并且由于任意嵌套的分支和循环，即使是简单的程序，甚至简单的程序也可以具有高度不规则的，不规则的条件行为。中心洞察力指导该计划的功能更加出色，可以使该计划的功能与正式的盒子相处，使得与正式的盒子相处融合了，使其具有正式化的作用，使其成为正式的工具。上面排序比目前可能的。最终，该项目将生成一个统一的系统，以优化可以利用优化技术和程序分析策略的灵活组合的程序。由于日常软件开发中面临的许多现实世界问题都是优化问题，因此该系统将为最终程序员提供新的功能。此外，这项研究将促进在不同学术部门通常安置的两个不同研究领域之间的协同作用。