ICML 2026 论文列表

International Conference on Machine Learning

录用类型

6,341篇论文

按官方录用论文列表统计,可能与会议公布的数字略有出入。

  • Spotlight
    5368.5%
  • Poster
    5,80591.5%

浏览全部论文

Threat2Traffic: Multi-Agent Environment Synthesis for Malware Traffic Generation from Threat Intelligence

Haoyang Chen, Chang Liu, Zhong Guan, Junzheng Shi, Gaopeng Gou, Gang Xiong

展开摘要

Data-driven cybersecurity research is fundamentally constrained by the scarcity of labeled datasets, yet acquiring authentic, large-scale malware traffic remains bottlenecked by obsolescent public datasets, unscalable manual construction, and inflexible sandboxes that fail to satisfy the sample-specific dependencies required for malware to exhibit malicious behavior. Threat intelligence documents these dependencies, and LLM agents offer a path to extract them for environment construction, yet directly applying such agents faces two challenges: input-side ambiguity and output-side fragility. In this paper, we propose Threat2Traffic, a multi-agent framework that extracts sample-specific dependencies from threat intelligence, reconstructs tailored environments, and captures malware traffic. To address input-side ambiguity, it formulates dependency extraction as structured multi-agent deliberation over an evidence graph. To overcome output-side fragility, it incorporates invariant-guided synthesis with dual-layer validation under syntactic and semantic constraints. Evaluated on 1,077 samples across eight malware families, Threat2Traffic achieves 83.1\% reproduction success, highlighting its effectiveness for scalable and realistic malware traffic generation. We release the core source code and traffic dataset at https://github.com/apos3637/Threat2Traffic

Poster
SWE-Compass: Towards Unified Evaluation of Agentic Coding Abilities for Large Language Models

Jingxuan Xu, Ken Deng, Weihao Li, Songwei Yu, Haoyang Huang, Xinping Lei, Yifan Yao, Huaixi Tang, Zhiyi Lai, Kepeng Lei, Zizheng Zhan, Yanan Wu, Chenchen Zhang, Wenqiang Zhu, Wen Xiang, Zongxian Feng, Han Li, Junqi Xiong, Dailin Li, Zuchen Gao, Kun Wu, Yuanxing Zhang, Wuxuan Gong, Ziyuan Gao, Guanxiang Wang, Yirong Xue, Mengfei Xie, Xiaojiang Zhang, Jinghui Wang, Wenhao Zhuang, Zheng Lin, Huiming Wang, Zhaoxiang Zhang, Yuqun Zhang, Haotian Zhang, Ming Sun, Chen Bin, Jiaheng Liu

展开摘要

Evaluating large language models (LLMs) for software engineering has been limited by narrow task coverage, language bias, and insufficient alignment with real-world developer workflows. Existing benchmarks often focus on algorithmic problems or Python-centric bug fixing, leaving critical dimensions of software engineering underexplored. To address these gaps, we introduce SWE-Compass, a comprehensive benchmark that unifies heterogeneous code-related evaluations into a structured and production-aligned framework. SWE-Compass spans 8 task types, 8 programming scenarios, and 10 programming languages, with 2000 high-quality instances curated from authentic GitHub pull requests and refined through systematic filtering and validation. We benchmark ten state-of-the-art LLMs under two agentic frameworks, SWE-Agent and Claude Code, revealing a clear hierarchy of difficulty across task types, languages, and scenarios. Moreover, by aligning evaluation with real-world developer practices, we hope SWE-Compass can provide a rigorous and reproducible foundation for diagnosing and advancing agentic coding capabilities in large language models.

Poster
Mitigating Bias in Locally Constrained Decoding via Tractable Proposals

Meihua Dang, Linxin Song, Honghua Zhang, Jieyu Zhao, Guy Van den Broeck, Stefano Ermon

展开摘要

Generations from large language models often fail to conform to desired constraints such as JSON schema. Existing locally constrained decoding (LCD) approaches enforce constraints by myopically masking out next tokens, resulting in biased sampling and degradation in performance. Recent work uses sequential Monte Carlo (SMC) methods to mitigate such biases, but designing effective proposal distributions or potential functions remains a key challenge. In this work, we propose a generic approach to construct proposals and potentials for SMC sampling from $p_{\mathrm{lm}}( \cdot \mid \mathrm{constraint})$. First, we show that constraints specified as finite automata can be tensorized for efficient execution on GPUs, which we use to construct globally constrained decoding (GCD) proposals. In addition, leveraging the fact that tensorized finite automata share the same circuit structure as hidden Markov models, we circuit-multiply them to obtain the probabilistic GCD (P-GCD) proposals encoding both logical and probabilistic information about the target distributions. We evaluate (P-)GCD on the tasks of function calling, keyword-based generation, and SQL generation. Experiments show that under the same SMC sampling setup, compared to LCD proposals, (P-)GCD converges faster to the target distribution with significantly fewer particles.

