Noticias de IA - ítems

arXiv:2606.20208v2 Announce Type: replace Abstract: Machine learning models are predominantly evaluated through predictive performance metrics such as ranking quality, prediction error, or classification accuracy. While these metrics effectively quantify how closely predictions match the ground truth, they do not assess whether model outputs respect predefined logical or domain-specific constraints. In high-stakes applications, including healthcare, finance, and autonomous systems, logical consistency can be as critical as predictive accuracy, yet no standard metric captures this dimension. We introduce the Rule Violation Score (RVS), a complementary evaluation metric that quantifies the extent to which a predictive model respects a given set of logical rules, independently of predictive accuracy. RVS treats hard rules (strict constraints) and soft rules (statistical regularities) differently, can be evaluated on any dataset and on any predictive model expressed over a relational vocabulary, and can be computed using SQL queries that are automatically generated for Horn rules. Beyond evaluating models, RVS can also evaluate the logical consistency of training datasets and help identify poorly defined rules. We evaluate RVS on three benchmarks covering knowledge graph link prediction and relational regression, including rule-based, embedding-based, and neuro-symbolic predictive models. Our results demonstrate that two models achieving comparable predictive accuracy can exhibit substantially different levels of logical compliance, revealing differences in model behavior that standard metrics fail to capture.

arXiv:2606.16567v3 Announce Type: replace Abstract: Neural ordinary differential equations (neural ODE) gained attention in safety critical settings such as continuous-time controllers for cyber-physical systems and classifiers integrated into automated decision pipelines, raising the question whether their behavior can be formally verified. Existing tools dedicated to neural ODE provide only a single reachability call without iterative input-set refinement, limiting the precision of their verdicts to whatever one reachability call can deliver. We present TNODEV, the first formal verifier for neural ODE that integrates a falsification checker, a fast interval-based reachability backend based on continuous-time mixed monotonicity, a verification and refinement loop with three input-set splitting heuristics, and a parallel scheduler in a single end-to-end pipeline. TNODEV supports safe-set inclusion verification on pure neural ODE, neural ODE in closed loop with a neural network controller and general neural ODE (GNODE), with the safe set specified either as an interval or as the half-space intersection induced by a target classification label. We evaluate TNODEV on a range of benchmarks across safe-set inclusion and classification-robustness properties, including a direct reachability comparison against NNV 2.0 and CORA and a verification comparison against NNV 2.0 on MNIST general neural ODE classifiers.

arXiv:2606.10279v2 Announce Type: replace Abstract: Supervised fine-tuning with synthetic rationales is widely assumed to improve clinical prediction by teaching models not only what to predict but why. We test this assumption on five-year Alzheimer's disease and related dementias (ADRD) prediction from longitudinal health histories. In this setting, we generate training rationales using the correct labels, then fine-tune models to output a rationale followed by a label. Across a large-scale controlled experiment of 504 configurations, we find that Rationale First SFT consistently and substantially hurts predictive performance relative to Label Only fine-tuning. The degradation persists across model families and data scales, and is not resolved by using a reasoning-oriented base model. A fixed-protocol cardiovascular disease (CVD) validation reproduces similar findings. Crucially, the failure is not explained by poor rationale quality: human expert annotation confirms that the generated rationales are medically accurate and faithfully grounded in patient-specific evidence, and few-shot experiments show that the same rationales improve performance when used as inference-time demonstrations rather than training targets. A simple label-ordering intervention clarifies the mechanism: placing the prediction before the same rationale restores predictive performance. This suggests that conditioning predictions on generated rationales contributes to the degradation. We hope our work paves the way toward a more precise understanding of when and how rationale-based supervision helps and when it does not, guiding the responsible development of language models for high-stakes clinical prediction.

