61 papers
This paper introduces Preguss, a modular framework that combines static analysis with LLM-aided synthesis to automatically generate and refine interprocedural specifications, enabling highly automated verification of large-scale programs (over 1,000 lines of code) while significantly reducing human effort.
This paper introduces a general framework that extends Knowledge Compilation to Satisfiability Modulo Theories (SMT) by combining input formulas with pre-computed theory lemmas to enable polytime propositional-style querying of compiled SMT d-DNNFs.
This paper explicitly establishes that the optimum circuit size changes by at most under truth table perturbations, extending the bound to general Hamming distances and verifying its tightness at through exhaustive SAT-based analysis.
This paper introduces an operad of dependent directed wiring diagrams to enable the composition of instantaneous systems like Mealy machines and parameterized stock-and-flow diagrams, providing a formal algebraic framework and a semantic morphism that maps these diagrams into Mealy machines.
This paper investigates how key properties of probability monads, including their Kleisli laws, monoidal structures, and affinity, arise from their codensity presentations, establishing new universal properties for these monads and characterizing their tensor products via Day convolution while highlighting the limitations of the Giry monad on standard Borel spaces.
This paper introduces RoadLogic, an open-source framework that bridges declarative OpenSCENARIO specifications and executable simulations by combining Answer Set Programming, motion planning, and specification-based monitoring to automatically generate diverse, realistic, and compliant autonomous vehicle testing scenarios.
This paper presents a scalable formal verification methodology for Quantum Phase Estimation circuits that utilizes symbolic qubit abstraction based on quantifier-free bit-vector logic to efficiently verify circuits with over 1,000 qubits while maintaining low memory usage.
This paper proposes the concepts of step automata and step Turing machines (STM) as a natural extension of traditional automata and Turing machines to bridge the gap between classical computation and concurrency by enabling the execution of atomic action steps without partial orders.
This paper establishes that the size difference between optimal Boolean circuits and formulas over the AIG basis is strictly limited to 0 or 1, characterizing the precise conditions under which sharing occurs and proving that any non-zero gap arises exclusively from a single gate with fan-out 2.
The paper introduces Apply2Isar, a tool that automatically converts procedural apply-style proofs in Isabelle/HOL into readable and robust declarative Isar proofs, demonstrating its effectiveness through evaluation on a large benchmark set from the Isabelle Archive of Formal Proofs.
This paper presents a computational method for automatically generating mathematical proof exercises with comparable complexity levels by utilizing cut-based tableau proofs and a mechanizable rule extraction procedure to control difficulty for undergraduate discrete mathematics education.
This paper introduces sketch-oriented databases, a categorical framework that unifies various graph-based paradigms and features through finite-limit sketches, while proposing localizers for lazy path inference and stuttering sketches to enable modular composition and scalable model growth.
This paper proposes using graph neural networks to predict initial branching orders for CDCL SAT solvers, demonstrating significant speedups on random and pseudo-industrial benchmarks while noting that the approach struggles with complex industrial instances due to the solver's dynamic heuristics overriding the predictions.
This paper presents LLM2SMT, a case study demonstrating that an LLM coding agent can autonomously build a complete, competitive DPLL(T)-style SMT solver for QF_UF—including the Nieuwenhuis-Oliveras congruence closure algorithm and Lean proof emission—without any human-written code.
This paper introduces Twitch, a tool that automatically discovers reusable term abstractions from failed or successful proofs to enhance the performance of the Twee equational theorem prover, resulting in the solution of new problems and significant speed-ups on existing benchmarks.
This paper presents "Agent Hunt," a decentralized autoformalization system for algebraic topology that utilizes a simulated bounty-based marketplace to coordinate multiple LLM agents in dynamically proposing, competing to prove, and iteratively refining formal statements within an Interactive Theorem Proving environment.
This paper proposes a novel approach to mining data-aware temporal specifications from execution traces by combining Syntax Guided Synthesis with a finite-prefix interpretation of Temporal Stream Logic (TSL), enabling the robust and sample-efficient synthesis of reactive programs that capture both data transformations and temporal behaviors.
This paper formalizes the Galois correspondence between covering spaces and subgroups of fundamental groups within homotopy type theory, extends the concept to n-dimensional generalizations, and applies the framework to classify lens space coverings and construct the Poincaré homology sphere.
This paper introduces dilated seminorm-enriched category theory as a unifying framework for central limit theorems, establishing an abstract CLT that recovers classical results and yields novel applications in symplectic manifolds and statistical mechanics.
This paper compares three fixed-dimension satisfiability semantics for quantum logic—standard Hilbert-lattice, global commuting-projector, and local partial-Boolean—proving a strict hierarchy where the standard semantics is strictly more expressive than the others, as demonstrated by an explicit formula that is satisfiable in the standard semantics but unsatisfiable under the other two for all dimensions .