Poster
Rubric Curriculum RL: Exploiting the Generation-Verification Gap in Non-Verifiable Domains

Tejas Krishnan, Sumeet Ramesh Motwani, Charles London, Suhaas M Bhat, Huitian Jiao, Philip Torr, Riashat Islam, Christopher Summerfield, Christian Schroeder de Witt, Qilong Gu, Shital Shah

展开摘要

Reinforcement learning with verifiable rewards (RLVR) on foundation models has led to significant gains in math and code generation. Extending these gains to open-ended domains remains challenging: ground-truth verification is unavailable, human annotation is expensive, and learned reward models are prone to reward hacking. We introduce Rubric Curriculum RL (RcRL), a general self-improvement method for non-verifiable tasks that requires no new data, human annotations, or stronger teacher models. RcRL exploits the generation-verification gap, where judging good outputs is easier than producing them. We combine pairwise preferences over rollouts with a curriculum over rubric criteria, yielding a more discriminative signal than absolute scoring while reducing reward hacking through a non-stationary objective. Whereas baselines plateau or collapse within a few hundred steps, RcRL preserves output entropy and keeps improving past 1000 steps. On creative writing, RcRL outputs are preferred 70.5% of the time compared to the base model, with consistent gains across multiple creative writing benchmarks and judges. On HealthBench, RcRL improves over the base model by 14.6% (full set) and 25.4% (consensus subset), outperforming all HealthBench training baselines, including instance-specific rubrics.

Poster
Motion-Aware Caching for Efficient Autoregressive Video Generation

Jing Xu, Yuexiao Ma, Xuzhe Zheng, Xing Wang, Shiwei Liu, Chenqian Yan, Xiawu Zheng, Rongrong Ji, Fei Chao, Songwei Liu

展开摘要

Autoregressive video generation paradigms offer theoretical promise for long video synthesis, yet their practical deployment is hindered by the computational burden of sequential iterative denoising. While cache reuse strategies can accelerate generation by skipping redundant denoising steps, existing methods rely on coarse-grained chunk-level skipping that fails to capture fine-grained pixel dynamics. This oversight is critical: pixels with high motion require more denoising steps to prevent error accumulation, while static pixels tolerate aggressive skipping. We formalize this insight theoretically by linking cache errors to residual instability, and propose $\textbf{MotionCache}$, a motion-aware cache framework that exploits inter-frame differences as a lightweight proxy for pixel-level motion characteristics. MotionCache employs a coarse-to-fine strategy: an initial warm-up phase establishes semantic coherence, followed by motion-weighted cache reuse that dynamically adjusts update frequencies per token. Extensive experiments on state-of-the-art models like SkyReels-V2 and MAGI-1 demonstrate that MotionCache achieves significant speedups of $\textbf{6.28}\times$ and $\textbf{1.64}\times$ respectively, while effectively preserving generation quality (VBench: 1%$\downarrow$ and 0.01%$\downarrow$ respectively). The code is available at https://github.com/ywlq/MotionCache.

Poster
How2Everything: Mining the Web for How-to Procedures to Evaluate and Improve LLMs

Yapei Chang, Kyle Lo, Mohit Iyyer, Luca Soldaini

展开摘要

Generating step-by-step "how-to" procedures is a key LLM capability: how-to advice is commonly requested in chatbots, and step-by-step planning is critical for complex reasoning tasks. Yet, measuring and improving procedural validity at scale on real-world tasks remains challenging and understudied. We introduce How2Everything, a scalable framework to evaluate and improve goal-conditioned procedure generation. Our pipeline How2Mine extracts and rewrites 351K procedures from 980K web pages across 14 topics, and can scale to larger corpora. From this pool we build How2Bench, a 7K-example evaluation set balanced across topics. We also introduce How2Score, an evaluation protocol that uses an LLM judge to detect whether a generation contains any critical failure that would prevent achieving the goal. For low-cost, reproducible evaluation, we distill a frontier judge into an open 8B model achieving 80.5\% agreement with human annotators. How2Bench reveals clear scaling trends across model size and training stages, providing signal early in pretraining. Finally, RL using How2Score as a reward improves performance on How2Bench by >10 points across three base models without systematic regressions on standard benchmarks, with gains not primarily explained by source-document memorization or superficial format compliance. We release all code and data at https://github.com/lilakk/how2everything.

