Tag
提出一个无奖励、无裁判、无答案键的自改进代理框架,通过双层循环在小型精确DSL上进行算子归纳,实现精确问答能力的自我扩展,并在多个领域验证其可靠性与跨模型迁移能力。
该论文研究 Verus/Rust 形式验证工作流中,正确性反馈如何反而抑制规格完整性审计所需的证据,发现独立无反馈探索比带纠正反馈的循环产生多一倍的认证反例,并在 NeurIPS 2026 AI for Verifiable Coding 工作坊被接收。
提出一种以程序验证器为奖励信号的智能体强化学习框架,通过读取验证器诊断信息(而非二元判决)并加入完整性审计,显著提升Qwen3系列模型在DafnyBench和SWE-Proof等验证基准上的正确率(最高达100%)。
论文提出"执行后学习"(Learning after Execution)框架,将程序执行结果作为中间状态支持额外的纠正学习动作,并为初始动作与纠正动作分配不同的信用,在Image-to-TikZ任务上将渲染成功率提升至92.70%。
本文提出 Reels-RSI,一个开源的可编程短视频(explainer reel)导演系统,将讲解视频视为程序而非像素,通过代码层面的日志、可执行规则与回顾反思实现 agent 的程序级自我改进,并在 111 个 reel 的实验中验证了规则审计效果及偏好信号的失败模式。
VIGOR 提出了一种将监督式场景程序生成、执行验证与分级几何修复相结合的方法,用于解决工业场景程序中「可执行性与工程可行性之间的差距」,在1749个场景的数据集上达到96.86%的完整可行性,显著超越基线。
VETR提出了一种执行证据驱动的递归自我改进框架,通过分析程序执行轨迹来改进符号图形推理中的场景生成,在BlenderGym和BlenderBench上超越了现有优化策略。
EliteTable is a self-improving, LLM-guided program-search algorithm that maintains a fixed-capacity table of high-scoring solutions to propose, edit, and remix candidate executable control policies, evaluated across six Gymnasium control tasks showing generalization gains in some tasks but needing ablations to establish relative performance.
ProgramGym introduces a framework with Program-Env and Program-Agent for building scalable, verifiable training environments for long-horizon program reproduction agents, achieving notable performance gains when fine-tuning Qwen3.8-27B on the generated environments.
Researchers introduce EPOCH, an evidence-governed architecture for AI research agents that combines task contracts, typed memory, active falsification, and independent replay, achieving state-of-the-art performance on AlgoTune (0.65 vs 0.53 mean normalized score) and the Math14 suite.
The paper proposes Recursive Self-Improvement (RSI), a training loop in which a unified multimodal model's text and visual abilities generate training data for each other, with program execution providing verified supervision. Evaluated on charts with a new BasicChartBench benchmark, four rounds of RSI improve performance from 45.7% to 60.2% while verified-program share rises from 48.9% to 95.2%.
Code to Control synthesizes parameterized Python controllers via LLM-generated program structure with derivative-free parameter fitting, enabling real-time control without LLM inference or planning at decision time, and outperforming planning-based program synthesis across Atari, Flappy Bird, and MuJoCo tasks.
This paper introduces component-aware feedback for LLM-guided evolutionary search, logging which component edits changed which fitness metrics in an attribution memory, achieving baseline-quality performance in one-third of the search budget and 7.2% higher nDCG@10 on Bright reranking tasks.
StepCAD 提出了一种将状态条件化 CAD 策略与 IoU 引导树搜索相结合的生成式优化方法,从 3D 网格重建可执行 CAD 程序,并发布了包含 150 万个程序的 ARCADE-1.5M 大规模数据集,在多个基准上实现了最先进的几何重建精度。
HeurEvo introduces an automated plan–code–component co-evolution framework in which AI agents jointly evolve algorithmic structure, executable implementations, and a shared pool of reusable components for hybrid solver-augmented heuristics. Across combinatorial optimization benchmarks and MIPLIB instances, it matches or surpasses state-of-the-art solvers under tight runtime budgets and sets new results on problems such as hexagon packing.
Lambda MicroEgg is a tool implementing an e-graph with support for well-scoped alpha-aware binders and higher-order Miller patterns for program synthesis and rewriting.
The article explains program synthesis techniques, specifically counterexample-guided iterative synthesis for loop-free programs, and provides an implementation in Rust using the Z3 solver.
This paper identifies the verification gap as a key constraint in AI reasoning progress, provides theoretical and empirical analysis of verifier soundness trade-offs, and introduces proof-carrying cognition to enhance reward settlement in reinforcement learning.
A repair tool that infers fixes from a single worked example and successfully repairs 5 out of 5 bugs in unseen code using only 4 CPU instructions and zero tokens, with exhaustive verification.
ClosureBench is a constructive benchmark for evaluating language models on compositional graph reasoning tasks, revealing that frontier models degrade with complexity while a fine-tuned model maintains performance through program synthesis.