arXiv:2606.06523v3 Announce Type: replace Abstract: Equipping Large Language Models (LLMs) to execute reliable multi-step workflows has become a central challenge in artificial intelligence. Despite recent advances in LLMs' agentic capabilities, most agent systems still lack formal methods for specifying, verifying, and debugging their workflow and execution trajectories. This challenge mirrors a long-standing problem in mathematics, where the ambiguity of natural languages (NLs) motivates the development of formal languages (FLs). Inspired by this paradigm, we propose **Lean4Agent**, to the best of our knowledge, the first framework that uses Lean4, a dependent-type FL to model and verify agent behavior. **Lean4Agent** launches **FormalAgentLib**, an extensible Lean4 library for formally modeling and verifying agent workflows' semantic consistency under explicit assumptions, and enabling localization of execution-time failures revealed by trajectories. Building on **FormalAgentLib**, we further develop **LeanEvolve**, which applies results in **FormalAgentLib** to revise workflows to enhance its capability. Extensive experiments on a hard problem subset of SWE-Bench-Verified and a subset of ELAIP-Bench across 5 leading LLMs indicate that the verification-passing workflows outperform the failing ones by an average of **11.94%**, and **LeanEvolve** further improves SWE performance by **7.47%** on average. Furthermore, **Lean4Agent** establishes a foundation for a new field of using expressive dependent-type FL to formally model and verify agent behavior.

arXiv:2606.05433v3 Announce Type: replace Abstract: Proposals for Frontier AI rules often use cumulative training compute as the main criterion for identifying high-impact models. Recent governance analyses call zero-knowledge proofs promising but currently impractical at frontier scale [26, 4]. We argue this barrier reflects the current paradigm, not a fundamental limit. Our frontier dense-pre-training design combines a pre-committed specification, inter-node network observations, and live Merkle commitments to intermediate computation. Our reference zero-knowledge virtual machine (zkVM) provides a succinct proof layer with native BF16/FP32 precompiles. We qualitatively compare zkVMs, custom circuits, and direct interactive audits by transferability, soundness, and cost. Public randomness beacons are a separate audit-selection choice. At challenged positions, proofs check the committed computation against declared BF16/FP32 semantics bit-for-bit. A private training specification targets model-architecture confidentiality. Genesis proofs cover initialisation; then, in-training step proofs verify selected steps across the run. Ex-ante attestations enforce policy-relevant claims as running invariants on every proved step. Together they create a governance-auditable training record. Detection-probability formulas quantify sampling guarantees from the sampling budget and the share of computation altered. We give numerical examples and explain what sampling does not cover. We note, however, that weight smuggling could reuse or merge weights trained elsewhere without charging that work to the current run. We then argue that regimes with global training budgets are more robust than regimes with per-run FLOP caps. This advantage depends on counting all contributing training. We catalogue remaining research and engineering problems for external contributors.

arXiv:2605.09511v2 Announce Type: replace Abstract: Many decisions in complex terrain require fast wind estimates at specific locations and heights rather than dense forecasts on fixed grids. We present WindINR, a latent-state implicit neural representation framework for continuous high-resolution local wind queries and correction using sparse observations. A latent-conditioned decoder maps terrain descriptors, a low-resolution background field, and continuous query coordinates to local wind estimates. WindINR separates reusable representation learning from sample-specific latent correction. During training, a privileged encoder infers reference latent states from high-resolution supervision, while a deployable predictor estimates initial states from inference-time inputs. Their discrepancies define a dataset-adaptive Gaussian prior over latent corrections. At inference time, network weights remain fixed, and only the latent state is updated through a regularized objective incorporating sparse observations and their uncertainty. We train WindINR on the large-scale FuXi-CFD dataset and evaluate it using controlled observing system simulation experiments, simulated helicopter trajectories, and real UAV measurements over Troms{\o}. Across these settings, sparse-observation assimilation consistently improves local wind predictions, with WindINR outperforming several baselines, including WindSeer. Updating only a low-dimensional latent state yields a 14-fold speedup over full-network fine-tuning while preserving continuous queries at arbitrary spatial coordinates. WindINR thus provides an efficient interface between kilometer-scale background products, sparse local observations, and local wind queries in complex terrain.

arXiv:2605.07002v2 Announce Type: replace Abstract: A major bottleneck in characterizing the failure modes of generative AI systems is the cost and time of annotation and evaluation. Consequently, adaptive testing paradigms have gained popularity, where one opportunistically decides which cases and how many to annotate based on past results. While this framework is highly practical, its extreme flexibility makes it difficult to draw statistically rigorous conclusions, as it violates classical assumptions: the number of observations is typically limited (often 10 to 50 cases) and decisions regarding sampling and stopping are made in the midst of data collection rather than based a pre-specified rule. To characterize what statistical inferences can be drawn from highly adaptive audits, we introduce a hypothesis testing framework from two "dueling" perspectives: (i) the model's null that asserts there is no failure mode with performance below a target threshold versus (ii) the auditor's null that asserts they have a sampling strategy that will uncover a failure mode. Leveraging Safe Anytime-Valid Inference (SAVI), we formalize the auditor as conducting "testing by betting," which translates into simultaneous e-processes for testing the dueling null hypotheses. Furthermore, if the auditor is sufficiently powerful, we prove that these two hypotheses are asymptotically inverses of each other, in that passage of such an audit certifies the AI system as being globally robust. Empirically, we demonstrate that our proposed testing procedures maintain anytime-valid Type-I error control, outperform pre-specified testing methods, and can reach statistically rigorous conclusions sometimes with as few as 20 observations.

