代码大模型 / AI 编程

Generation of Compiler Backends from Formal Models of Hardware

Gus Henry Smith

专题命中 程序分析与验证 ：code generation(abstract)；program synthesis(abstract)；分类 cs.PL

Comments PhD thesis

Unleashing the Power of Compiler Intermediate Representation to Enhance Neural Program Embeddings

Zongjie Li, Pingchuan Ma, Huaijin Wang, Shuai Wang, Qiyi Tang, Sen Nie, Shi Wu

专题命中 程序分析与验证 ：program repair(abstract)；program synthesis(abstract)；分类 cs.SE

Type- and Content-Driven Synthesis of SQL Queries from Natural Language

Navid Yaghmazadeh, Yuepeng Wang, Isil Dillig, Thomas Dillig

专题命中 程序分析与验证 ：program repair(abstract)；program synthesis(abstract)；分类 cs.PL

Generative Compilation: On-the-Fly Compiler Feedback as AI Generates Code

生成式编译：人工智能生成代码时的即时编译器反馈

Niels Mündler-Sasahara, Hristo Venev, Dawn Song, Martin Vechev, Jingxuan He

机构 * ETH Zurich（苏黎世联邦理工学院） ； Sofia University ``St. Kliment Ohridski''（索菲亚大学） ； University of California, Berkeley（加州大学伯克利分校） 纠错

专题命中 程序分析与验证 ：repository(abstract)；分类 cs.AI、cs.LG、cs.PL

AI总结 研究针对人工智能生成代码时的问题，提出生成式编译方法，核心是sealor技术，能在生成中获取编译器反馈，在Rust编码任务中评估，减少非编译输出、提高功能正确性，使编译器在生成阶段发挥更重要作用。

Magellan: Autonomous Discovery of Novel Compiler Optimization Heuristics with AlphaEvolve

Magellan：利用AlphaEvolve自主发现新型编译器优化启发式方法

Hongzheng Chen, Alexander Novikov, Ngân Vũ, Hanna Alam, Zhiru Zhang, Aiden Grossman, Mircea Trofin, Amir Yazdanbakhsh

机构 * Google（谷歌） ； Google DeepMind（谷歌DeepMind） ； Cornell University（康奈尔大学） 纠错

专题命中 程序分析与验证 ：coding agent(abstract)；分类 cs.AI、cs.LG、cs.PL

AI总结 Magellan通过AlphaEvolve自主发现新型编译器优化启发式方法，提升编译器优化效率与性能。

Comments Accepted to C4ML@CGO'26

TypyBench: Evaluating LLM Type Inference for Untyped Python Repositories

Honghua Dong, Jiacheng Yang, Xun Deng, Yuhe Jiang, Gennady Pekhimenko, Fan Long, Xujie Si

机构 * University of Toronto（多伦多大学） ； Vector Institute（向量研究所） ； CIFAR AI Chair（CIFAR人工智能主席） 纠错

专题命中 程序分析与验证 ：repository(abstract)；分类 cs.SE、cs.AI、cs.PL

Journal ref Proceedings of the 42nd International Conference on Machine Learning, Vancouver, Canada. PMLR 267, 2025

miniCTX: Neural Theorem Proving with (Long-)Contexts

Jiewen Hu, Thomas Zhu, Sean Welleck

专题命中 程序分析与验证 ：repository(abstract)；分类 cs.CL、cs.AI、cs.LG

Comments Project page: https://cmu-l3.github.io/minictx

FlakyFix: Using Large Language Models for Predicting Flaky Test Fix Categories and Test Code Repair

Sakina Fatima, Hadi Hemmati, Lionel Briand

专题命中 程序分析与验证 ：code model(abstract)；分类 cs.SE、cs.AI、cs.LG

Comments 26 pages, 20 Figures

Journal ref IEEE Transactions on Software Engineering (TSE) (2024) 1-26

