公开论文雷达

实验覆盖367个线性和50个非线性程序验证基准。框架把不变量建模为两类引理组成的有序序列：bounding lemma约束变量范围，essential lemma捕获语义，并为每类引理定义专属学习目标。每推出一条新引理，就用它过滤已有的归纳反例和负反例，防止反例集膨胀。LLM按顺序生成引理候选，SMT求解器负责校验，ICE-DT兜底补全LLM没覆盖到的引理。

Loop invariant synthesis is a fundamental problem in program verification, yet the inherent undecidability makes it highly challenging. Recent studies have increasingly employed various machine learning techniques to generate loop invariants. However, most of these methods adopt a monolithic approach. Due to the inability to strictly constrain the learning process, learning-based methods struggle to simultaneously consider all necessary conditions and generate complete invariants when tackling complex problems. In fact, a loop invariant is often an ordered sequence of lemmas, rather than a single invariant formula. This motivates us to propose Incremental ICE, a novel learning framework for incremental synthesis. Our framework integrates the incremental philosophy of IC3 into the general invariant learning framework ICE. By defining a lemma-specific learning objective and introducing a counterexample filtering mechanism, we can achieve sound incremental learning. Under this framework, we instantiate a loop invariant synthesis tool, LimICE, which leverages LLMs to generate the ordered sequence of lemmas and incorporates ICE-DT as a fallback mechanism to complement the lemma sequence. Experiments on 367 linear benchmarks and 50 nonlinear benchmarks demonstrate the effectiveness of the proposed approach. LimICE solves 349 (out of 367) linear problems on an average of 15.2 seconds and 47 (out of 50) nonlinear problems on an average of 8.8 seconds. Compared to the state-of-the-art LLM-based baseline, our approach solves 12-24% more instances while running 36-63% faster across linear and nonlinear benchmarks. LimICE also consistently outperforms strong non-LLM baselines and solves at least 86 and 27 additional instances on the linear and nonlinear benchmarks, respectively.

从开源Java和Python仓库采集已合并PR。映射规则很简单：整个PR对应一个复合提交（CC），PR内各独立提交对应单任务提交（STC），形成天然ground truth标注对，PR review实践充当原子性约束。然后施加过滤规则筛选「理想PR」——PR整体纠缠、但内部每个提交都原子。过滤分三步：识别PR整体纠缠、验证内部提交原子、排除CC或STC大小异常的样本。验证上，对新旧数据集做统计分布对比，控制CC与STC大小变量，并在置信投票方法上检验分布偏差的实际影响。

Composite commits (CC), in which multiple unrelated changes are bundled into a single commit, are frequent in software development and significantly hinder code comprehension and maintenance. Although machine learning-based methods have been developed to ``untangle'' such commits into smaller, coherent change sets, these methods require large-scale training data with correct untangling labels. Preparing such datasets is costly and typically requires expert labelling. In this study, we propose a scalable and cost-effective method for dataset construction by leveraging commits extracted from open-source repositories' pull requests (PRs). We empirically validated our dataset and found that when applying our filtering rules, PRs that, when viewed as a single commit, are tangled, yet each individual commit on the feature branch is atomic (ideal PRs), increased from 9.5% to 55%. This composite commits dataset is more than 5.7 times larger than previous heuristic-based datasets. Using our new dataset, we find that the PR-based dataset differs statistically from previous datasets directly constructed using Herzig's proposed heuristics even after accounting for our proposed rules that may alter CC or STS sizes. When constructing datasets using the previous heuristics, they differ statistically along dimensions that impact the confidence voters and are likely to impact learning-based approaches. We validate the impact on the original Herzig \etal method, which used confidence voters across our dataset. To show that our approach extends to other languages, we also create a Python dataset which we empirically validate, finding comparable rates for ideal PRs (56.5%).

每轮用全部历史实验点自适应拟合多项式回归，阶次随数据量调整；在原始搜索空间采样并赋伪目标值；把伪数据与真实数据合并；用合并集更新高斯过程代理模型，再由采集函数选下一个真实实验点。数据来源是多地形合成基准函数和一个真实材料成分优化问题；对比传统BO和TSBO。

