archive
Every paper Pith has read. Search by title, abstract, or pith.
341 papers in cs.LO · page 1
-
Lean tactic solves 19% more ZKP benchmarks than SMT solvers
Automating Bitvector and Finite Field Equivalence Proofs in Lean
-
Guises encode relations as internal perspectives
Guises and Perspectives: An Intentional and Hyperintensional Sketch
-
Parameterized program safety reduces to local proofs
Complete Local Reasoning About Parameterized Programs Over Topologies
-
Higher sheaf models of type theory built constructively
Constructive higher sheaf models with applications to synthetic mathematics
-
One-var loop termination decided in poly time under Collatz conjecture
Loop Termination and Generalized Collatz Sequences
-
The paper shows that adding a reversal operation to self-dual cubical type theories is a…
Eliminating reversals from cubical type theories
-
Viverra adds verified assertions to LLM-generated C code
Viverra: Text-to-Code with Guarantees
-
Transducers extend stabilization for faster relational string solving
String Solving with Stabilization and Transducers (Technical Report)
-
Nested reset counters hit exact F_Ωk levels
The Complexity of Nested Reset Counter Systems
-
CSLib benchmark finds structure reranking beats BM25 modestly
CSLibPremiseBench: Structure-Guided Premise Retrieval and Label Robustness for Lean 4 Computer-Science Theorems
-
Proof nets canonically represent PiL sequent derivations
Proof Nets for PiL (Full Version)
-
Sampling and model-checking oracles learn regular POMDP policies
Synthesizing POMDP Policies: Sampling Meets Model-checking via Learning
-
Diagrams encode all commutative algebras and varieties
Graphical Algebraic Geometry: From Ideals and Varieties to Quantum Calculi
-
New logic QLL turns constraints into neural losses that match verifiers
Quantitative Linear Logic for Neuro-Symbolic Learning and Verification
-
Quantitative linear logic aligns neural training with formal verification
Quantitative Linear Logic for Neuro-Symbolic Learning and Verification
-
Hoare logic equivalent to second-order logic with first-order predicates
A foundational characterization of Hoare Logic
-
LLMs reach only 52% accuracy on HMSC semantic tasks
(How) Do Large Language Models Understand High-Level Message Sequence Charts?
-
LLMs reach only 52% accuracy on HMSC formal semantics
(How) Do Large Language Models Understand High-Level Message Sequence Charts?
-
Amaryllis adds dynamic allocation to probabilistic logics
First Steps Towards Probabilistic Iris: Harmonizing Independence, Conditioning, and Dynamic Heap Allocation
-
Shared graph reuses subformula results for many properties
Multi-Property Temporal Logic Monitoring
-
Subsumption in FL_bot_reg with TBoxes is ExpTime-complete
Subsumption in $\mathcal{FL}_{\bot \mathit{reg}}$ with TBoxes Is in ExpTime
-
Canonical distributive laws arise for operadic and commutative monads
Monads and Distributive Laws in Substructural Contexts (Extended Version)
-
Logic proves exact samplers for Gaussian and Laplace correct
Verifying Exact Samplers for Continuous Distributions with a Discrete Program Logic
-
ELbotpreceq extends DL-Lite with reachability in NL
A Horn extension of DL-Lite with NL data complexity
-
Real-valued provability in linear logic converges to MALL at infinite hardness
Quantitative Linear Logic
-
Calculus measures linear logic proofs with real numbers
Quantitative Linear Logic
-
LLM states project to F2 for 93% zero-shot ontology accuracy
Controlling Logical Collapse in LLMs via Algebraic Ontology Projection over F2
-
Flattening lets QuAK analyze nested quantitative automata
Extending QuAK with Nested Quantitative Automata
-
Syntactic obligations translate to MTBDD automata for fast synthesis
Fast Obligation Translation and Synthesis
-
Sound rewards let POMDPs meet LTL specs despite fog
Ensuring Logic in the Fog: Sound POMDP Synthesis with LTL Objectives
-
Tool synthesizes reactive systems over infinite integers
sweap: Reactive Synthesis for Infinite-State Integer Problems
-
Alternative algorithm computes conditional MDP reachability without cyclic hardness
Fast Computation of Conditional Probabilities in MDPs and Markov Chain Families
-
New method computes conditional probabilities in MDPs faster
Fast Computation of Conditional Probabilities in MDPs and Markov Chain Families
-
FO2 groundings can force exponential DNNF size
On Knowledge Compilation For Two-Variable First-Order Logic
-
Optimal LTLf synthesis realizes maximal objectives from conflicting goals
Optimal LTLf Synthesis
-
Adaptive teacher exposure lifts LLM reasoning self-distillation
Adaptive Teacher Exposure for Self-Distillation in LLM Reasoning
-
Streaming transducers admit minimal models
Minimization of Streaming Transducers
-
General criteria guarantee minimal models for streaming transducers
Minimization of Streaming Transducers
-
Shields enforce probabilistic safety bounds in MDPs
Shields to Guarantee Probabilistic Safety in MDPs
-
Probabilistic shields cannot keep both strong safety and full permissiveness
Shields to Guarantee Probabilistic Safety in MDPs
-
FOMOD logic testable in constant time on finitary graphs
Constant time testability of first-order logic with modulo counting on finitary graphs
-
Preservation theorems hold for all lattice semirings
Preservation Theorems in Semiring Semantics
-
This paper shows that reachability in RDMA programs is undecidable even in restricted…
On the Verification Problem of Remote Direct Memory Access programs (Extended Version with Appendix)
-
Neuro-symbolic system turns G-code collisions into bounding-box fixes
Correct-by-Construction G-Code Generation: A Neuro-Symbolic Approach via Separation Logic
-
Neuro-symbolic loop fixes G-code via spatial proof failures
Correct-by-Construction G-Code Generation: A Neuro-Symbolic Approach via Separation Logic
-
Coherency yields equivalent yet preferred FRETish-to-MTL translation
Coherency through formalisations of Structured Natural Language, A case study on FRETish
-
Separation logic catches CNC collisions as spatial data races
Separation Logic for Verifying Physical Collisions of CNC Programs
-
Mean MPNNs verify polynomial counting on labelled graphs
The Polynomial Counting Capabilities of Message Passing Neural Networks
-
Refinement calculus certifies index reductions for DAEs
A Deductive Refinement Calculus for Differential-Algebraic Programs
-
Every prevision is the infimum of sublinear previsions
Just Previsions