Poster
The Invisible Lottery: How Subtle Cues Steer Algorithm Choice in LLM Code Generation

Akanksha Narula, Mofasshara Binte Rafique, Laurent Bindschaedler

展开摘要

Large language models (LLMs) now generate substantial production code, often for tasks with multiple valid algorithmic solutions. Incidental prompt cues—contextual words or metadata outside the task specification—can steer which algorithm the model selects, even when all outputs pass the same tests. Prompt sensitivity is well studied as a mechanism for improving output quality; here, we instead study *output policy*: algorithm choice under fixed correctness. We define *algorithm steering* as cue-induced shifts in algorithm-family distributions and run 46,535 controlled experiments across 11 tasks, 19 cue types (18 channels plus a memoization semantic-vs-surface ablation that preserves meaning while changing typography and punctuation), and 15 model configurations. We find large, systematic shifts in algorithm-family distributions (up to 100 percentage points, pp), largely consistent with cue semantics, including in applied tasks such as rate limiting. Direct algorithm naming is the most reliable mitigation we tested. These results reveal an “invisible lottery” in which accidental context alters downstream properties such as performance, security, and maintainability.

Poster
AutoBaxBuilder: Bootstrapping Code Security Benchmarking

Tobias von Arx, Niels Mündler, Mark Vero, Maximilian Baader, Martin Vechev

展开摘要

As large language models (LLMs) see wide adoption in software engineering, the reliable assessment of the correctness and security of LLM-generated code is crucial. Notably, prior work showed that LLMs are prone to generating code with security vulnerabilities, highlighting that security is often overlooked. These insights were enabled by specialized benchmarks crafted by security experts through significant manual effort. However, benchmarks (i) inevitably end up contaminating training data, (ii) must extend to new tasks to provide a more complete picture, and (iii) must increase in difficulty to challenge more capable LLMs. In this work, we address these challenges and present AutoBaxBuilder, an automated pipeline that generates code security benchmarking tasks from scratch. It leverages the code-understanding capabilities of LLMs combined with robust reliability checks to construct functional tests and end-to-end security-probing exploits. The quality of the pipeline is quantitatively confirmed by aligning its predictions with an expert-written baseline and qualitatively validated through manual soundness verification. We use AutoBaxBuilder to construct a new benchmark and release it to the public as AutoBaxBench, together with a thorough evaluation on contemporary LLMs. AutoBaxBuilder generates new tasks in under 2 hours, for less than USD 4. Including a manual verification, this reduces the required human effort for benchmark construction by a factor of 12.

Poster
BOOSTAPR: Boosting Automated Program Repair via Execution-Grounded Reinforcement Learning with Dual Reward Models

Yuanhao Li, Hongbo Wang, Xiaotang Shang, Xunzhu Tang, Yiming Cao, Xuhong Chen

展开摘要

Reinforcement learning for program repair is hindered by sparse execution feedback and coarse sequence-level rewards that obscure which edits actually fix bugs. We present BoostAPR, a three-stage framework: (1) supervised fine-tuning on execution-verified demonstrations with reasoning traces, (2) training dual reward models—a sequence-level assessor and a line-level credit allocator—from execution outcomes, and (3) PPO optimization where the line-level model redistributes rewards to critical edit regions. This line-level credit assignment operates at an intermediate granularity naturally suited to code changes. Trained on SWE-Gym and evaluated on four benchmarks, BoostAPR achieves 40.7% on SWE-bench Verified (+22.9pp over the base model), 24.8% on Defects4J (Python→Java transfer), 84.5% on HumanEval-Java, and 95.0% on QuixBugs, showing competitive open-source performance with strong cross-language generalization.

Poster
$A_2$DEPT: Large Language Model–Driven Automated Algorithm Design via Evolutionary Program Trees

Bin CHEN, Shouliang Zhu, Beidan Liu, Yong Zhao, Tianle Pu, Huichun Li, Zhengqiu Zhu

展开摘要

