代码大模型 / AI 编程

Data Overfitting for On-Device Super-Resolution with Dynamic Algorithm and Compiler Co-Design

Gen Li, Zhihao Shu, Jie Ji, Minghai Qin, Fatemeh Afghah, Wei Niu, Xiaolong Ma

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

Comments ECCV2024

Naturalness of Attention: Revisiting Attention in Code Language Models

Mootez Saad, Tushar Sharma

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

Comments Accepted at ICSE-NIER (2024) track

Constrained Training of Neural Networks via Theorem Proving

Mark Chevallier, Matthew Whyte, Jacques D. Fleuriot

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

Fast and Reliable Formal Verification of Smart Contracts with the Move Prover

David Dill, Wolfgang Grieskamp, Junkil Park, Shaz Qadeer, Meng Xu, Emma Zhong

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

HIPPODROME: Data Race Repair using Static Analysis Summaries

Andreea Costea, Abhishek Tiwari, Sigmund Chianasta, Kishore R, Abhik Roychoudhury, Ilya Sergey

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

Towards establishing formal verification and inductive code synthesis in the PLC domain

Matthias Weiß, Philipp Marks, Benjamin Maschler, Dustin White, Pascal Kesseli, Michael Weyrich

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

Comments 8 pages, 6 figures, 1 table. Accepted for publication at IEEE INDIN 2021

NPAS: A Compiler-aware Framework of Unified Network Pruning and Architecture Search for Beyond Real-Time Mobile Acceleration

Zhengang Li, Geng Yuan, Wei Niu, Pu Zhao, Yanyu Li, Yuxuan Cai, Xuan Shen, Zheng Zhan, Zhenglun Kong, Qing Jin, Zhiyu Chen, Sijia Liu, Kaiyuan Yang, Bin Ren, Yanzhi Wang, Xue Lin

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

Comments Accepted as an oral paper in the Conference on Computer Vision and Pattern Recognition (CVPR), 2021

Bring Your Own Codegen to Deep Learning Compiler

Zhi Chen, Cody Hao Yu, Trevor Morris, Jorn Tuyls, Yi-Hsiang Lai, Jared Roesch, Elliott Delaye, Vin Sharma, Yida Wang

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

MLGO: a Machine Learning Guided Compiler Optimizations Framework

Mircea Trofin, Yundi Qian, Eugene Brevdo, Zinan Lin, Krzysztof Choromanski, David Li

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

Comments First two authors are equal contributors

Multiparty Session Type-safe Web Development with Static Linearity

Jonathan King, Nicholas Ng, Nobuko Yoshida

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

Comments In Proceedings PLACES 2019, arXiv:1904.00396

Journal ref EPTCS 291, 2019, pp. 35-46

DLVM: A modern compiler infrastructure for deep learning systems

Richard Wei, Lane Schwartz, Vikram Adve

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

Synthesizing Imperative Programs from Examples Guided by Static Analysis

Sunbeom So, Hakjoo Oh

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

Comments The paper is accepted in Static Analysis Symposium (SAS) '17. The submission version is somewhat different from the version in arxiv. The final version will be uploaded after the camera-ready version is ready

Proceedings Seventh Workshop on Intersection Types and Related Systems

Jakob Rehof

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

Journal ref EPTCS 177, 2015

ATLAS: Multi-View Code Representation Tool for C and C++ Source Programs

ATLAS: C和C++源代码的多视图代码表示工具

Jaid Monwar Chowdhury, Ahmad Farhan Shahriar Chowdhury, Humayra Binte Monwar, Mahmuda Naznin

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

AI总结 提出ATLAS工具，无需完整构建即可为C/C++生成对齐的AST、CFG和DFG，支持部分输入，输出JSON/DOT/PNG，在TheAlgorithms语料上CFG正确率达96.80%（C）和91.67%（C++）。

