61 papers
This paper introduces a categorical notion of "explanation" between probabilistic models using spans, demonstrating that every locally-finite probabilistic theory admits a canonical, sharp classical representation through a functorial construction.
NL2GDS is a novel framework that leverages large language models to automatically translate natural language hardware specifications into synthesizable RTL and complete GDSII layouts via the OpenLane flow, achieving significant improvements in area, delay, and power efficiency while democratizing ASIC design.
This paper introduces a novel approach for solving complex string equations by extending Nielsen transformations through the integration of a string power operator, generalized Parikh images, and equality decomposition.
This paper introduces and iteratively refines a constraint learning approach for the classical first-order connection calculus that significantly reduces backtracking in non-confluent proof search while preserving completeness.
This paper investigates the preservation of Kripke completeness and decidability in the independent fusion of one-variable first-order modal logics, demonstrating that these properties hold without equality under both expanding and constant domain semantics but fail when equality and non-rigid constants are introduced due to the encoding of Diophantine equations, while also establishing that the finite model property is preserved only in the local case.
This paper proposes MPBMC, a hybrid approach that leverages Graph Neural Network embeddings and runtime design statistics to functionally cluster properties, thereby significantly accelerating multi-property Bounded Model Checking verification on HWMCC benchmarks compared to state-of-the-art methods.
This paper introduces the constructive master-modality logics and , proving their EXPTIME-completeness and exponential-size finite model property via translations to , while resolving a conjecture regarding their diamond-free fragment and demonstrating the EXPTIME membership of and through embeddings.
This paper surveys systematic approaches to basis-restricted fragments of propositional and modal logics, leveraging Post's lattice and generalized frameworks to analyze how expressive power and computational complexity depend on allowed operators, while also extending results on learnability and identifying open problems.
This paper presents complete diagrammatic axiomatisations for Kullback-Leibler and Rényi divergences by characterizing them as quantitative enrichments of stochastic matrix categories under both Kronecker product and direct sum monoidal structures within a graphical string diagram framework.
This paper establishes a machine-checked impossibility result proving that direct compositional measures cannot terminate step-duplicating recursors, while demonstrating that projection-based methods successfully escape this barrier and providing a complete certified termination chain for a minimal witness calculus.
This paper introduces Strat2Rocq, a framework that extracts and formalizes proof strategies from large language models as lemmas to augment symbolic provers like CoqHammer, significantly improving their automated theorem proving success rates while also benefiting LLM-based proof agents.
This paper introduces a novel equational theory for the I-calculus based on "Ohana trees" that track hidden or infinite variables, establishes a commutation theorem between these trees and Taylor expansions, and provides a corresponding non-idempotent relational denotational model to capture this refined notion of equality.
This paper introduces SCORE, a reversible programming language that utilizes a proof-assisted state space to ensure all stack manipulation operations are interpreted as total bijective functions, thereby overcoming the limitations of traditional partial bijection approaches and enabling the study of computational complexity in fully reversible models.
This paper establishes that in pure polymorphic dependent type theory (P2), parametric quotient types and strong coinduction principles are not definable, and that function extensionality is strictly necessary to prove induction principles, by constructing specific models where these principles fail.
This paper introduces Continuous Modal Logical Neural Networks (CMLNNs), a framework called Fluid Logic that lifts modal reasoning from discrete structures to continuous manifolds using Neural Stochastic Differential Equations to embed logical constraints directly into neural network training, thereby enabling structurally consistent solutions for epistemic, temporal, and deontic reasoning tasks without requiring explicit governing equations.
SpotIt+ is an open-source tool that evaluates Text-to-SQL systems by actively generating database counterexamples to verify query equivalence, utilizing a novel constraint-mining pipeline to ensure these differentiating instances reflect practically relevant discrepancies missed by standard testing.
This paper proposes a Brouwerian assertibility constraint for responsible AI in high-stakes domains that replaces probabilistic confidence with a three-status interface (Asserted, Denied, Undetermined), requiring systems to provide publicly inspectable certificates of entitlement before making claims to preserve democratic epistemic agency.
This paper presents a scalable, modular methodology for the formal verification of floating-point arithmetic that employs direct RTL-to-RTL model checking, counterexample-guided refinement, and AI-assisted property generation to overcome the limitations of high-level abstraction and achieve higher coverage efficiency.
The paper introduces SpotIt, a novel evaluation pipeline that employs formal bounded equivalence verification to actively search for database instances distinguishing generated SQL queries from ground-truths, thereby addressing the limitations of optimistic test-based methods and revealing hidden discrepancies in current Text-to-SQL performance assessments.
This paper proposes a novel geometric framework that models LLM reasoning as smooth flows in representation space, demonstrating through empirical experiments that next-token prediction enables models to internalize logical invariants as higher-order geometry, thereby challenging the "stochastic parrot" hypothesis and suggesting a universal representational law underlying machine understanding.