archive
Every paper Pith has read. Search by title, abstract, or pith.
731 papers in cs.LO · page 1
-
Claude agent verifies programs at 98 percent success rate
Agentic Proving for Program Verification
-
ASP encoding computes exact winning probabilities in stochastic games
An ASP-based approach to Solving General Stochastic Two-Player Games
-
Rocq proves liveness for multiparty session types
Formally Verified Liveness with Multiparty Session Types in Rocq
-
Modal logic still triggers Arrow impossibility on cyclic frames
Arrow-Type Impossibility for Genuinely Modal Judgments
-
Noninterference of masked algorithms verified via conditional independence
Formal Verification of Probing Security via Conditional Independence
-
AI agent produces verified distributed systems on all 7 tests
Inductive Deductive Synthesis: Enabling AI to Generate Formally Verified Systems
-
Unrolling recursive definitions is complete for datatype theories
Complete first-order reasoning for functional programs
-
Mediative connective extends fuzzy logic soundly to quantum level
Mediative Fuzzy Logic: From Type-1 Foundations to Type-2, Type-3 and Quantum Extensions
-
Parametric modules make answer set programs declarative
Parametric Modular Answer Set Programs Made Declarative
-
Rewriting equivalents at test time stabilizes LLM theorem proving
What are the Right Symmetries for Formal Theorem Proving?
-
Attention mask forces transformer backtracking to ignore search history
Can Transformers Learn to Verify During Backtracking Search?
-
7B model beats larger ones at Lean proof optimization
ImProver 2: Iteratively Self-Improving LMs for Neurosymbolic Proof Optimization
-
Rado graph has the finite length property
The Finite Length Property of the Rado Graph and Friends
-
Tool verifies probabilistic logic in stochastic systems 10-1000x faster
SENTIL: A Runtime Verification Tool for Probabilistic Temporal Logic
-
Contract method verifies all SRA configurations at once
Verification of Configurable SRA Systems
-
Two-watched literal scheme lifted to first-order logic
A Two-Watched Literal Scheme for First-Order Logic
-
Inductive logic turns neural circuit findings into transferable theories
From Circuit Evidence to Mechanistic Theory: An Inductive Logic Approach
-
Separation logic axioms derived with locality built in
Systematic Design of Separation Logics
-
New tool reduces 62-step proof to 20 rewrite steps
Tao's Equational Proof Challenge Accepted (Technical Report)
-
Supermartingales certify almost-sure ω-regular properties
Complete $\omega$-Regular Supermartingale Certificates
-
Complexity results proven for entailment in cumulative dependence logics
On the Complexity of Entailment for Cumulative Propositional Dependence Logics
-
Vector-clock monitor matches causal-guard semantics locally
Causal Past Logic for Runtime Verification of Distributed LLM Agent Workflows
-
Verifier rewards train neural translator to 86% LTL satisfiability
NeuroNL2LTL: A Neurosymbolic Framework for Natural Language Translation of Linear Temporal Logic
-
Proofs verified by checking natural language modules separately
Pseudo-Formalization for Automatic Proof Verification
-
NFA intersections built with O(mn) transitions
Intersecting Dense Automata
-
ASP Automates Long-Term Power Grid Planning
Long-term Power Grid Planning via Answer Set Programming
-
AI verifies local lemmas for Grasshopper problem but leaves global count unresolved
Using Aristotle API for AI-Assisted Theorem Proving in Lean 4: A Formalisation Case Study of the Grasshopper Problem
-
Protocol wraps agent outputs in four-type verifiable attestations
Pramana: A Protocol-Layer Treatment of Claim Verification in Autonomous Agent Networks
-
Single trajectory yields neural k-inductive barriers for unknown dynamics
k-Inductive Neural Barrier Certificates for Unknown Nonlinear Dynamics
-
Extended unification automates proofs with logical equality
Automating proof search when equality is a logical connective
-
Knowing-how satisfiability is NP-complete
Satisfiability for Knowing How over Linear Plans is NP-complete
-
Refined superposition finds programs if computable ones exist
Completeness of Synthesis under Realizability Assumptions using Superposition
-
Boundary contracts detect hidden timing failures in sound events
Executable Boundary Contracts for Sound Event Traces
-
New acceleration handles array loops via inductive lvalues
Accelerating Loops with Arrays
-
Adjoint modalities mix structural rules in ordered logic
Ordered Adjoint Logic (Extended Version)
-
Shrinking factors enable super-linear NRD bounds for CSP predicates
Super-linear Lower Bounds for CSP Non-Redundancy via Shrinking Instances
-
Unified calculus and lattice language reduce CS problems to performance evaluation
On Generalized Performance Evaluation and Generalized Controller Synthesis
-
Wires become substitutions in ownership-restricted pi-calculus
Wiring the Pi-calculus to Denotational Semantics
-
Closed languages model unifies Kleene algebras with hypotheses
Continuous Algebras with Hypotheses
-
Process algebra resolves probabilistic choices before others
Probabilistic imperative process algebra
-
Algorithms defined as graphs with edges labelled by partial maps
Mathematical Informatics: Algorithms
-
De Simone laws over Kleisli categories ensure trace-equivalence compositionality
Compositionality in Coalgebraic Trace Semantics
-
Deciding reparameterization for MSO formulas on countable chains
Decidability of MSO Reparameterization over Countable Chains
-
Decidability of MSO reparameterization on countable chains
Decidability of MSO Reparameterization over Countable Chains
-
Hypersequent framework unifies modal logic proof systems
A Proof-Theoretic Study of Modal Logic
-
DHNs capture unary negation fragment and counting extensions
Expressive Power of Deep Homomorphism Networks over Relational Databases
-
Compiler enforces AI rules in constant time with formal proofs
Ethical Hyper-Velocity (EHV): A Hardware-Rooted Zero-Trust Runtime Enforcement Architecture for Agentic AI Systems
-
Retrieval system compresses Lean proofs over 70 percent
Lean Refactor: Multi-Objective Controllable Proof Optimization via Agentic Strategy Search
-
A framework generates neural network verification instances with known ground-truth…
Stress-Testing Neural Network Verifiers with Provably Robust Instances
-
GRASS merges graded and substructural logics for flexible resource control
A unification of graded and substructural logics