Learning-aided Program Reasoning

学习辅助程序推理

• 批准号: RGPIN-2021-03537
• 负责人: Si, Xujie
• 金额: $ 2.11万
• 依托单位: University of Toronto
• 依托单位国家: 加拿大
• 项目类别: Discovery Grants Program - Individual
• 财政年份: 2022
• 资助国家: 加拿大
• 起止时间: 2022-01-01 至 2023-12-31
• 项目状态: 已结题
• 来源: https://www.nserc-crsng.gc.ca/ase-oro/Details-Detailles_eng.asp?id=750386
• 关键词: Learning; aided; Program; Reasoning

Software forms the cornerstone of our modern digital world. However, developing reliable software is notoriously challenging. An inadvertent programming mistake (e.g. Heartbleed bug) could make millions of web servers vulnerable. To systematically eliminate software vulnerabilities, many program reasoning tools have been developed by research communities and industrial labs. Unfortunately, in order to achieve a usable accuracy and scalability, these program reasoning tools have to be carefully customized for each codebase, which requires non-trivial expertise, limiting their adoption by average software developers. Training (or simply recruiting) highly-skilled programmers, in other words, "human learning", is the conventional and industrial way to mitigate these issues, which is however slow, expensive, and non-scalable. The proposed program aims to develop an economical, scalable and easily accessible approach, which can assist hundreds of thousands of real-world programmers at once. The key insight is to make the programming environment itself actively learn from past executions, mistakes, patches, historical versions, and other similar software repositories. The main goal of this program is to investigate how machine learning, or more generally artificial intelligence (AI), can help to improve programming reasoning in various stages of software development. We will design and build an intelligent programming assistant, which learns from large software repositories, catches various mistakes and suggests idioms and patches on the fly, and which replaces manually designed heuristics or rules for analysis and testing with learnable components that gradually adapt to given codebase overtime. Particularly, the proposed program will focus on three objectives: 1) improving syntactic-level reasoning by mining idioms and specifications, 2) improving static reasoning by learning rules and relaxing rules with numerical weights; 3) improving dynamic reasoning by learning an effective neural-policy guiding dynamic symbolic execution. The proposed research will significantly advance state-of-the-art programming reasoning techniques and the resulting toolchain will be freely available and easily accessible to average software developers. This program will train 10 Highly Qualified Personnel (HQP), including 2 PhDs, 3 MSc and 5 undergraduate students, in the interdisciplinary areas of programming languages, software engineering, and machine learning. HQP will gain hands-on experience of building a "big code" processing pipeline, designing program analysis and synthesis algorithms and machine learning models, developing practical software analysis and testing toolchain, and conducting user studies and large-scale evaluations. These skills form a solid background for HQP to achieve great successes in the interdisciplinary area of research as well as software industry.

软件构成了现代数字世界的基石。然而，开发可靠的软件是出了名的具有挑战性。无意的编程错误（例如 Heartbleed bug）可能会使数百万网络服务器容易受到攻击。为了系统地消除软件漏洞，研究团体和工业实验室开发了许多程序推理工具。不幸的是，为了实现可用的准确性和可扩展性，这些程序推理工具必须针对每个代码库进行仔细定制，这需要大量的专业知识，从而限制了普通软件开发人员的采用。培训（或简单地招募）高技能程序员，换句话说，“人类学习”，是缓解这些问题的传统工业方法，但速度慢、成本高且不可扩展。该计划旨在开发一种经济、可扩展且易于访问的方法，可以同时帮助数十万现实世界的程序员。关键的见解是让编程环境本身主动从过去的执行、错误、补丁、历史版本和其他类似的软件存储库中学习。 该项目的主要目标是研究机器学习，或更普遍的人工智能 (AI) 如何帮助改进软件开发各个阶段的编程推理。我们将设计和构建一个智能编程助手，它可以从大型软件存储库中学习，捕获各种错误并即时建议惯用语和补丁，并用逐渐适应给定代码库的可学习组件来取代手动设计的启发式或分析和测试规则。特别是，所提出的计划将重点关注三个目标：1）通过挖掘习语和规范来改进句法级推理，2）通过学习规则和用数字权重放松规则来改进静态推理； 3）通过学习指导动态符号执行的有效神经策略来提高动态推理。 拟议的研究将显着推进最先进的编程推理技术，并且由此产生的工具链将免费提供并可供普通软件开发人员轻松访问。该项目将在编程语言、软件工程和机器学习等跨学科领域培养10名高素质人才（HQP），其中包括2名博士、3名硕士和5名本科生。 HQP将获得构建“大代码”处理管道、设计程序分析综合算法和机器学习模型、开发实用软件分析和测试工具链、进行用户研究和大规模评估的实践经验。这些技能为 HQP 在跨学科研究领域以及软件行业取得巨大成功奠定了坚实的背景。