arXiv:2604.04074v5 Announce Type: replace Abstract: AI is accelerating scientific research, but providing timely and trustworthy feedback remains challenging. Such feedback requires evaluating specific claims against verified evidence, helping researchers and autonomous research systems determine which findings can guide subsequent work. Thorough verification is time-consuming, and reviewers under time pressure may overlook or misjudge critical issues. Existing AI reviewers have yet to fill this gap because they often assess claims without adequately verifying the supporting evidence. We introduce FactReview, a framework that verifies claims in papers to provide more trustworthy feedback. It checks claims against the literature and examines derivations, while also executing the paper's code to test empirical claims. Across 300 papers, FactReview ranks best among all evaluated systems on five of seven metrics, achieving 6.8% false support and 79.2% classification accuracy. In a study of 36 papers, reviewers using FactReview detect 9.4 issues per paper compared with 5.6 independently, while spending 74.1% less time. FactReview thus supports more reliable peer review, with the potential to accelerate research iteration. The code is public at https://github.com/DEFENSE-SEU/FactReview.

arXiv:2603.18712v3 Announce Type: replace Abstract: The task of multi-channel time series forecasting is ubiquitous in numerous fields such as finance, supply chain management, and energy planning. It is critical to effectively capture complex dynamic dependencies within and between channels for accurate predictions. However, traditional method paid few attentions on learning the interaction among channels. This paper proposes Linear-Network (Li-Net), a novel architecture designed for multi-channel time series forecasting that captures the linear and non-linear dependencies among channels. Li-Net dynamically compresses representations across sequence and channel dimensions, processes the information through a configurable non-linear module and subsequently reconstructs the forecasts. Moreover, Li-Net integrates a sparse Top-K Softmax attention mechanism within a multi-scale projection framework to address these challenges. A core innovation is its ability to seamlessly incorporate and fuse multi-modal embeddings, guiding the sparse attention process to focus on the most informative time steps and feature channels. Through the experiment results on multiple real-world benchmark datasets demonstrate that Li-Net achieves competitive performance compared to state-of-the-art baseline methods. Furthermore, Li-Net provides a superior balance between prediction accuracy and computational burden, exhibiting significantly lower memory usage and faster inference times. Detailed ablation studies and parameter sensitivity analyses validate the effectiveness of each key component in our proposed architecture. Keywords: Multivariate Time Series Forecasting, Sparse Attention Mechanism, Multimodal Information Fusion, Non-linear relationship

arXiv:2603.01092v3 Announce Type: replace Abstract: Scientific discovery is constrained not only by what is true, but by what is cognitively available to researchers. Many directions are coherent in light of the literature yet unlikely to be proposed because no existing community combines the relevant concepts, methods, and intuitions. Modern language models inherit this bias, recombining high-density regions of the literature when prompted for novel ideas. We target the complementary region, the alien space of science: directions that are scientifically plausible but unlikely under the distribution of existing researchers. Our method decomposes papers into conceptual units and clusters them into a vocabulary of idea atoms. A coherence model scores whether atom combinations form viable research directions, while an availability model scores whether any existing author community is positioned to produce them. We rank combinations to maximize coherence while minimizing availability. On 16,068 peer-reviewed LLM papers from NeurIPS, ICLR, ICML, and major NLP venues, the sampler produces more diverse research portfolios than frontier LLM baselines, including batch-prompted variants that see their entire output, while matching or exceeding their per-idea quality under blind human, LLM, and downstream experimental evaluation. In temporal validation, all components use only pre-2025 data. Selecting less than 1% of the candidate space recovers 2025 combinations at 35.9 times chance; weighting unavailability increases recovery of strictly novel combinations to 3.24 times chance. By separating scientific plausibility from community availability, our framework points toward AI ideation that complements rather than merely accelerates human science, expanding exploration into coherent directions the community may overlook.