papers checked against Recognition
Pith ran a Recognition coverage check on each paper here and surfaced at least one Lean theorem in the public Recognition library that looks relevant to the paper's claims. The link is Pith's machine assessment, not a citation by the paper. Click into the paper for the full Pith review and the suggested theorem matches.
60 of 33886 papers
-
Relative numbers of ends and quasi-median graphs
math.GR · 2026-04-08 · 3 theorem links
Relative ends and coends for group-subgraph pairs are characterized in terms of actions on quasi-median graphs, extending Sageev's codimension-one subgroup result.
-
Gravitational Memory from Hairy Binary Black Hole Mergers
gr-qc · 2026-04-10 · 3 theorem links
Gravitational memory from hairy binary black hole mergers in scalar-Gauss-Bonnet gravity differs from GR by a few percent due to altered nonlinear dynamics, with direct scalar contributions suppressed, and including memory increases GR-sGB mismatch by more than an order of magnitude.
-
Exoplanet Orbital Distribution around FGK Sun-like Host Stars II: a valley in the orbital semi-major axis distribution of sub-Neptunes
astro-ph.EP · 2026-04-09 · 3 theorem links
A valley in sub-Neptune semi-major axes is presented as evidence for orbital quantization from standing waves in the inner protoplanetary disk.
-
Development of a Simple Stellarator using Tilted Circular Toroidal Field Coils
physics.plasm-ph · 2026-04-08 · 3 theorem links
A stellarator built from tilted circular TF coils and compensating PF coils produces nested magnetic surfaces with low neoclassical transport and favorable alpha-particle confinement after optimizing coil radius and tilt angle.
-
LiveCodeBench: Holistic and Contamination Free Evaluation of Large Language Models for Code
cs.SE · 2024-03-12 · 3 theorem links
LiveCodeBench collects 400 recent contest problems to create a contamination-free benchmark evaluating LLMs on code generation and related capabilities like self-repair and execution.
-
DeepSeek-Coder: When the Large Language Model Meets Programming -- The Rise of Code Intelligence
cs.SE · 2024-01-25 · 3 theorem links
DeepSeek-Coder open-source models trained on 2T code tokens with fill-in-the-blank pretraining achieve SOTA results among open models and surpass closed-source Codex and GPT-3.5 on code benchmarks.
-
Hierarchical Text-Conditional Image Generation with CLIP Latents
cs.CV · 2022-04-13 · 3 theorem links
A hierarchical prior-decoder model using CLIP latents generates more diverse text-conditional images than direct methods while preserving photorealism and caption fidelity.
-
Training language models to follow instructions with human feedback
cs.CL · 2022-03-04 · 3 theorem links
Fine-tuning GPT-3 on human demonstrations followed by reinforcement learning from human preference rankings yields smaller models that humans judge superior to the much larger base model on instruction following, truthfulness, and reduced toxicity.
-
Semantic Rate-Distortion Theory: Deductive Compression and Closure Fidelity
cs.IT · 2026-04-13 · 3 theorem links
Semantic rate-distortion theory shows that under closure fidelity the rate-distortion function depends only on the irredundant core, yielding zero-distortion rates strictly below classical entropy and semantic leverage in source-channel coding.
-
Phase-Field Peridynamics
cs.CE · 2026-04-10 · 3 theorem links
Phase-field peridynamics degrades bond energies continuously via a bond phase-field parameter while using kinematic degradation to preserve nonlocal deformation gradient accuracy, with an analytically derived normalization constant for thermodynamic consistency.
-
GenTac: Generative Modeling and Forecasting of Soccer Tactics
cs.AI · 2026-04-13 · 3 theorem links
GenTac applies diffusion models to generate diverse, style-conditioned multi-agent trajectories and 15-class tactical events for soccer, supporting counterfactual rollouts and outcome prediction.
-
The Large N Limit of Superconformal Field Theories and Supergravity
hep-th · 1997-11-27 · 3 theorem links
The large N limit of superconformal field theories is dual to supergravity on Anti-de Sitter spacetimes.
-
EMBER: Autonomous Cognitive Behaviour from Learned Spiking Neural Network Dynamics in a Hybrid LLM Architecture
cs.AI · 2026-04-14 · 3 theorem links
A hybrid SNN-LLM system uses learned spiking dynamics and lateral STDP propagation to trigger LLM actions without external prompts, producing the first autonomous action after 7 exchanges from a clean start.
-
How to deal with conformal and pure scale-invariant theories of gravity in d dimensions?
hep-th · 2026-04-10 · 3 theorem links
Conformal and scale-invariant gravity theories in d dimensions have distinct properties from 4D analogues, enabled by a new formulation method.
-
Minimal Embodiment Enables Efficient Learning of Number Concepts in Robot
cs.RO · 2026-04-13 · 3 theorem links
Minimal robotic embodiment boosts data-efficient learning of number concepts and produces brain-like representations including logarithmic tuning and mental number lines.
-
Entropic independence via sparse localization
cs.IT · 2026-04-13 · 3 theorem links
Sparse localization deduces entropic independence from sparse ℓ2-independence with explicit loss, yielding approximate entropy conservation for uniform independent sets of fixed size in bounded-degree graphs.
-
Quantum Geometry, Fractionalization, and Provability Hierarchy: A Unified Framework for Strongly Correlated Systems
physics.gen-ph · 2026-04-13 · 3 theorem links
The paper claims five discoveries that unify quantum geometry with fractionalization and a new provability hierarchy in strongly correlated systems, including golden-ratio scaling and links to unprovable QMA-hard problems.
-
Spectral Operadic Calculus: Norm-Analytic Functor Calculus
math.CT · 2026-05-02 · 3 theorem links
An operadic spectrum acts as a control parameter for a norm-analytic functor calculus, delivering criteria for polynomial behavior, exponential convergence bounds on Taylor towers, and a reconstruction theorem from derivative data via operadic plethysm.
-
Qwen-Image Technical Report
cs.CV · 2025-08-04 · 3 theorem links
Qwen-Image is a foundation model that reaches state-of-the-art results in image generation and editing by combining a large-scale text-focused data pipeline with curriculum learning and dual semantic-reconstructive encoding for editing consistency.
-
LLaVA-OneVision: Easy Visual Task Transfer
cs.CV · 2024-08-06 · 3 theorem links
LLaVA-OneVision is the first single open LMM to simultaneously achieve strong performance in single-image, multi-image, and video scenarios with cross-scenario transfer capabilities.
-
Training a Helpful and Harmless Assistant with Reinforcement Learning from Human Feedback
cs.CL · 2022-04-12 · 3 theorem links
RLHF alignment training on language models boosts NLP performance, supports skill specialization, enables weekly online updates with fresh human data, and shows a linear relation between RL reward and sqrt(KL divergence from initialization.
-
Flow Straight and Fast: Learning to Generate and Transfer Data with Rectified Flow
cs.LG · 2022-09-07 · 3 theorem links
Rectified flow learns straight-path neural ODEs for distribution transport, yielding efficient generative models and domain transfers that work well even with a single simulation step.
-
Mamba: Linear-Time Sequence Modeling with Selective State Spaces
cs.LG · 2023-12-01 · 3 theorem links
Mamba is a linear-time sequence model using input-dependent selective SSMs that achieves SOTA results across modalities and matches twice-larger Transformers on language modeling with 5x higher inference throughput.
-
Laser Interferometer Space Antenna
astro-ph.IM · 2017-02-02 · 3 theorem links
Pith review generated a malformed one-line summary.
-
Pattern detection in ordered graphs
cs.DS · 2023-02-22 · 3 theorem links
Pith review generated a malformed one-line summary.
-
DINOv2: Learning Robust Visual Features without Supervision
cs.CV · 2023-04-14 · 3 theorem links
Pith review generated a malformed one-line summary.
-
The AI Scientist-v2: Workshop-Level Automated Scientific Discovery via Agentic Tree Search
cs.AI · 2025-04-10 · 3 theorem links
Pith review generated a malformed one-line summary.
-
U-Net: Convolutional Networks for Biomedical Image Segmentation
cs.CV · 2015-05-18 · 3 theorem links
A u-shaped fully-convolutional encoder-decoder with skip connections trained with elastic-deformation augmentation produces accurate biomedical image segmentations from very small training sets.
-
A Gentle Introduction to Conformal Prediction and Distribution-Free Uncertainty Quantification
cs.LG · 2021-07-15 · 3 theorem links
Pith review generated a malformed one-line summary.
-
Qwen3 Technical Report
cs.CL · 2025-05-14 · 3 theorem links
Pith review generated a malformed one-line summary.
-
Outrageously Large Neural Networks: The Sparsely-Gated Mixture-of-Experts Layer
cs.LG · 2017-01-23 · 3 theorem links
A noisy top-k gated mixture-of-experts layer between LSTMs scales neural networks to 137B parameters with sub-linear compute, beating SOTA on language modeling and machine translation.
-
Proximal Policy Optimization Algorithms
cs.LG · 2017-07-20 · 3 theorem links
A clipped surrogate objective L^CLIP = E[min(r_t A_t, clip(r_t, 1-ε, 1+ε) A_t)] enables multi-epoch minibatch policy updates with TRPO-like stability but first-order optimization.
-
Lost in the Middle: How Language Models Use Long Contexts
cs.CL · 2023-07-06 · 3 theorem links
Pith review generated a malformed one-line summary.
-
Constitutional AI: Harmlessness from AI Feedback
cs.CL · 2022-12-15 · 3 theorem links
Pith review generated a malformed one-line summary.
-
Euclid Definition Study Report
astro-ph.CO · 2011-10-14 · 3 theorem links
Pith review generated a malformed one-line summary.
-
The Llama 3 Herd of Models
cs.AI · 2024-07-31 · 3 theorem links
Llama 3 is a herd of dense Transformer language models, up to 405B parameters with 128K context, released with weights and reported as competitive with GPT-4 on a broad benchmark suite.
-
CvxCluster: Solving Large, Complex, Granular Resource Allocation Problems 100-1000x Faster
cs.DC · 2026-05-02 · 3 theorem links
CvxCluster reformulates cluster resource allocation as a convex problem solved via relaxation for prices followed by greedy placement, achieving 100-2500x speedups over MIP solvers while staying within 3% of optimal on large Azure traces.
-
The proximal point method and its two variants for monotone vector fields in Hadamard spaces
math.FA · 2026-05-02 · 3 theorem links
The proximal point method and its variants converge for monotone vector fields in Hadamard spaces.
-
SteeringDiffusion: A Bottlenecked Activation Control Interface for Diffusion Models
cs.CV · 2026-05-03 · 3 theorem links
SteeringDiffusion supplies a bottlenecked, prompt-conditioned activation interface for frozen diffusion models that delivers smooth monotonic content-style control via one runtime scalar and timestep gating.
-
Brain criticality through nonadditive entropic analysis of electroencephalograms
cond-mat.stat-mech · 2026-05-02 · 3 theorem links
EEG amplitudes follow q-Gaussian distributions where the entropic index q varies monotonically with β, revealing critical brain behavior and higher complexity in ADHD children than typical ones.
-
Can Causal Discovery Algorithms Help in Generating Legal Arguments?
cs.AI · 2026-05-04 · 3 theorem links
Causal discovery applied to annotated homicide cases identifies probabilistic links between legal concepts that can support generation of legal arguments.
-
Generalized Distributional Alignment Games for Unbiased Answer-Level Fine-Tuning
cs.LG · 2026-05-04 · 3 theorem links
Generalized Bregman alignment games plus U-statistics and optimal minimax polynomial estimators remove Jensen bias and achieve optimal statistical rates for unbiased answer-level fine-tuning.
-
Actionable Understanding: Action Units for Bridging the Knowledge-Action Gap in Post-FAIR Knowledge Infrastructures
cs.DB · 2026-05-02 · 3 theorem links
Action Units are introduced as typed, composable components in knowledge graphs that encode epistemic, transformational, and intervention operations with explicit applicability conditions, enabling post-FAIR infrastructures via the TripleA principle.
-
Molecular ISAC via Markov State-Space Modeling: Joint Distance Sensing and Data Detection
eess.SP · 2026-05-03 · 3 theorem links
A Markov state-space model parameterized by distance enables joint TX-RX distance sensing and data detection in molecular communication, yielding accurate sensing and lower bit error rates.
-
Hall-Like Transversal Stress and Sandpile Criticality on Real Production Networks
econ.EM · 2026-05-02 · 3 theorem links
The Hall-Sandpile model on WIOD networks generates four ordered regimes of instability where mean avalanche size and large-event probabilities increase with shock intensity and reduced redundancy, without evidence for universal power-law criticality.
-
SwiftChannel: Algorithm-Hardware Co-Design for Deep Learning-Based 5G Channel Estimation
cs.IT · 2026-05-03 · 3 theorem links
SwiftChannel delivers a compressed CNN-based channel estimator with parameter-free attention running on FPGA, achieving sub-millisecond latency, 24x speedup, and 33x better energy efficiency than GPU baselines while generalizing across noise and channel profiles.
-
ViM-Q: Scalable Algorithm-Hardware Co-Design for Vision Mamba Model Inference on FPGA
cs.AR · 2026-05-03 · 3 theorem links
ViM-Q delivers 4.96x speedup and 59.8x energy efficiency for Vision Mamba inference on FPGA versus a quantized GPU baseline using dynamic activation quantization, per-block APoT weights, and a pipelined SSM engine.
-
Preparing High-Fidelity Thermofield Double States
quant-ph · 2026-05-04 · 3 theorem links
A gapped parent Hamiltonian built from two copies of a target Hamiltonian plus ultra-local inter-copy couplings allows adiabatic preparation of high-fidelity thermofield double states for ETH-obeying systems.
-
Glauber dynamics for random field Ising models on bounded degree graphs and MLSI
math.PR · 2026-05-03 · 3 theorem links
Glauber dynamics for RFIM on bounded-degree graphs mixes in polynomial time w.h.p. under anti-concentrated random fields, with MLSI and weak Poincaré inequalities also established.
-
Decoherence due to the sudden coupling of an impurity to a metal
cond-mat.mes-hall · 2026-05-02 · 3 theorem links
Sudden hybridization quenches induce dephasing via particle-hole excitations, with mixed linear-logarithmic discretization suppressing finite-size revivals to reveal crossover from coherent oscillations to irreversible decoherence.
-
TumorXAI: Self-Supervised Deep Learning Framework for Explainable Brain MRI Tumor Classification
cs.AI · 2026-05-03 · 3 theorem links
Self-supervised pretraining with SimCLR on ResNet-50 achieves 99.64% accuracy on 17-class brain tumor MRI classification, outperforms supervised baselines with limited labels, and includes Grad-CAM explainability.
-
Dependency Parsing Across the Resource Spectrum: Evaluating Architectures on High and Low-Resource Languages
cs.CL · 2026-05-04 · 3 theorem links
Biaffine LSTM outperforms transformer parsers like AfroXLMR and RemBERT in low-resource dependency parsing, with transformers gaining advantage as data increases and morphological complexity as a secondary predictor.
-
Mid-infrared photo-induced force microscopy (IR-PiFM/PiF-IR) -- Answers to some questions
cond-mat.mtrl-sci · 2026-05-03 · 3 theorem links
The manuscript provides explanatory answers to questions on the background, handling, and applications of the IR-PiFM/PiF-IR technique raised during a scientific discussion.
-
Witness Set: A Visibility Problem in $NP\cap XP$
cs.CG · 2026-05-02 · 3 theorem links
Witness Set for simple polygons is in NP ∩ XP and admits an n^{f(k)}-time algorithm via combinatorial discretization, in contrast to its ∃R-complete dual.
-
Waveform Design for 6G ISAC Systems Under Full-Duplex Residual Self-Interference
eess.SP · 2026-05-04 · 3 theorem links
A dual-power phase-coded pulse waveform for full-duplex ISAC eliminates blind range and improves long-range multi-target detection under residual self-interference compared to OFDM and LFM baselines.
-
Constraints on Phenomenological Amplitudes of CMB Anisotropy with Multi-Datasets
astro-ph.CO · 2026-05-03 · 3 theorem links
Lensing amplitude A_L deviates from 1 at up to 3.06 sigma in combined datasets while other phenomenological amplitudes remain consistent with Lambda CDM or are poorly constrained.
-
A Comprehensive Study of Morphology and Kinematics in Extended Nebulae Around UV Luminous Quasars at $z\approx1$
astro-ph.GA · 2026-05-03 · 3 theorem links
Quasar nebulae at z~1 are diverse objects shaped by galaxy interactions, host gas, group environments, and quasar activity, with the largest irregular ones most tied to interactions.
-
Trust, but Verify: Peeling Low-Bit Transformer Networks for Training Monitoring
cs.LG · 2026-05-04 · 3 theorem links
A layer-wise peeling framework creates reference bounds to diagnose under-optimized layers in trained decoder-only transformers, including low-bit and quantized versions.
-
Reference-Sampled Boltzmann Projection for KL-Regularized RLVR: Target-Matched Weighted SFT, Finite One-Shot Gaps, and Policy Mirror Descent
cs.LG · 2026-05-04 · 3 theorem links
Reference-sampled weighted SFT with prompt-normalized Boltzmann weights induces the same policy as fixed-reference KL-regularized RLVR, with BOLT as the estimator and a finite one-shot error decomposition separating coverage, variance, and other terms.
-
A Structure-Preserving Stagewise Rescaling Algorithm for a Two-Dimensional Nonlocal MEMS Equation in an Asymptotically Constant-Feedback Regime
math.NA · 2026-05-04 · 3 theorem links
A structure-preserving stagewise rescaling algorithm is developed and analyzed for 2D nonlocal MEMS equations in the asymptotically constant-feedback touchdown regime, yielding energy dissipation identities and a defect-aware nonexistence criterion.