TodayNewsResearchFieldsStacksMarketAnalytics
⌘K

Research

New papers ranked by attention, with their code, models and discussion linked. Pick a field on the left.

WeekMonthQuarterAll
NewestMost relevant

Papers

Open problems

Rising research topics

Ask the research

Sample
ByteTrail · AI and developer-tools intelligence
NewsResearchStacksAPI
Fields · this week
All fields3393Multimodal539Agents509Frontier LLMs435Inference & serving263Image segmentation178Learning verifiable rewards1593D scene158Graph learning153Voice AI98Evals94Classifier & causal discovery86Forecasting time78Flow matching72Training & fine-tuning56Teacher policy distillation51All 32 fields

Open problems across fields

  • General in-context learning for embodied agents1 paper raises it · 0 address it

    Enables models to adapt to new tasks and environments without retraining, improving robustness in real-world deployment.

    • Has GPT-6-Astra Achieved Embodied Intelligence?raises
  • Cost and latency in embodied control loops1 paper raises it · 0 address it

    High computational and time costs limit real-time applicability of agentic systems in dynamic environments.

    • Has GPT-6-Astra Achieved Embodied Intelligence?raises
  • Physical-state verification and failure recovery1 paper raises it · 0 address it

    Agents must reliably detect and correct errors in physical interactions to avoid irreversible failures in real-world tasks.

    • Has GPT-6-Astra Achieved Embodied Intelligence?raises
  • Long-horizon task preservation in embodied agents1 paper raises it · 0 address it

    Maintaining progress over extended sequences is critical for complex, multi-step tasks in robotics and navigation.

    • Has GPT-6-Astra Achieved Embodied Intelligence?raises
  • Open-source stacks for generalist computer-use agents1 paper raises it · 1 addresses it

    Closed systems hinder reproducibility and systematic study of agent design for real-world computer tasks.

    • OpenGCUA: Toward a Fully Open Stack for Generalist Computer Useraises · addresses

Named by an AI from these papers' abstracts.

