{"id":890049,"date":"2022-11-17T11:25:36","date_gmt":"2022-11-17T19:25:36","guid":{"rendered":"https:\/\/www.microsoft.com\/en-us\/research\/?post_type=msr-project&#038;p=890049"},"modified":"2024-10-23T15:47:00","modified_gmt":"2024-10-23T22:47:00","slug":"trusted-ai-assisted-programming","status":"publish","type":"msr-project","link":"https:\/\/www.microsoft.com\/en-us\/research\/project\/trusted-ai-assisted-programming\/","title":{"rendered":"Trusted AI-assisted Programming"},"content":{"rendered":"<section class=\"mb-3 moray-highlight\">\n\t<div class=\"card-img-overlay mx-lg-0\">\n\t\t<div class=\"card-background  has-background-auburn card-background--full-bleed\">\n\t\t\t\t\t<\/div>\n\t\t<!-- Foreground -->\n\t\t<div class=\"card-foreground d-flex mt-md-n5 my-lg-5 px-g px-lg-0\">\n\t\t\t<!-- Container -->\n\t\t\t<div class=\"container d-flex mt-md-n5 my-lg-5 \">\n\t\t\t\t<!-- Card wrapper -->\n\t\t\t\t<div class=\"w-100 w-lg-col-5\">\n\t\t\t\t\t<!-- Card -->\n\t\t\t\t\t<div class=\"card material-md-card py-5 px-md-5\">\n\t\t\t\t\t\t<div class=\"card-body \">\n\t\t\t\t\t\t\t\n\t\t\t\t\t\t\t\n\n<h2 class=\"wp-block-heading\" id=\"trusted-ai-assisted-programming\">Trusted AI-assisted Programming<\/h2>\n\n\n\n<p><\/p>\n\n\t\t\t\t\t\t<\/div>\n\t\t\t\t\t<\/div>\n\t\t\t\t<\/div>\n\t\t\t<\/div>\n\t\t<\/div>\n\t<\/div>\n<\/section>\n\n\n\n\n\n<p>Machine learning, in particular Large Language Models, has shown great promise at automating several aspects of programming and software development such as coding, testing, integration, static analysis, verification etc. in recent years. In this project, we leverage and extend large language models with ideas grounded in programming languages and correctness to develop trusted AI agents for all aspects of programming for reliable software development.<\/p>\n\n\n\n<p>Current work explores various directions:<\/p>\n\n\n\n<h4 class=\"wp-block-heading\" id=\"ai-for-program-specifications\">AI for program specifications<\/h4>\n\n\n\n<p>We study the problem of<em> user-intent formalization<\/em> (<a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" href=\"https:\/\/pnwplse.org\/slides\/2024\/Shuvendu%20Lahiri.pdf\">high-level deck<span class=\"sr-only\"> (opens in new tab)<\/span><\/a>) to derive formal specifications from informal requirements, and applications towards developing correct software. Some results<\/p>\n\n\n\n<ul class=\"wp-block-list\">\n<li><em>Test (oracle) generation <\/em>to find functional bugs in <a href=\"https:\/\/www.microsoft.com\/en-us\/research\/publication\/toga-a-neural-method-for-test-oracle-generation\/\">TOGA<\/a><\/li>\n\n\n\n<li>Test-driven <em>interactive <\/em>intent-formalization for improving accuracy and explainability of code generation in <a href=\"https:\/\/www.microsoft.com\/en-us\/research\/publication\/interactive-code-generation-via-test-driven-user-intent-formalization\/\">TiCoder<\/a><\/li>\n\n\n\n<li>Generating program specifications from natural language as in <a href=\"https:\/\/www.microsoft.com\/en-us\/research\/publication\/formalizing-natural-language-intent-into-program-specifications-via-large-language-models\/\">nl2postcond<\/a><\/li>\n\n\n\n<li>Symbolically testing specifications for correctness using program verifiers <a href=\"https:\/\/www.microsoft.com\/en-us\/research\/publication\/evaluating-llm-driven-user-intent-formalization-for-verification-aware-languages\/\">Evaluating LLM-driven User-Intent Formalization for Verification-Aware Languages &#8211; Microsoft Research<\/a><\/li>\n\n\n\n<li>Instantiating these ideas for security-critical domains such as verified parser generation from RFC descriptions in <a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" href=\"https:\/\/arxiv.org\/abs\/2404.10362\">3DGen<span class=\"sr-only\"> (opens in new tab)<\/span><\/a>.<\/li>\n<\/ul>\n\n\n\n<h4 class=\"wp-block-heading\" id=\"ai-for-proof-synthesis-and-proof-oriented-programming\">AI for proof synthesis and proof-oriented programming<\/h4>\n\n\n\n<p>We explore program proof automation using neural techniques including (a) improving LLMs ability to generate correct loop invariants by neurally ranking LLM-generated loop invariants in <a href=\"https:\/\/www.microsoft.com\/en-us\/research\/publication\/ranking-llm-generated-loop-invariants-for-program-verification\/\"><strong>iRank<\/strong><span class=\"sr-only\"> (opens in new tab)<\/span><\/a>, and (b) creating large-scale dataset and fine-tuned models for <a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" href=\"https:\/\/arxiv.org\/abs\/2405.01787\">proof automation for proof-oriented programming (PoPAI)<span class=\"sr-only\"> (opens in new tab)<\/span><\/a><strong><a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" href=\"https:\/\/arxiv.org\/abs\/2405.01787\"> <span class=\"sr-only\"> (opens in new tab)<\/span><\/a><\/strong>in languages such as F*.<\/p>\n\n\n\n<h4 class=\"wp-block-heading\" id=\"others\">Others<\/h4>\n\n\n\n<p>Previous works include fine-tuning large language models on test execution data to predict runtime faults for generated code in <strong><a href=\"https:\/\/www.microsoft.com\/en-us\/research\/publication\/fault-aware-neural-code-rankers\/\">CodeRanker<\/a><\/strong>, and <strong>improving search-based test generation with LLMs<\/strong> in <a href=\"https:\/\/www.microsoft.com\/en-us\/research\/publication\/codamosa-escaping-coverage-plateaus-in-test-generation-with-pre-trained-large-language-models\/\"><strong>CodaMOSA<\/strong><\/a>.<\/p>\n\n\n","protected":false},"excerpt":{"rendered":"<p>Machine learning, in particular Large Language Models, has shown great promise at automating several aspects of programming and software development such as coding, testing, integration, static analysis, verification etc. in recent years. In this project, we leverage and extend large language models with ideas grounded in programming languages and correctness to develop trusted AI agents [&hellip;]<\/p>\n","protected":false},"featured_media":0,"template":"","meta":{"msr-url-field":"","msr-podcast-episode":"","msrModifiedDate":"","msrModifiedDateEnabled":false,"ep_exclude_from_search":false,"_classifai_error":"","footnotes":""},"research-area":[13556,13560],"msr-locale":[268875],"msr-impact-theme":[],"msr-pillar":[],"class_list":["post-890049","msr-project","type-msr-project","status-publish","hentry","msr-research-area-artificial-intelligence","msr-research-area-programming-languages-software-engineering","msr-locale-en_us","msr-archive-status-active"],"msr_project_start":"2022-09-01","related-publications":[879321,1087500,1094508,885843,925401,976782,976788,841948,1057761,1057767,1084344],"related-downloads":[1087350,1087356],"related-videos":[],"related-groups":[],"related-events":[],"related-opportunities":[],"related-posts":[],"related-articles":[],"tab-content":[],"slides":[],"related-researchers":[{"type":"user_nicename","display_name":"Saikat Chakraborty","user_id":42411,"people_section":"Section name 0","alias":"saikatc"},{"type":"user_nicename","display_name":"Gabriel Ebner","user_id":42573,"people_section":"Section name 0","alias":"gabrielebner"},{"type":"user_nicename","display_name":"Sarah Fakhoury","user_id":42180,"people_section":"Section name 0","alias":"sfakhoury"},{"type":"user_nicename","display_name":"Jianfeng Gao","user_id":32246,"people_section":"Section name 0","alias":"jfgao"},{"type":"user_nicename","display_name":"Jeevana Priya Inala","user_id":41377,"people_section":"Section name 0","alias":"jinala"},{"type":"user_nicename","display_name":"Markus Kuppe","user_id":32784,"people_section":"Section name 0","alias":"makuppe"},{"type":"user_nicename","display_name":"Shuvendu Lahiri","user_id":33640,"people_section":"Section name 0","alias":"shuvendu"},{"type":"user_nicename","display_name":"Madan Musuvathi","user_id":32766,"people_section":"Section name 0","alias":"madanm"},{"type":"user_nicename","display_name":"Tahina Ramananandro","user_id":36293,"people_section":"Section name 0","alias":"taramana"},{"type":"user_nicename","display_name":"Nikhil Swamy","user_id":33138,"people_section":"Section name 0","alias":"nswamy"},{"type":"user_nicename","display_name":"Chenglong Wang","user_id":41251,"people_section":"Section name 0","alias":"chenwang"}],"msr_research_lab":[199565],"msr_impact_theme":[],"_links":{"self":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-project\/890049"}],"collection":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-project"}],"about":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/types\/msr-project"}],"version-history":[{"count":28,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-project\/890049\/revisions"}],"predecessor-version":[{"id":1096872,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-project\/890049\/revisions\/1096872"}],"wp:attachment":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/media?parent=890049"}],"wp:term":[{"taxonomy":"msr-research-area","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/research-area?post=890049"},{"taxonomy":"msr-locale","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-locale?post=890049"},{"taxonomy":"msr-impact-theme","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-impact-theme?post=890049"},{"taxonomy":"msr-pillar","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-pillar?post=890049"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}