WhiteFox: White-Box Compiler Fuzzing Empowered by Large Language Models

Chenyuan Yang, Yinlin Deng, Runyu Lu, Jiayi Yao, Jiawei Liu, Reyhaneh Jabbarvand, Lingming Zhang

专题命中 程序分析与验证 ：code generation(abstract)；分类 cs.SE、cs.LG、cs.PL

Comments Published in OOPSLA 2024

Journal ref Proc. ACM Program. Lang., Vol. 8, No. OOPSLA2, Article 296. Publication date: October 2024

FVEL: Interactive Formal Verification Environment with Large Language Models via Theorem Proving

Xiaohan Lin, Qingxing Cao, Yinya Huang, Haiming Wang, Jianqiao Lu, Zhengying Liu, Linqi Song, Xiaodan Liang

专题命中 程序分析与验证 ：program synthesis(abstract)；分类 cs.CL、cs.AI、cs.LG

Autoformalization with Large Language Models

Yuhuai Wu, Albert Q. Jiang, Wenda Li, Markus N. Rabe, Charles Staats, Mateja Jamnik, Christian Szegedy

专题命中 程序分析与验证 ：program synthesis(abstract)；分类 cs.SE、cs.AI、cs.LG

Comments 44 pages

Example-based Synthesis of Static Analysis Rules

Pranav Garg, Srinivasan Sengamedu SHS

专题命中 程序分析与验证 ：program synthesis(abstract)；分类 cs.SE、cs.AI、cs.PL

Type-driven Neural Programming by Example

Kiara Grouwstra

专题命中 程序分析与验证 ：program synthesis(abstract)；分类 cs.SE、cs.AI、cs.PL

Compiler Testing With Relaxed Memory Models

Luke Geeson, Lee Smith

专题命中 程序分析与验证 ：code generation(abstract,comments)；分类 cs.SE、cs.PL

Comments 12 pages, Accepted to IEEE/ACM International Symposium on Code Generation and Optimization

GitSkills: A Dataset of Agent Skills on GitHub

GitSkills：GitHub上的智能体技能数据集

Giuseppe Destefanis, Daniel Graziotin, Matteo Vaccargiu, Marco Ortu

专题命中 程序分析与验证 ：repository(abstract)；分类 cs.SE、cs.AI

AI总结 本文提出GitSkills数据集，包含从28.22万个公开GitHub代码库收集的379.7117万个智能体技能相关文件，为智能体技能的多维度研究提供了数据支撑。