Comments 5 pages, 4 figures, 2 tables; Video demonstration: https://youtu.be/50DvEbenp14; Tool repository: https://github.com/jaid-monwar/ATLAS-multi-view-code-representation-tool.git

Source-Free Detection and Impact Analysis of Compiler Optimization Problems in Mobile Applications

移动应用中编译器优化问题的无源检测与影响分析

Han Hu, Xiaoheng Xie, Bo Sun, Jian Gu, Gang Fan, Li Li

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

AI总结 提出无源框架OptDetect，直接从二进制文件检测编译器优化问题，无需源码或构建元数据，准确率达93.0%，发现30.5%的库使用低优化级别，修复后CPU指令减少10-63%。

KVerus: Scalable and Resilient Formal Verification Proof Generation for Rust Code

KVerus：面向Rust代码的可扩展且高鲁棒性的形式化验证证明生成工具

Yuwei Liu, Xinyi Wan, Yanhao Wang, Minghua Wang, Lin Huang, Tao Wei

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

AI总结 KVerus是适配Rust代码的形式化验证工具，通过自适应范式与动态知识库，在单文件、仓库级基准及Rust内核验证中均优于现有方案，为形式化验证的规模化应用提供了关键进展。

Comments Accepted at ASE 2026

Rise From The Ashes: LLM-based Static Analysis for Deep Learning Framework Bugs

从灰烬中崛起：基于LLM的深度学习框架缺陷静态分析

Shaoyu Yang, Haifeng Lin, Chunrong Fang, Xiang Chen, Wei Cheng, Jiawei Liu, Yiyu Zhang, Hongyu Liu, Zhenyu Chen

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

AI总结 提出首个基于LLM的静态分析技术Phoenix，通过结构化语义桥接中间表示建模跨语言张量流，结合多智能体工作流检测深度学习框架缺陷，已在PyTorch中发现31个新bug。

Reading AI Model Compilation in MLIR Through the Lens of Formal Theories

通过形式理论的视角解读MLIR中的AI模型编译

Javed Absar

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

AI总结 本文通过形式理论（如项重写系统、精化演算、抽象解释）对应MLIR的匹配-重写引擎、阶段降低和范围分析，论证形式概念有助于明确抽象完备性、理想设计及实际权衡。

OpenAnt: LLM-Powered Vulnerability Discovery Through Code Decomposition, Adversarial Verification, and Dynamic Testing

OpenAnt：通过代码分解、对抗性验证和动态测试实现LLM驱动的漏洞发现

Nahum Korda, Gadi Evron

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

AI总结 提出OpenAnt系统，结合静态分析与LLM推理，通过代码分解、对抗性验证和动态测试三阶段流水线，在降低误报率的同时发现未知漏洞。

Dimensional Type Systems and Deterministic Memory Management: Design-Time Semantic Preservation in Native Compilation

维度类型系统与确定性内存管理：原生编译中的设计时语义保留

Houston Haynes

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

AI总结 本文提出一种编译框架，通过多阶段MLIR降低保持维度类型注解，使编译器能联合解决数值表示选择和确定性内存管理作为程序语义图的共同效应。维度推断确定值范围，进而决定表示选择、字宽、内存占用、分配策略和跨目标传输保真度。

Comments 33 pages, 8 tables, 3 appendices with extended examples

Benchmarking Testing in Automated Theorem Proving

在自动化定理证明中的基准测试

Jongyoon Kim, Hojae Han, Seung-won Hwang

机构 * Interdisciplinary Program in Artificial Intelligence, Seoul National University（人工智能交叉学科项目，首尔国立大学） ； Electronics and Telecommunications Research Institute（电子与电信研究所） 纠错

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

AI总结 本文提出T框架，通过依赖后继定理的编译成功来评估形式定理的语义正确性，揭示了当前定理生成能力的差距。

Comments ACL 2026 Industry

Journal ref The 64th Annual Meeting of the Association for Computational Linguistics -- Industry Track, 2026

Debt Behind the AI Boom: A Large-Scale Empirical Study of AI-Generated Code in the Wild