Papers

  • arXiv cs.LGOct 18

    PACT: NVFP4 Data-Flow LoRA Fine-Tuning on Consumer GPUs

    Lei Gao, Hossein Entezari Zarch, Chaoyi Jiang, Murali Annavaram

    Fine-tuning language models on consumer GPUs is constrained by computation and memory. Although LoRA reduces trainable parameters and optimizer state, frozen projections remain expensive, and activations retained for backward can dominate memory usage. We present PACT, a LoRA fine-tuning system that accelerates frozen projections with native NVFP4 GEMMs while reducing quantization and dequantization overhead and limiting quantization error. To reduce activation memory, PACT reuses quantized RMSNorm outputs and saves gate/up activations in NVFP4 for backward. To limit numerical error, it preserves BF16 inputs for forward nonlinear operations and calibrates frozen weights offline using GPTQ adapted to NVFP4 scales and quantized activations. Fused nonlinear kernels and cached forward and backward weight layouts reduce quantization and dequantization overhead. Evaluations across multiple models and tasks on a 16\,GB RTX~5080 show lower memory usage and faster LoRA fine-tuning with competitive accuracy, enabling model adaptation on resource-constrained consumer hardware.

    PDF
  • arXiv cs.AIOct 18

    SteadyThought: Mitigating LLM Under-Thinking via Thought-Level Preference Optimization

    Zhenyue Peng, Lin Yang, Jie Wang, Xiaoqi Ni, Hanzhu Chen +5

    Flexible switching between reasoning trajectories (i.e., thought switching) has significantly enhanced the reasoning capabilities of Large Reasoning Models (LRMs). However, existing models often switch excessively yet fail to sustain promising reasoning thoughts, a phenomenon termed "under-thinking". While recent efforts suppress switching to mitigate this, such over-correction may discard valuable trajectories. To address this challenge, we propose Steady Thought (ST), a novel thought-level preference optimization framework. ST formalizes under-thinking as a preference issue at switching points, forcing single-path continuations from identified points to yield high-quality reasoning. Then, ST performs thought-level preference optimization by treating the newly generated response as preferred and the original one as dis-preferred. Experiments across multiple models and datasets show that ST effectively reduces token consumption, achieving reductions of up to 63.8%, while maintaining strong reasoning accuracy. Further analysis suggests that ST helps models acquire a generalizable ability to reduce redundant switching across domains and languages. Code is available at…

    PDF
  • arXiv eess.SPOct 18

    Normalizing Flow for Neural-Enhanced Track-Before-Detect

    Shaoxiu Wei, Bhaskar Rao, Florian Meyer

    Multiobject tracking (MOT) is a fundamental capability in autonomous navigation, radar and sonar systems, as well as 6G integrated sensing-and-communication (ISAC) networks. In this paper, we propose a neural-enhanced track-before-detect (TkBD) framework that operates directly on complex-valued raw signals and learns a latent representation of unmodeled propagation effects during runtime. We introduce an environment-dependent latent intensity variable that characterizes the signal power of each object in the shared propagation environment. The probability density function of this intensity variable is represented by a normalizing flow and trained online in an unsupervised manner within the sequential Bayesian inference procedure. The learning objective is derived from a variational Bayes formulation by maximizing the evidence lower bound (ELBO), thereby accounting for the uncertainties inherent in the Bayesian TkBD problem. To enable scalable inference, we make use of a recently introduced Bayesian TkBD framework that combines belief propagation, which avoids high-dimensional operations, with sequential Monte Carlo methods for efficient low-dimensional updates.

    PDF
  • arXiv cs.AIOct 18▲ 59

    VLA-Rolling: Fewer Denoising Steps, Better Control via Adaptive Action Reuse

    Sicheng He, Yi Pan, Qiuting Yu, Jiaming Huang, Qi Lu +8

    Flow-matching vision-language-action (VLA) models generate an action chunk by iteratively denoising Gaussian noise, but typically execute only a short prefix before replanning with updated observations. Under this receding-horizon paradigm, the unexecuted remainder---the action tail---is discarded, and the next chunk is regenerated from fresh noise. We show that this discarded tail retains transferable denoising progress: action-tail initialization can match or outperform a native 10-step Gaussian baseline using fewer denoising steps. However, the optimal denoising budget varies substantially across samples, indicating that tail reuse should be adapted to the updated environment. Based on this observation, we introduce VLA-Rolling, a lightweight inference framework that reuses action tails through three stages: action-tail inheritance, per-action confidence estimation, and confidence-guided refinement through renoising and denoising budget allocation, while the underlying VLA remains frozen. Across $π_{0.5}$, SmolVLA, X-VLA, and MolmoAct2 on LIBERO, MetaWorld, LIBERO-Plus, and RoboTwin 2.0, VLA-Rolling reduces action-chunk inference cost in all 16 model--benchmark pairs,…

    Code
  • arXiv cs.LGOct 18

    Beyond the Teacher: Understanding and Preserving Distillation Overshoot in Agentic On-Policy Distillation

    Jike Zhong, Ming Li, Yuxiang Lai, Xi Xiao, Sheng Zhang +7

    On-policy distillation (OPD) trains agents on their own trajectories using supervision from a stronger teacher. We uncover a counterintuitive phenomenon in multi-turn agentic tasks: a smaller, initially weaker student can substantially outperform its teacher during training, only to regress as distillation continues. We term this phenomenon distillation overshoot. Through decision- and task-level analyses, we trace overshoot to two competing effects of OPD: repairing weak student decisions and eroding successful student choices that the teacher disfavors. Early in training, repair outpaces erosion, allowing the student to combine the teacher's corrections with its own strengths and surpass the teacher. As training continues, erosion overtakes repair, causing these gains to vanish. Motivated by this finding, we propose Success-Preserving On-Policy Distillation (SPOD), which selectively masks conflicting teacher supervision on successful student choices and introduces a soft probability floor to counteract their erosion, while retaining teacher guidance elsewhere. SPOD requires only binary episode success and model probabilities already available during OPD. Across two model…

    PDF
  • arXiv cs.CLOct 18

    One Head Away from Language Confusion: Single Attention Heads Across Model Families

    Jiwon Jeong, Anjelo Jann Laroza, Chaewoon Yoon, Arjun Pillai, Pranav Kokati +2

    Large language models sometimes reply in an unexpected language, a failure known as language confusion. We ablate individual attention heads in 12 model checkpoints spanning seven model series, using FLORES-200 continuations in five languages and Language Confusion Benchmark (LCB) chat replies. In ten models, zeroing one head causes substantially more departures from the expected language than zeroing any other head in its layer; its LCB pass-rate drop persists, though reduced, under mean ablation. Seven heads move 8.0 to 51.5 percent of all FLORES continuations out of the prompt's language, versus at most 1.4 percent for other same-layer heads; the other three mainly affect explicitly requested languages. These seven heads matter less in base models given plain text. In two models, replacing the values a head reads at the requested-language name with another language's mean makes replies fail and shifts some into that language, unlike a random change of equal size. Replacing a head's output with another language's mean redirects 84 to 99 percent of scored non-English monolingual LCB replies into that language in five models. Yet the requested language's mean improves…

    PDF
  • arXiv stat.MLOct 18

    Quadratic Sample Complexity for Strictly Replicable Realizable Learning with Unknown Marginals

    Guangjian Zhang

    Under the quantifier $\exists A\,\forall D$, where the realizable distribution and its marginal are unknown, we determine the finite-class sample-complexity exponent for strict replicability: two independent samples and one shared seed must produce identical functions. For $\varepsilon=δ=ρ=10^{-4}$, the worst case over $|H|\le M$ is $Θ((\log M)^2)$, without iterated logarithms. For $d\ge1$, $0<\varepsilon\le1/16$, and $0<δ,ρ\le10^{-3}$, every randomized, possibly improper learner valid throughout an explicit anchored realizable family requires $Ω(d^2/(\varepsilonρ^2))$ samples. For the full Boolean class $P_d$, $d\ge2$, in the same parameter range, we prove the matching characterization $Θ(d^2/(\varepsilonρ^2)+\varepsilon^{-1}\log(1/δ))$ using a proper Poissonized ball-sampling algorithm. We also give an explicit proper Gibbs upper bound for every finite measurable Boolean class. Our lower bound uses square-root probabilities and volumetric packing; the Gibbs proof builds on established coupling and generalization identities. Finally, we characterize the known-marginal worst case for $P_d$, showing why that interface must be kept distinct.

    PDF
  • arXiv math.NAOct 18

    Integrable building blocks for symplectic neural networks: learned-type layers, fiber-preserving layers, and what a single layer can do

    Andrew Qing He

    Exactly symplectic neural networks are built almost exclusively from shear maps and gain expressivity only through depth. We ask what else a single explicit symplectic layer can be. Observing that every layer in use is the exact flow of a Hamiltonian that is a function of commuting integrals, we obtain three families of layers: a learned-type layer, in which every conjugate pair is rotated, squeezed or sheared by a state-dependent amount and the type is found by training; moving-plane shears, residual symplectic maps outside the known ridge-function class; and fiber-preserving layers, which combine an unconstrained point transformation with a fiber translation at the cost of one linear solve. We characterize residual symplectic layers $x \mapsto x + J\nabla H(x)$: in one degree of freedom they are exactly the shears along a line, while from two degrees of freedom on a strictly larger class exists. Conjugating a learned-type layer by a symplectic network yields an exact one-parameter group with an exactly conserved learned Hamiltonian. In experiments on sixteen systems with one to forty degrees of freedom, against SympNets, HénonNets and learned-plane shear networks, layers built…

    PDF
  • arXiv cs.LGOct 18

    Synergy-Aware Residual Flow Matching for Single-Cell Perturbation Prediction

    Jingrui Wu, Wangyun Dan

    Predicting single-cell responses to genetic and chemical perturbations is important for understanding regulatory mechanisms and prioritizing therapeutic interventions. Existing methods have made progress by modeling perturbation-conditioned expression shifts with neural networks, graph priors, foundation-model representations, or distributional generative models. However, combinatorial perturbation prediction remains challenging because much of the response can be explained by additive single-perturbation effects, while the biologically informative signal often lies in a smaller non-additive residual induced by perturbation interactions. Directly generating the full post-perturbation expression profile may therefore allocate substantial capacity to the dominant additive component and underemphasize synergy-specific structure. To address this issue, we propose \textbf{SynGeneFlow}, a synergy-aware flow matching framework that anchors the source distribution at an additive prior and learns a residual flow toward the true perturbed state. SynGeneFlow further incorporates perturbation-conditioned gene interaction modeling, where a static gene-gene mask provides biological structure…

    PDF
  • arXiv cs.LGOct 18

    LLM Agents as Suppliers of Physical System Models: Calibration and Acceptance in Modelica

    Jörg Frochte, Herbert Schmidt

    To procure a model of a device, a client hands a supplier a description, sometimes with recorded data or a target response, and accepts the model against this handover. We let LLM coding agents act as the supplier on handovers with data, building Modelica models from library components for four simulated systems and a real switching magnet, and ask what acceptance certifies. Several agents reach the noise floor, but a handover admits a set of models: the description leaves parts of the structure open, and the data narrow it only to the agreed accuracy. We therefore accept by membership in this set, not by matching one reference, and add layers above behaviour: a physical invariant exposes an energy-creating model at the noise floor. Interpretability becomes a property of the delivered model, tested on a variant, read where none exists and shaped through the handover. Most failures are fits delivered with a systematic residual on their own fitting data, where the handover left open how close is close enough. In a follow-up, stating a threshold makes the agents compare against it, and more deliveries pass. The argument applies wherever a handover underspecifies a model meant to be…

    PDF
  • arXiv cs.PLOct 18

    Structure-Aware Equivalence for Evaluating Autoformalized Statements

    Yi Yu, Yu-Hsuan Wu, Guang Lin, Yuhui Zhang, Yuxiang Peng

    Evaluating autoformalized mathematical statements requires determining whether a candidate preserves the mathematical claim intended by a trusted reference. Existing methods approach this problem from complementary directions: reference-free learned evaluators estimate semantic agreement but are not constrained to a formal equivalence relation, while reference-based proof methods typically employ whole-statement logical equivalence to provide formal certificates, which is too coarse for translation fidelity and may identify mathematically unrelated statements. We introduce Structure-Aware Equivalence (SAE), a role-preserving formal equivalence relation between syntactic and whole-statement logical equivalence that allows formally justified reformulations while preserving translation-relevant mathematical structure. We operationalize SAE in the Autoformalization Correctness Evaluator (ACE), which provides certified equivalence or inequivalence judgments and reports Inconclusive otherwise. On ProofNetVerif, a benchmark introduced with BEq+, ACE retains substantial equivalent-case coverage while remaining highly conservative in certifying disputed or inequivalent pairs. On targeted…

    PDF
  • arXiv cs.LGOct 18

    Decentralized Online Exp-Concave Optimization

    Hao Qiu, Mengxiao Zhang, Yuanyu Wan

    Decentralized Online Convex Optimization (D-OCO) is a fundamental framework in which a set of local agents aims to minimize a sequence of global loss functions using only local computations and communications. While recent work has established near-optimal regret guarantees for convex and strongly convex losses, the case of exp-concave losses remains an open challenge: specifically, whether logarithmic regret is achievable. In this paper, we answer this question affirmatively by proposing Decentralized Online Newton Step (D-ONS), which adapts the idea of blocking and accelerated gossip to the Online Newton Step algorithm in a non-trivial manner. Concretely, our algorithm achieves a regret bound of $O\left(Nd(1-σ_2)^{-1/2}\,\log^2(T) \right)$ where $N$ is the number of agents, $d$ is the dimension, $T$ is the horizon, and $1-σ_2$ represents the spectral gap of the network. To our knowledge, this is the first logarithmic regret bound for decentralized online exp-concave optimization. We further establish a nearly matching lower bound of $Ω\left(Nd (1-σ_2)^{-1/2}\,\log(T/N) \right)$ showing the near optimality of our upper bound. Finally, we extend our algorithm to decentralized…

    PDF
  • arXiv cs.LGOct 18

    Multifidelity Monte Carlo Estimator for High-Dimensional Quantities of Interest

    Zhibo Dai, Hamdi A. Tchelepi, Daniel M. Tartakovsky

    Multifidelity Monte Carlo (MFMC) reduces the cost of estimating the statistics of quantities of interest (QoIs) computed via expensive high-fidelity model by using cheaper low-fidelity models as control variates. We extend MFMC to vector-valued QoIs by replacing the scalar control-variate coefficients with matrices and minimizing a weighted mean-squared error. The optimal full-matrix coefficients are available in closed form, and their variance reduction is summarized by an effective correlation that takes the place of the squared Pearson correlation in the closed-form MFMC design. Restricting the coefficients to block-diagonal, diagonal, and scalar classes gives a nested hierarchy of estimators with increasing variance reduction and increasing pilot-data demand, with closed-form coefficients for compatible weightings. For a scalar QoI obtained by linearly projecting the state, correcting the full state before projecting is never worse at the population level. Experiments on a Gaussian problem, a reduced-order model of an advection--diffusion problem, and a coarse-grid two-phase flow problem show that the best class depends on the pilot size relative to the number of covariance…

    PDF
  • arXiv cs.CVOct 18

    IECLA: Interpretable Emotion Contribution Learning for Affective Image Editing

    Yijie Guo, Dexiang Hong, Weidong Chen, Xinyan Liu, Zhendong Mao

    Affective image editing (AIE) aims to evoke a target emotion while preserving the content and structure of a source image. Existing methods improve emotional expression or visual fidelity, but the target emotion alone does not reveal which source regions should be changed and which should remain intact, especially in complex scenes. We introduce Interpretable Emotion Contribution Learning for Affective Image Editing (IECLA), a framework that separates source-emotion attribution from target-aware editing. IECLA constructs signed object-level supervision through counterfactual interventions and trains a context-conditioned contribution predictor to localize evidence that supports or opposes the source emotion. At inference, an image-level evaluator estimates the source emotion directly from the input, while the predictor identifies editable and preservation evidence without repeated interventions. A target-aware editing agent then translates this evidence and the desired emotion into localized, content-aware operations for existing editors. Extensive evaluations show that IECLA predicts counterfactual contributions more faithfully on both in-domain and cross-dataset tests, while…

    PDF
  • arXiv cs.LGOct 18

    Latent World Models Should Plan with Distances Along the Latent Manifold

    Zunzhi You, Linwei Tao, Siyu Xu, Yunke Wang, Chang Xu

    Latent world models such as LeWM plan by searching for an action sequence whose predicted terminal latent is closest to the goal latent under an ambient norm, such as the Euclidean distance. Planning with such a cost assumes that proximity in the ambient latent space reflects proximity to the goal in the environment. Studying LeWM, we find that this assumption holds only in a small neighborhood around the goal, whereas farther away the L2 cost forms spurious low-cost basins that trap the planner. Yet neighborhood-based embeddings show that the latents retain the underlying physical state. We therefore hypothesize that the latents lie near a curved, low-dimensional manifold, and that the terminal cost should measure the distance along this latent manifold rather than through the ambient space. To estimate this manifold distance, we propose the Neighborhood Graph Cost (NGC), which computes shortest-path distances on a mutual nearest-neighbor graph constructed over training latents. NGC changes only the terminal cost and requires no retraining. This single change improves the planning success rate of LeWM across all four benchmark tasks and nearly solves TwoRoom and Reacher: even at…

    PDF
  • arXiv cs.LGOct 18

    Conjugate Compilation: Self-Improving Agentic Co-Compilation for Speculative Decoding

    Annabelle Sujun Tang, Rohan Mahapatra, Christopher Priebe, Hanyang Xu, Manya Ghobadi +2

    As LLM adoption surges, scaling model serving requires unlocking stranded GPU capacity alongside deploying more GPUs. Speculative decoding brings two models into the serving process: a small draft model proposes tokens that a larger target model verifies. Yet compiling these models individually leaves their shared execution outside the compiler's optimization boundary. We introduce CONJUGATE COMPILATION, which reframes speculative decoding as a cross-model compilation problem and jointly optimizes the draft and target models within their shared execution rather than treating each in isolation. Our key insight is that cross-model compilation should be informed by the measured performance of the co-located shared execution it produces: an optimization that improves a kernel in isolation need not improve the models when they execute together. To expand cross-model opportunities, we devise operand layouts that interleave blocks from both models within common tiles, co-locating GEMM and non-GEMM work while preserving their mathematics. We realize CONJUGATE COMPILATION through a self-improving agentic search system in which an LLM edits cross-model optimization plans using the compiler…

    PDF
  • arXiv cs.CVOct 18▲ 18

    FineSplat: Fine Patches, Local Groups, Detailed Splats

    Hyebin Kim, Hwasik Jeong, Joonhyuk Park, Gyeongjin Kang, Jungwoo Kim +2

    Feed-forward 3D Gaussian Splatting (3DGS) promises instant scene reconstruction with high-quality novel-view synthesis. Yet, fine-grained geometry and appearance remain difficult to recover, motivating us to revisit how feed-forward models represent, aggregate, and refine detailed visual information. We introduce FineSplat, a feed-forward 3DGS framework built around fine-grained image patches. Since global multi-view attention becomes prohibitively expensive at such high token resolutions, we develop a dual-grouping strategy that combines two complementary forms of locality: view-wise grouping enables efficient interaction among neighboring views, while 3D spatial grouping reconnects geometrically related tokens that may never have interacted under view-wise grouping by lifting them into the 3D scene space. We further leverage reconstruction error as direct feedback, providing an explicit rendering-based signal to recover fine-grained structures and appearance, thereby overcoming the limitations of one-pass feed-forward prediction. Finally, a compact Gaussian generation scheme preserves the benefits of fine-grained features without unnecessarily increasing the number of…

    Code
  • arXiv cs.AIOct 18

    MAMath-Bench: Process-Aware and Robust Evaluation of Multimodal Multi-Agent Mathematical Reasoning

    Xinping Wang, Jie Ma, Rui Xing, Wensong Guo, Xiayi Zhang +4

    Mathematical reasoning is a fundamental capability for educational applications of Large Language Models (LLMs), where reliable problem solving requires not only correct answers but also coherent and verifiable reasoning processes. Multi-agent systems (MASs) have shown growing potential in this domain by leveraging collaboration and verification among multiple LLM agents. However, existing evaluations primarily focus on the correctness of final answers in text-only settings, offering limited insight into multimodal reasoning capabilities, the reliability of intermediate reasoning steps, and robustness against reasoning errors. To address these limitations, we introduce MAMath-Bench, a process-aware benchmark designed to evaluate the multimodal mathematical reasoning capabilities of MASs. MAMath-Bench comprises 1,003 problems spanning 11 mathematical categories, multiple difficulty levels, and several modalities, including text, images, and audio. It features fine-grained milestone annotations to evaluate systems across three dimensions: problem-solving correctness, reasoning-process reliability, and robustness to adversarial reasoning-chain perturbations. Our evaluation yields…

    PDF
  • arXiv cs.DSOct 18

    No Escape from the Quadratic Barrier: Adaptive Attacks on Linear $\ell_2$ Sketches

    Edith Cohen, Uri Stemmer

    Linear sketches estimate properties of high-dimensional inputs from a fixed low-dimensional projection. At constant accuracy, randomized Euclidean-norm sketches, notably the Johnson-Lindenstrauss transform, support exponentially many nonadaptive queries in sketch dimension $k$. For adaptive black-box queries, known privacy-based defenses guarantee $\widetildeΩ(k^2)$ and it remained open whether stronger guarantees were possible. Prior attacks used more queries, restricted the responder, or provided weaker failure guarantees. We show that the quadratic guarantee is optimal up to logarithmic factors, even with a computationally unbounded responder that knows the matrix, attack algorithm, history, and query distributions and may change its randomized rule after every query. For every fixed hidden $A\in\mathbb{R}^{k\times n}$ with $n>40k$ and target accuracy $α\in (0,1]$, our black-box attack uses $O(k+α^2k^2\log(2+α^2k))$ queries in $\widetilde{O}(1+α^2k)$ adaptive rounds to force, with constant probability, a round in which a constant fraction of answers have $Ω(α)$ relative error. Our results clarify the limits of defending a fixed compressive linear representation by adapting the…

    PDF
  • arXiv cs.AIOct 18

    Fix, Not Just Resample: Bounded Compiler-Guided Repair in Lean 4

    Haotian Deng, Chris Farber, Sonal Narasimha, Samskrithi Sivakumar, Yexiang Xue

    Automated theorem provers often rely on sampling language models, but proof assistants like Lean reject each failed step with a precise error message --- information that pure sampling discards. To overcome this, we introduce a bounded, online step-level repair module. Our search samples $K$ candidate tactics at each step and repairs a failed tactic at most $R$ times. Instead of discarding failed tactics, we feed the compiler's error message to a pretrained repair model to fix individual rejected steps in place. This approach improves the solve rate over a sampling-only baseline across all tested candidate budgets ($K \in \{1,3,5,8\}$), achieving up to a $32\%$ relative gain and solving $82$ additional theorems on a $1{,}990$-theorem subset of the LeanDojo benchmark. Repair is not free: it trades extra runtime for reachable proofs. But the trade is predictable: repair pays most when sampling is constrained; its return is front-loaded, with the first repair attempt capturing $84\text{--}96\%$ of the total gain; and the gain comes almost entirely from shallow tactic-execution failures rather than structural errors such as type mismatches. This targeted repair successfully…

    PDF
Load more
PDF
PDF

Rising research topics

Coming with more sources: more tagged papers
  • Small LLMs11+1000.0%
  • AI safety42+740.0%
  • Training & fine-tuning56+600.0%
  • Robotics28+600.0%
  • Image & video generation34+580.0%
  • Evals93+520.0%
  • Computer vision43+437.5%
  • Code models20+400.0%