Notation3 (N3) Logic extends RDF with graph terms—entire graphs used as terms in triples—to support statements about statements and rule-based reasoning. This paper fills a long-standing gap by providing the first comprehensive formal semantics for these graph terms, introducing an abstract syntax and a two-layer semantics (basic entailment followed by N3-entailment for built-in predicates). The work matters because N3 has lacked a standardized model-theoretic account, leaving implementations like EYE and Cwm without a common semantic foundation.

Autoformalization pipelines translate natural mathematical text into theorem-prover code, but current verification relies on LLM judges that miss subtle domain and sign errors. This paper proposes a layered faithfulness verifier that stacks semantic LLM review with mechanical numerical and vacuity checks, and deploys it within an Extract–Verify–Prove pipeline to build the Formalized Library of Mathematical Functions. On three labeled benchmarks the method achieves the lowest accepted-error rate, while also uncovering hundreds of defects in existing datasets.

Reinforcement learning for reachability specifications has been limited to model-based methods that explicitly estimate transition probabilities. This paper introduces Quasar, a model-free Q-learning variant that provably converges to optimal reachability policies on MDPs without non-terminal maximal end components, using only $O(|S||A|)$ memory. By replacing the missing discount factor with an intrinsic expected hitting time, the authors obtain a weighted contraction and demonstrate orders-of-magnitude sample improvements over the state of the art.

Hob-VL introduces a diagnostic benchmark for visually grounded Boolean reasoning, asking vision-language models to evaluate ten-literal Boolean combinations over images and to identify objects satisfying Boolean descriptions. The core idea is to pair each expression with a mechanically verified De Morgan equivalent and to test both symbolic and natural-language presentations, isolating compositional reasoning from surface memorization. It matters because real-world visual queries—warehouse checks, agricultural monitoring, medical imaging—depend on reliably combining multiple visual facts under logical constraints.

Coding agents for Lean can produce compiler-passing proofs that do not match the intended theorem or rely on hidden assumptions. Forall-Lean-Agent tackles this by binding verifier results, fresh review, and artifact digests into a traceable acceptance protocol that works with any frontend. The paper evaluates the harness on software-verification and mathematics benchmarks and argues that auditable execution improves correctness guarantees and efficiency, though its empirical claims are stronger on integrity than on controlled performance gains.

This paper investigates why compressing different weight matrices in transformers leads to wildly different outcomes—from negligible impact to 20,000× perplexity increases. The authors map this structural sensitivity across five architectures, revealing that early-layer MLP up-projections are catastrophically fragile while value projections are nearly free to compress. Using Lyapunov stability theory, they explain how residual connections contract errors, and they provide machine-checked formal bounds in Lean 4 to guarantee per-matrix approximation quality.