Learning-aided Program Reasoning

学习辅助程序推理

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

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