Designing heuristics for combinatorial optimization problems (COPs) is a fundamental yet challenging task that traditionally requires extensive domain expertise. Recently, Large Language Model (LLM)-based Automated Heuristic Design (AHD) has shown promise in autonomously generating heuristic components with minimal human intervention. However, most existing LLM-based AHD methods enforce fixed algorithmic templates to ensure executability, which confines the search to component-level tuning and limits system-level algorithmic expressiveness. To enable open-ended solver synthesis beyond rigid templates, we propose Automated Algorithm Design via Evolutionary Program Trees (A$_2$DEPT), which treats LLMs as system-level algorithm architects. A$_2$DEPT explores the vast program space via a tree-structured evolutionary search with hybrid selection and hierarchical operators, enabling iterative refinement of complete algorithms. To make open-ended generation practical, we enforce executability with a lightweight program-maintenance loop that performs feedback-driven repair. In experiments, A$_2$DEPT consistently outperforms state-of-the-art baselines across standard and highly constrained benchmarks, reducing the optimality gap by an average of 9.8\%. Our work implies that system-level algorithm synthesis is a viable and scalable paradigm for LLM-driven optimization.

Poster
Deterministic Component Mining for Multi-Framework UI2Code Generation

Zixiong Yang, Linxiao Li, Jiaye Lin, Binrui Wu, Xiaoyu Kang, Jiechao Gao

展开摘要

Automating User Interface (UI) generation substantially improves productivity and accelerates development by reducing engineering time and manual effort. Despite recent progress of Multimodal Large Language Models (MLLMs) in UI2Code, most existing approaches focus on a single HTML/CSS form and fail to systematically incorporate front-end frameworks such as React, Vue, and Angular. Moreover, their outputs are often verbose and hard to reuse at the component level. To address those issues, we propose Deterministic Component Mining (DCM), a multi-stage pipeline that couples MLLMs with a compact intermediate representation to enable multi-framework and component-oriented code generation. Firstly, a lightweight structure model predicts the representation of the DOM tree in JSON format, capturing the coarse layout from a webpage screenshot. Subsequently, we formulate deterministic rules to normalize the predicted DOM tree and mine reusable components with repetitive patterns via structural hashing and clustering, thereby yielding a portable intermediate representation. Finally, we employ a framework-conditioned prompting strategy governed by a binding specification and a file-block protocol to emit HTML/React/Vue/Angular code with explicit component props and repeat constructs. Extensive experiments demonstrate that DCM significantly outperforms baselines on automatic evaluation metrics and component-level reuse, while delivering consistent gains in multi-framework portability and overall code structural quality.

Poster
Synthesizing Multimodal Geometry Datasets from Scratch and Enabling Visual Alignment via Plotting Code

Haobo Lin, Tianyi Bai, Chen Chen, Jiajun Zhang, Bohan Zeng, Wentao Zhang, Binhang Yuan

展开摘要

Multimodal geometry reasoning requires models to jointly understand visual diagrams and perform structured symbolic inference, yet current vision--language models struggle with complex geometric constructions due to limited training data and weak visual--symbolic alignment. We propose a pipeline for synthesizing complex multimodal geometry problems from scratch and construct a dataset named \textbf{GeoCode}, which decouples problem generation into symbolic seed construction, grounded instantiation with verification, and code-based diagram rendering, ensuring consistency across structure, text, reasoning, and images. Leveraging the plotting code provided in GeoCode, we further introduce code prediction as an explicit alignment objective, transforming visual understanding into a supervised structured prediction task. GeoCode exhibits substantially higher structural complexity and reasoning difficulty than existing benchmarks, while maintaining mathematical correctness through multi-stage validation. Extensive experiments show that models trained on GeoCode achieve consistent improvements on multiple geometry benchmarks, demonstrating both the effectiveness of the dataset and the proposed alignment strategy.

Poster
UniCode: Augmenting Evaluation for Code Reasoning

Xinyue Zheng, Haowei Lin, Shaofei Cai, Yaodong Yang, Zilong Zheng, Yitao Liang

展开摘要

Current coding benchmarks often overstate Large Language Model (LLM) capabilities due to static paradigms and data contamination, allowing models to exploit statistical shortcuts rather than genuine reasoning. To address this, we introduce UniCode, a generative evaluation framework that systematically probes LLM reasoning boundaries via: (1) multi-dimensional augmentation operators to create diverse algorithmic variants; (2) a scalable test generation pipeline achieving 94.5\% correctness without human-written solutions; and (3) fine-grained diagnostic metrics for rich error signals. Our evaluation of state-of-the-art models reveals a significant 31.2\% performance collapse. Critically, we observe a high variance across different reasoning axes, revealing a profound fragility under structural shifts despite surface-level robustness. Furthermore, we identify a ``seed-problem regression," where models fail by defaulting to memorized seed logic and inefficient complexities. Our evaluation code is publicly available at \url{https://github.com/grandsmile/UniCode}.