人工智能繁荣背后的债务：对真实世界中AI生成代码的大规模实证研究

Yue Liu, Ratnadira Widyasari, Yanjie Zhao, Ivana Clairine Irsan, Junkai Chen, David Lo

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

AI总结 本文研究了AI生成代码在真实软件项目中的技术债务影响，发现代码异味是最常见的问题，且部分问题长期存在，凸显了AI辅助开发中质量保障的必要性。

PROMISE: Proof Automation as Structural Imitation of Human Reasoning

PROMISE：证明自动化作为人类推理的结构模仿

Youngjoo Ahn, Sangyeop Yeo, Gijung Im, Jongmin Lee, Jinyoung Yeo, Jieung Kim

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

AI总结 PROMISE通过结构化嵌入框架实现证明生成自动化，通过挖掘证明状态的结构模式提升大规模定理证明的可扩展性。

Agentic Code Optimization via Compiler-LLM Cooperation

通过编译器-LLM协作实现代理代码优化

Benjamin Mikek, Danylo Vashchilenko, Bryan Lu, Panpan Xu

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

AI总结 本文提出编译器-LLM协作方法，结合传统编译优化与LLM生成，提升代码性能，实验显示比现有方法快1.25倍。

Do Code LLMs Do Static Analysis?

代码LLM进行静态分析吗？

Chia-Yi Su, Collin McMillan

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

AI总结 本文研究代码LLM在代码智能任务中的静态分析能力，发现LLM在静态分析任务中表现不佳，且预训练静态分析任务无法提升代码智能任务性能。

Comments 42 pages, 2 figures, Accepted at Empirical Software Engineering

ProofWright: Towards Agentic Formal Verification of CUDA

ProofWright: 向 CUDA 的代理形式验证迈进

Bodhisatwa Chatterjee, Drew Zagieboylo, Sana Damani, Siva Hari, Christos Kozyrakis

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

AI总结 ProofWright 通过整合自动形式验证与 LLM 代码生成，为 CUDA 核心提供内存安全、线程安全和语义正确性保证，验证了 74% 的生成内核，发现传统测试遗漏的细微错误。

Twitch: Learning Abstractions for Equational Theorem Proving

Twitch: 为等式定理证明学习抽象

Guy Axelrod, Moa Johansson, Nicholas Smallbone

机构 * Chalmers University, of Technology（查尔姆斯理工大学） ； University of Gothenburg（哥德堡大学） 纠错

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

AI总结 Twitch通过自动学习等式定理证明中的抽象模式，提升证明效率和速度。

Comments 20 pages, submitted to IJCAR 2026

Understanding Typing-Related Bugs in Solidity Compiler

理解Solidity编译器中的输入相关错误

Lantian Li, Yue Pan, Dan Wang, Jingwen Wu, Zhongxing Yu

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

AI总结 本文首次系统研究Solidity编译器中的输入相关错误，通过分析146个已修复错误，揭示其分布模式和特征，并总结12项核心发现。

Comments 37 pages, 8 figures

Propose, Solve, Verify: Self-Play Through Formal Verification

提出、解决、验证：通过形式验证进行自我对战

Alex Wilf, Pranjal Aggarwal, Bryan Parno, Daniel Fried, Louis-Philippe Morency, Paul Pu Liang, Sean Welleck

机构 * Carnegie Mellon University, School of Computer Science（卡内基梅隆大学计算机科学学院） ； MIT（麻省理工学院） 纠错

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

AI总结 通过形式验证的自我对战框架PSV，在代码生成中显著提升了模型性能，展示了形式验证和难度感知生成对自我对战的重要性。

Inside VOLT: Designing an Open-Source GPU Compiler

Shinnung Jeong, Chihyo Ahn, Huanzhi Pu, Jisheng Zhao, Hyesoon Kim, Blaise Tine

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

Comments 11 pages, 10 figures, two tables, two algorithms