Theory & Algorithms · Computer Science & AI
Logic in Computer Science
The newest papers in Logic in Computer Science that ReadSearch has read, newest first. Each links to its own page, with its authors, date, where it was published and the original.
168 papers, from 4 September 2026 to 5 November 2026: 168 arXiv preprints.
Get the few papers worth your time in Logic in Computer Science every morning.
Follow Logic in Computer Science and ReadSearch reads its new papers each day, then brings you the few worth reading, each with its key finding in a sentence.
Newest papers, page 2
From the Transformer to a Formal Semantics of Coordinated Transformations
We develop a formal semantics for a general class of coordinated systems of parameterized transformations, taking the Transformer as a paradigmatic starting point but abstracting from its particular…UPPAAi: Towards LLM-Assisted Modeling, Verification, Analysis and Synthesis
For more than three decades, UPPAAL has supported the modelling and analysis of real-time and cyber-physical systems.Hammering with Vampire in Lean
We present Vampire-Hammer, a hammer for the Lean interactive theorem prover that discharges goals using the Vampire automated theorem prover and reconstructs proofs checked by the Lean kernel.Algebraic World Model: From Exploration to Proofs
AI has made remarkable progress in mathematics, solving challenging problems with machine-checkable proofs in Lean, yet typically relying on predefined mathematical definitions and formal…FARMS: A Verifiable Foundation for Automated Computational Science
Automated computational science could accelerate discovery by selecting, adapting and developing numerical methods.On the Quantum Chromatic Gap II
We confirm a conjecture of the first author [SODA'26] on a strong form of pseudo-telepathy for Khot's $d$-to-$1$ games: for every $d\geq 4$, every $ε>0$, and every $k\in\mathbb N$, there is a…Scaling Lean Theorem Proving for Real-World Code Verification
We present EasyProver, a Lean proving system built from recursive agents with isolated contexts, asynchronous search, parallel tactic probing, and an elastic elaboration service.A Witnessing Duality for ReLU Network Depth
A depth lower bound for ReLU networks asserts that every sufficiently shallow network fails on some input.Order Maintenance in Worst-Case Constant Time, Verified
Order maintenance asks for a data structure that keeps a sequence of elements under insertions and deletions and tells which of two elements comes first.Counting by the Book: Verifying Alaska's Ranked-Choice Elections
We present Alaska's ranked-choice elections as a case study in Formally Verified Democracy, a program to establish election results through formally checked proofs.Log-Derivative Trick for Parametric Markov Chains
Optimizing expected rewards and reachability probabilities in parametric Markov chains (pMCs) is central to the analysis and synthesis of probabilistic systems with loops.An Algebra of Transformers
On the theoretic analyses on transforms, they mainly focus on the computability analysis, such the Turing-completeness of unbounded precision transformers, the advantage of parallelizability of…SoK: Timestamps Are Not a Time Model: Rethinking Temporal Reasoning in Host-Based Intrusion Detection
Host-based intrusion detectors order events, window audit streams and sequence attack stages by their timestamps.Formal Explanations for Linear Temporal Logic over Finite Traces
Linear Temporal Logic over Finite Traces (LTLf) is widely used in Artificial Intelligence to specify desired temporal behavior and determine whether finite traces satisfy or violate it.Ranking Function Generation with LLMs for Termination
Ranking functions are a fundamental technique for proving loop termination, but constructing them manually is challenging and requires substantial expertise.KAPPA: Checking the Proofs in Statistics Papers with Lean 4 and Language Model Agents
Papers in statistical theory rest on long proofs that few readers check line by line.Replication or Corroboration? An Axiomatic Framework for Evidential Dependence in Multi-Agent Debate
In multi-agent debates, matching reports can arise for two different reasons: agents may repeat the same evidence (replication), or they may provide separate evidential roots that support the same…count-catcher: Lean Theorems from Model Counting Certificates
We present count-catcher, a tool that turns a CPOG certificate of a count by the exact model counter d4 into a Lean theorem that a CNF formula defined in Lean has exactly N models over V variables.How Stable Are LLM-Generated Proofs Under Program Refactoring? A Stress Test for Verifiable Code Generation
Benchmarks for verifiable code generation usually test a proof against one fixed implementation.h1: A Taste of the Bitter Lesson in Automated Theorem Proving
While progress in informal mathematics has come largely from scaling the chain-of-thought and agentic reasoning of frontier language models, formal theorem proving has increasingly relied on…