Poster
TritonGym: A Benchmark for Agentic LLM Workflows in Triton GPU Code Generation

Yue Guan, Yichen Lin, Xu Zhao, Jianzhu Yao, Xinwei Qiang, Zhongkai Yu, Pramod Viswanath, Yufei Ding, Adnan Aziz

展开摘要

Large language models (LLMs) can already draft plausible Triton kernels, yet most existing evaluations still focus on single-shot generation and underplay tool use and feedback. We introduce *TritonGym*, a benchmark and orchestration framework for evaluating agentic workflows in GPU code generation. *TritonGym* standardizes access to a set of code generation tools via function-calls, separating intrinsic model capability from workflow design and enabling fair, apples-to-apples comparison. The benchmark spans a maintained operator set, community samples, out-of-distribution tasks, and DSL extensions, ensuring both generality and extensibility. By providing a common orchestration and evaluation framework, *TritonGym* democratizes the development of GPU coding agents, supports practical adoption of agent-generated kernels, and facilitates progress on advanced agentic systems.

Poster
S-Quant: Rethinking Weight Quantization with Seed-Based Generation

Mingzi Wang, Lancheng Zou, Shuo Yin, Zhuolun He, Bei Yu

展开摘要

The progressive scaling of large language models (LLMs) has consistently enhanced multimodal understanding and advanced reasoning capabilities, but has substantially increased computational and hardware execution overhead. In this paper, we present S-Quant, a novel post-method that compresses only model weights. We partition each weight tensor into fixed-size blocks and assign a single seed to each block. The seed drives a hardware-friendly Linear Feedback Shift Register (LFSR) generator that dynamically produces multiple basis matrices. Each block is then reconstructed as a linear combination of these basis matrices, with block-specific coefficients, which substantially reduces the amount of stored data, increases the data-transfer efficiency between memory and compute units, and consequently speeds up memory-bound inference for large language models. Experimental results on different LLM models ranging from 7B–70B parameters show that S-Quant attains state-of-the-art performance when weights are compressed to approximately 3-bit or 4-bit. We also design a dedicated ASIC accelerator that achieves a 4× speed-up for memory-bound LLM inference.

Poster
InertialAR: Autoregressive 3D Molecule Generation with Inertial Frames

Haorui Li, Weitao Du, Yuqiang Li, Hongyu Guo, Shengchao Liu

展开摘要

Transformer-based autoregressive models have emerged as a unifying paradigm across modalities such as text and images, but their extension to 3D molecule generation remains underexplored. The gap stems from two fundamental challenges: (1) how to tokenize molecules into a canonical 1D sequence of tokens that is invariant to both SE(3) transformations and atom index permutations, and (2) how to design an architecture capable of modeling hybrid atom-based tokens that couple discrete atom types with continuous 3D coordinates. To address these challenges, we introduce InertialAR. It first performs generation-oriented canonical tokenization by aligning each molecule to a canonical inertial frame and reordering atoms, thereby converting arbitrary 3D structures into a unique, SE(3)- and permutation-invariant sequence of tokens for autoregressive generation. Built upon this canonical tokenization, we propose geometric positional encoding (GeoPE), which endows Transformer attention with 3D geometric awareness. Finally, InertialAR utilizes a hierarchical autoregressive paradigm to decode the next atom, consecutively predicting the atom type and 3D coordinates via Diffusion Loss. Experimentally, InertialAR achieves state-of-the-art performance on 8 of the 10 evaluation metrics for unconditional generation across QM9, GEOM-Drugs, and B3LYP. Moreover, it significantly outperforms baselines in controllable generation for targeted chemical functionality, attaining state-of-the-art results across all 5 metrics. Code is available at github.com/HaoruiLi46/InertialAR.

Poster
Efficient Skill Grounding via Code Refactoring with Small Language Models

Sera Choi, Wonje Choi, Saehun Chun, Daehee Lee, Jooyoung Kim, Chaeun Lee, Honguk Woo

展开摘要