Comments Giuseppe Destefanis, Daniel Graziotin, Matteo Vaccargiu, and Marco Ortu. 2027. GitSkills: A Dataset of Agent Skills on GitHub. In Proceedings of the 24th International Conference on Mining Software Repositories (MSR '27). Association for Computing Machinery, New York, NY, USA, 3 pages. To appear

FVRuleLearner: Operator-Level Reasoning Tree (Op-Tree)-Based Rules Learning for Formal Verification

FVRuleLearner：基于操作级推理树（OP-Tree）的规则学习用于形式验证

Lily Jiaxin Wan, Chia-Tung Ho, Yunsheng Bai, Cunxi Yu, Ghaith Bany Hamad, Deming Chen, Haoxing Ren

机构 * University of Illinois Urbana-Champaign（伊利诺伊大学厄巴纳-香槟分校） ； NVIDIA（英伟达） ； University of Maryland, College Park（马里兰大学帕克分校） 纠错

专题命中 程序分析与验证 ：code generation(abstract)；分类 cs.SE、cs.AI

AI总结 本文提出FVRuleLearner，通过操作级推理树模型，提升形式验证中SVA操作符选择的准确性和效率，显著提高语法和功能正确性。

Comments Accepted to IEEE VTS'26

Finding and Understanding Miscompilation Bugs in the Solidity Compiler

在Solidity编译器中发现并理解错误编译漏洞

Bhargava Shastry

专题命中 程序分析与验证 ：code generation(abstract)；分类 cs.SE、cs.PL

AI总结 研究旨在提高Solidity编译器质量，创建SolSmith工具。通过生成有效测试程序使编译器测试更严格，发现25个错误编译漏洞。还对这些漏洞进行定性和定量分析，揭示优化编译器的陷阱，为智能合约及用户减少潜在风险。

Comments 16 pages, 7 figures, 4 tables

Understanding Agent-Based Patching of Compiler Missed Optimizations

理解基于智能体的编译器遗漏优化补丁

Batu Guan, Zirui Wang, Shaohua Li

专题命中 程序分析与验证 ：coding agent(abstract)；分类 cs.SE、cs.AI

AI总结 研究智能体如何为编译器遗漏优化打补丁，发现关键挑战在于泛化而非仅修复报告案例，提出历史知识增强技术以提升泛化能力。

Comments 11 pages, 10 figures

Mining Architectural Quality Under Agentic AI Adoption: A Causal Study of Java Repositories

在智能体AI采用下的架构质量挖掘：Java仓库的因果研究

Oliver Aleksander Larsen, Mahyar T. Moghaddam

机构 * SDU Software Engineering, University of Southern Denmark（SDU软件工程，丹麦南部大学） 纠错

专题命中 程序分析与验证 ：repository(abstract)；分类 cs.SE、cs.AI

AI总结 通过差分差分设计和Borusyak插值估计器，研究智能体AI工具采用对Java仓库架构气味密度（ASD）的因果影响，发现ASD下降6.7%源于代码量增长，而非架构改进。

Comments 16 pages. Accepted for presentation at the 52nd Euromicro Conference on Software Engineering and Advanced Applications (SEAA) 2026, Krakow, Poland, 2-4 September 2026, and for publication in the Springer LNCS proceedings. This is the author's accepted manuscript

Automating Formal Verification with Reinforcement Learning and Recursive Inference

用强化学习和递归推理自动化形式验证

Max Tan

机构 * Department of Electrical Engineering and Computer Science（电气工程与计算机科学系） ； Massachusetts Institute of Technology（麻省理工学院） 纠错

专题命中 程序分析与验证 ：repository(abstract)；分类 cs.SE、cs.LG

AI总结 研究通过可验证奖励的强化学习和验证器引导的推理搜索，提升大语言模型生成验证程序和证明的能力，在Dafny和Lean上取得显著进展。

Comments Master's thesis, 140 pages, 16 figures, 17 tables

LLM Translation of Compiler Intermediate Representation

编译器中间表示的大型语言模型翻译

Andrea Valenzuela Ramirez, Cristian Gutierrez-Gomez, Marta Barroso, Dario Garcia-Gasulla, Sara Royuela

机构 * Barcelona Supercomputing Center, Universitat Politècnica de Catalunya（巴塞罗那超级计算中心，加泰罗尼亚理工大学） ； Barcelona Supercomputing Center（巴塞罗那超级计算中心） 纠错

专题命中 程序分析与验证 ：code generation(abstract)；分类 cs.AI、cs.PL

AI总结 本文提出IRIS-14B模型，通过训练实现GIMPLE到LLVM IR的翻译，展示了大型语言模型在编译器中间表示转换中的高效性与准确性。

PolyBlocks: A Compiler Infrastructure for AI Chips and Programming Frameworks

PolyBlocks：面向AI芯片和编程框架的编译器基础设施

Uday Bondhugula, Akshay Baviskar, Navdeep Katel, Vimal Patel, Anoop JS, Arnab Dutta

机构 * Polymage Labs（Polymage实验室） ； Indian Institute of Science（印度科学研究院） 纠错

专题命中 程序分析与验证 ：code generation(abstract)；分类 cs.LG、cs.PL

AI总结 PolyBlocks是一种基于MLIR的编译器基础设施，通过自动代码生成和优化，实现AI编程框架到AI芯片的高效转换。

Comments Fixed the "Acknowledgments" section that was missing phrases

Agint: Agentic Graph Compilation for Software Engineering Agents

Agint：软件工程代理的代理图编译

Abhi Chivukula, Jay Somasundaram, Vijay Somasundaram

专题命中 程序分析与验证 ：coding agent(abstract)；分类 cs.SE、cs.LG

AI总结 Agint通过代理图编译器和运行时实现高效、可靠的软件工程代理，支持自然语言到代码的自动化转换与协作开发。

Comments 18 pages, 5 figures, NeurIPS 2025: Deep Learning for Code in the Agentic Era

Towards Formal Verification of LLM-Generated Code from Natural Language Prompts

向自然语言提示生成的LLM代码形式验证

Aaron Councilman, David Jiahao Fu, Aryan Gupta, Chengxiao Wang, David Grove, Yu-Xiong Wang, Vikram Adve

机构 * University of Illinois at Urbana-Champaign（伊利诺伊大学厄巴纳-香槟分校） ； IBM Research（IBM研究院） 纠错

专题命中 程序分析与验证 ：code generation(abstract)；分类 cs.AI、cs.PL

AI总结 Astrogator通过形式查询语言和知识库实现对LLM生成代码的正确性验证，验证准确率达83%。

Comments 28 pages, 10 figures

Towards Verified Code Reasoning by LLMs

Meghana Sistla, Gogul Balakrishnan, Pat Rondon, José Cambronero, Michele Tufano, Satish Chandra

机构 * University of Texas at Austin（德克萨斯大学奥斯汀分校） ； Google DeepMind（谷歌DeepMind） ； Google（谷歌） ； Meta Platforms（元平台） 纠错

专题命中 程序分析与验证 ：code generation(abstract)；分类 cs.SE、cs.LG

Comments 43 pages

Local Success Does Not Compose: Benchmarking Large Language Models for Compositional Formal Verification

Xu Xu, Xin Li, Xingwei Qu, Jie Fu, Binhang Yuan

机构 * Shanghai AI Lab（上海人工智能实验室） 纠错

专题命中 程序分析与验证 ：code generation(abstract)；分类 cs.AI、cs.PL

Automated Code Repair for C/C++ Static Analysis Alerts

David Svoboda, Lori Flynn, William Klieber, Michael Duggan, Nicholas Reimer, Joseph Sible

专题命中 程序分析与验证 ：program repair(abstract)；分类 cs.SE、cs.PL

Training Language Models to Generate Quality Code with Program Analysis Feedback

Feng Yao, Zilong Wang, Liyuan Liu, Junxia Cui, Li Zhong, Xiaohan Fu, Haohui Mai, Vish Krishnan, Jianfeng Gao, Jingbo Shang

机构 * University of California, San Diego（加州大学圣迭戈分校） ； Microsoft Research（微软研究院） ； CausalFlow Inc.（CausalFlow公司） 纠错

专题命中 程序分析与验证 ：code generation(abstract)；分类 cs.CL、cs.AI

Comments 10 pages, 3 figures

Show Me Your Code! Kill Code Poisoning: A Lightweight Method Based on Code Naturalness

Weisong Sun, Yuchen Chen, Mengzhe Yuan, Chunrong Fang, Zhenpeng Chen, Chong Wang, Yang Liu, Baowen Xu, Zhenyu Chen

专题命中 程序分析与验证 ：code model(abstract)；分类 cs.SE、cs.AI

Comments Accepted to the 47th International Conference on Software Engineering (ICSE 2025)

Exploiting Code Symmetries for Learning Program Semantics

Kexin Pei, Weichen Li, Qirui Jin, Shuyang Liu, Scott Geng, Lorenzo Cavallaro, Junfeng Yang, Suman Jana

专题命中 程序分析与验证 ：code model(abstract)；分类 cs.LG、cs.PL