Bayesian optimization (BO) is an optimization method that sequentially proposes the next candidate explainable variables for optimizing target variables by balancing exploration and exploitation. BO is often used under a limited evaluation budget, such as hyperparameter tuning of deep learning. Despite its effectiveness, conventional BO may have poor convergence in practical experimental science where each evaluation is often costly and time-consuming. Recently, BO methods have been proposed that accelerate optimization by using pseudo-experimental data that simulate experimental data. However, when only a limited number of experimental data are available, the generated pseudo-experimental data may be of insufficient quality. In this study, we developed PolyBO to improve optimization time by generating high-quality pseudo-experimental data even when the number of trials is limited. PolyBO performs BO efficiently by generating pseudo-experimental data with an adaptively updated versatile parametric model. This low-capacity polynomial regression model is intended to enable efficient BO even with limited experimental data. PolyBO updates the BO surrogate model with a combined dataset consisting of experimental data and pseudo-experimental data and then performs optimization. Using synthetic benchmark functions with diverse landscapes, we found that PolyBO reduced the optimization time by a median of 42\%. For a real-world material composition optimization problem, PolyBO reduced the optimization time by a median of 96\% compared with conventional methods. Overall, PolyBO achieves efficient optimization in settings where each experiment requires a long time.

TCQM批量生成覆盖边界场景的测试，并用自验证过滤输入无效或逻辑错误的用例。Parallel TDD Refinement以可信测试为反馈迭代优化代码，并生成多条候选。BiCoTeV把候选代码和测试建成二部图，按执行通过或失败关系建边并双向打分，选出得分最高的候选。研究在HumanEval、MBPP、APPS、LiveCodeBench四个基准和四个LLM上受控评估。

Large Language Model (LLM)-based Test-Driven Development (TDD) has advanced automated code generation. However, existing approaches depend heavily on human-crafted test cases and cannot operate effectively when only natural-language requirements are available. Although recent work enables automatic test generation, it often overlooks the inherent stochasticity of LLMs, leading to two key defects: faulty tests generate misleading feedback that distorts code optimization, while mixed-quality test cases produce conflicting evaluation signals that hinder reliable code selection. To address these challenges, we propose MineValiCoder, a collaborative closed-loop TDD framework based on the mutual reinforcement of test-case quality and code quality. MineValiCoder comprises three modules. The Test Case Quality Mining (TCQM) module filters faulty test cases through self-validation, providing reliable optimization supervision. The Parallel TDD Refinement module iteratively optimizes code and generates diverse high-quality code candidates using validated test-case feedback. The Bipartite Graph-Based Code-Test Mutual Validation (BiCoTeV) module dynamically models code-test interactions and performs mutual validation scoring for stable and reliable optimal-code selection. Extensive evaluations across four LLMs and mainstream benchmarks show that MineValiCoder significantly outperforms state-of-the-art methods. Specifically, it achieves Pass@1 scores of 96.34% on HumanEval, 87.40% on MBPP, 64.00% on APPS, and 51.33% on LiveCodeBench. These results demonstrate the effectiveness of MineValiCoder in mitigating LLM stochasticity and improving the reliability of automated code generation.

框架分两支。语义分支用Titans编码器处理文本，把局部短语注意力和联想式长期记忆分开。时序分支用卡尔曼滤波，在非均匀交互间隔下递推估计潜在状态。关键模块是UDFM：它把卡尔曼的后验协方差转成不确定性信号，驱动ACFM调整静态-时序融合中的特征权重；首次有效交互之后，FD-TSE再用前一步后验协方差校准记忆检索。评测在Amazon Video Games与MovieLens-32M上进行，采用时间感知拆分加物品冷启动双协议、采样候选排名，设12条基线，含消融、固定增益对比和卡尔曼诊断。

Item cold-start recommendation is difficult when new items have sparse early interactions and appear in recommendation environments that keep changing over time. Static content, early feedback, and temporal-state evidence are all useful, but their reliability varies across the item lifecycle. This work proposes a framework--Neural Memory Kalman Fusion Recommender (NMKFR), which combines a Titans-based semantic encoder with time-aware Kalman state tracking. The semantic branch extracts memory-enhanced item observations from text, while the temporal branch estimates latent states under irregular interaction intervals. The NMKFR further uses posterior covariance as an uncertainty signal to calibrate semantic memory retrieval and adaptive static-temporal fusion. Experiments on Amazon Video Games and MovieLens-32M evaluate NMKFR under time-aware and item cold-start protocols using sampled candidate ranking. Across the reported comparisons, ablations, diagnostics, and robustness analyses, NMKFR achieves the strongest retained results and exhibits bounded uncertainty-related internal behavior. These findings provide empirical evidence for posterior-covariance-guided semantic-temporal fusion under the evaluated offline settings.