Effective skill grounding is essential for deploying reusable skills in embodied agents, as even minor embodiment or environmental differences can render an entire skill incompatible. This challenge is particularly pronounced in embodied settings, where agents must operate in dynamic, partially observable environments without access to large language models (LLMs). In this setting, reliance on LLMs is impractical, while small language models (sLMs) remain insufficient for the effective skill grounding required for reliable long-horizon control. We present RECENT, a refactoring-centric agent framework that enables efficient skill grounding with sLMs by decoupling skill semantics from embodiment- and environment-specific execution binding. By representing skills as executable code, RECENT preserves the semantic intent encoded in a skill’s control structure while grounding it by modifying only execution bindings through localized refactoring, rather than regenerating code from scratch. We evaluate RECENT across diverse skill grounding scenarios spanning multiple robot embodiments in dynamic environments, demonstrating robust long-horizon performance when deployed with an sLM. Across all scenarios, RECENT achieves the best performance among sLM-based Code-as-Policies (CaP) methods and matches the task performance of LLM-based CaP.

Poster
DFSAttn: Dynamic Fine-grained Sparse Attention for Efficient Video Generation

Jie Hu, Zixiang Gao, Yutong He, Kun Yuan

展开摘要

Diffusion transformers have achieved remarkable success in high-quality video generation, yet their reliance on spatiotemporal 3D full attention incurs prohibitive computational cost due to the quadratic complexity of attention. Block sparse attention is a common approach to mitigate this by focusing computation on important regions. However, attention maps in DiTs exhibit inherently dynamic and fine-grained sparsity, which causes existing block sparse attention methods to degrade significantly in quality, especially at high sparsity ratios. In this paper, we revisit block sparse attention and derive a theoretical lower bound on attention recall to characterize the key factors governing its effectiveness. Guided by these insights, we propose DFSAttn, a training-free sparse attention framework that enables dynamic, fine-grained sparsification efficiently. DFSAttn incorporates three core designs: Hilbert curve-based token reordering to achieve fine-grained sparsity while preserving efficient GPU execution, hierarchical block scoring for accurate block importance estimation, and sparse mask caching with adaptive ratios to balance accuracy and efficiency. Experimental results demonstrate that DFSAttn consistently outperforms prior methods under high sparsity, achieving up to 2.1$\times$ end-to-end speedup while maintaining high generation quality. Our code is open-sourced and available at https://github.com/jessica-hujie/DFSAttn.

Poster
Efficient Code Analysis via Graph Representation Learning-Guided Large Language Models

Hang Gao, Tao Peng, Baoquan Cui, Hong Huang, Fengge Wu, Junsuo Zhao, Jian Zhang

展开摘要

Large Language Models (LLMs) have significantly advanced code analysis tasks, yet they struggle to detect malicious behaviors fragmented across files, whose intricate dependencies easily get lost in the vast amount of benign code. We therefore propose a graph-centric attention acquisition pipeline that enhances LLMs' ability to localize malicious behavior. The approach parses a project into a code graph, uses an LLM to encode nodes with semantic and structural signals, and trains a Graph Neural Network (GNN) under sparse supervision. The GNN performs an initial detection, and by interpreting these predictions, identifies key code sections that are most likely to contain malicious behavior. These influential regions are then used to guide the LLM's attention for in-depth analysis. This strategy significantly reduces interference from irrelevant context while maintaining low annotation costs. Extensive experiments show that the method consistently outperforms existing approaches on multiple public and custom datasets, highlighting its potential for practical deployment in software security scenarios. Codes can be found in https://github.com/Epiphaniespt/GMLLM.git.

Poster
ExVerus: Verus Proof Repair via Counterexample Reasoning

Jun Yang, Yuechun Sun, Yi Wu, Rodrigo Caridad, Yongwei Yuan, Jianan Yao, Shan Lu, Kexin Pei

展开摘要

Large Language Models (LLMs) have shown promising results in automating formal verification. However, existing approaches treat proof generation as a static, end-to-end prediction over source code, relying on limited verifier feedback and lacking access to concrete program behaviors. We present ExVerus, a counterexample-guided framework that enables LLMs to reason about proofs using behavioral feedback via counterexamples. When a proof fails, ExVerus automatically generates and validates counterexamples, and then guides the LLM to generalize them into inductive invariants to block these failures. Our evaluation shows that ExVerus significantly improves proof accuracy, robustness, and token efficiency over the state-of-the-art prompting-based Verus proof generator.

Poster