Papers

What is "structure," and how can we exploit it in combinatorial optimization? Reasoning tasks such as system design, state estimation, and prediction can be cast as combinatorial optimization problems (COPs), traditionally attacked by dedicated algorithms that fail outside their narrow subclass, while communities working on equivalent problems reinvent each other's techniques. The weighted constraint satisfaction problem (WCSP) is a general framework that subsumes COPs from many communities and represents complex physical and non-physical systems, from spin glasses to social networks. Is such generality a curse? Our answer is to exploit "structure": a general-purpose WCSP algorithm should automatically imitate the specialized algorithm for whatever subclass its input belongs to. A WCSP has macro (graphical) structure, which variables interact, and micro (numerical) structure, how they interact. Separate schools of thought exploit one or the other, never both. The constraint composite graph (CCG), introduced in 2008, unifies them: it is an undirected graph over a WCSP instance's variables plus auxiliary ones, on which minimum weighted vertex cover (MWVC) solves the original instance. It is efficiently constructible, but largely unexploited. This dissertation answers three questions affirmatively. The CCG has theoretical advantages beyond identifying tractable classes (new properties proved here); it is practically useful (efficient implementation and experiments); and it extends promisingly to non-Boolean variables (new encodings). We use the CCG to (a) kernelize a WCSP instance, fixing optimal values of some variables by maxflow before search begins, (b) improve min-sum message passing, (c) exploit integer linear programming solvers, and (d) solve COPs on quantum annealers. Solving general COPs faster classically also yields better baselines for the debated quantum advantage.

We present a mathematically rigorous, systematic approach for the verification of database isolation guarantees, which (i) supports a spectrum of seven isolation levels, (ii) uncovers a fundamental dichotomy among isolation levels: stronger levels can be verified via refinement alone, whereas weaker levels additionally require reduction, and (iii) provides a hierarchy of abstract models that substantially simplifies proofs by factoring out their most labor-intensive parts. In particular, we eliminate the need for per-protocol reduction proofs for the weaker class of isolation levels by performing a once-and-for-all reduction at a high level of abstraction in our hierarchy. To achieve this, we develop and apply a generic theory of reduction, which is also of more general interest. Overall, our approach minimizes the user's proof effort to a single, simpler refinement of the most concrete model in our hierarchy. All our results are formalized in Isabelle/HOL.

We present a Lean 4 formalization of the Laplace transform for complex-valued functions, its fundamental operational rules, and a Bromwich-type inversion theorem proved through real-variable integration and the Dirichlet integral. As an application, we formalize the Laplace-domain solution of the harmonic oscillator and identify its transform with that of $\sin(\omega t)$. We also discuss the principal analytic and formalization challenges encountered in the development.

We formalize the Dirichlet integral and several of its classical applications in the Lean~4 proof assistant. Since the sinc function is not Lebesgue integrable on the positive half-line, the Dirichlet integral must be represented as the limit of integrals over bounded intervals. To avoid the difficulty of removing an exponential factor from a conditionally convergent integral, we instead pass through the absolutely integrable function \(\operatorname{sinc}^2\). We evaluate its integral by differentiation under the integral sign and dominated convergence, and then recover the Dirichlet integral from an identity between truncated integrals. Using these results, we formalize the convergence of the Dirichlet cutoff to the Heaviside function and derive several quadratic and bilinear trigonometric integral identities. Finally, we formalize Lobachevsky's integral formula for continuous periodic functions satisfying a reflection symmetry, using the density of cosine polynomials obtained from Mathlib's Fourier analysis on the additive circle.

Kolokolnikov conjectured that, among all simple graphs on \(n\) vertices with exactly \(2(n-2)\) edges, the complete bipartite graph maximizes algebraic connectivity. This paper proves the conjecture. The underlying Lean~4 formalization was generated with MerLean and checked by the Lean kernel.

Data centers are among the power grid's fastest-growing loads. Since data center servers are sensitive electronic components, they need to be protected against the grid's voltage disturbances during grid faults. While disconnecting from the grid achieves this, it can further destabilize the power system if many data centers trip at once. To address this emerging concern, voltage ride-through (VRT) grid codes have been proposed to standardize data center behavior. They require a data center to stay connected for a period of time through the disturbance, hold an active power floor, and recover its draw within a deadline upon restoration. However, systematically designing and certifying controllers that satisfy these coupled temporal and operational requirements remains challenging. We propose SolVRT, a system that synthesizes a grid-code-compliant VRT controller for a given data center using formal methods. We develop a specification language that expresses a grid code in Signal Temporal Logic (STL) as the basis for formal reasoning. Our encoding algorithm takes the specification, along with a model of the data center's power topology, and translates the constraints into a controller synthesis problem. This step produces a correct-by-construction controller if a solution can be found, or a proof that no such controller exists. For the latter case, SolVRT provides a diagnostic step: it traces the facility's "conflict frontier," isolates the conflicting clauses that led to non-compliance, and computes the smallest hardware or workload change that would enable compliance. We evaluate SolVRT through closed-loop simulations of a 200 MW data center connected to a 140-bus transmission system. The results demonstrate that SolVRT can synthesize compliant VRT controllers, certify infeasibility when compliance is unattainable, and identify targeted modifications that enable compliance.

We present a new proof of the embedding of the classical modal logic S4 into the logic of Boolean Bunched Implications (BBI). While the original proof is semantical, this proof is entirely syntactical. It proceeds via Hilbert-style calculi, and is built by analogy with a recently discovered proof by Godel of the embedding of intuitionistic propositional logic into S4. We present the first full proofs of deduction theorems for BBI, which are used to show that the embedding is preserved by reasoning with assumptions, including where those assumptions are organised into bunches. Unlike the existing proof, our proof is stable under arbitrary axiomatic extensions of S4, and applies to all known axiomatic extensions of BBI in the literature. We observe how this embedding is related to semantical properties of both logics. Moreover, the proof extends gracefully to language extensions of BBI, as we show with hybrid BBI, classical BI, and sub-classical BBI.

Constrained specification mining enables the automatic discovery of desired properties from system traces. Generalized Reactivity of Rank 1, or GR(1), is a fragment of LTL with polynomial-time synthesis that natively encodes assume-guarantee properties present in most hardware and robotics domains. In this paper, we present GR1MINE, a SAT-based tool for efficiently learning GR(1) formulas from examples. We exploit the GR(1) temporal skeleton to incrementally enumerate formula candidates, leveraging learnt clauses to avoid recomputation. On the Boolean GR(1) Syntech suite, GR1MINE learns a realizable formula for all 60 benchmarks over 30X faster than generic and constrained LTL mining tools. On non-GR(1) specifications from SYNTCOMP, GR1MINE is still able to recover >2X more realizable specifications than baselines within the timeout.

The red-blue pebble game is a well known two-player game on graphs that has been used in the past as a tool to analyze complexity measures in several computation models as well as proof systems. We define a new way to measure the cost of the game, the blue cost, which only counts the number of pebbles that are colored blue during the game. This new measure characterizes exactly several space bounds in tree-like and negative Resolution. In particular we prove that for any unsatiafiable formula $F$, the clause space requirements of the formula in tree-like Resolution, exactly coincide with the minimum blue pebbling cost of the game played on a refutation graph of $F$ (not necessarily a tree). This exactly parallels the known result for general Resolution in terms of the standard black pebble game, and improves the existing approximated characterization of tree-like space in terms of reversible pebbling. We show that the blue pebbling cost is also well suited for analyzing the space requirements of the lifted pebbling formulas $Peb_G[\vee]$ and $Peb_G[\oplus]$ in the two Resolution restrictions. In the case of tree-like Resolution, the clause space of $Peb_G[\vee]$ asymptotically coincides with the blue cost of the underlying graph $G$. For the case of negative Resolution, we obtain almost matching upper and lower bounds for the space in the two classes of lifted formulas, similar to the ones existing for general Resolution. We also prove a close to optimal space separation between tree-like and negative Resolution, presenting a class of formulas with $n$ variables that require clause space $\Omega(\frac{n}{\log n})$ in negative Resolution, but have constant space tree-like refutations. This contrasts with the fact that negative Resolution can simulate tree-like Resolution with only a small increase in size.

We present a method for partitioning the solution space of statements in extremal set theory. Compared with domain-agnostic partitioning methods like look-ahead, we perform case analysis on the strategies by which a candidate solution can be constructed. We demonstrate that our approach can decompose problems in extremal set theory more effectively than look-ahead. Combining this new partitioning strategy with an exact proof-producing MILP solver, we are able to verify larger finite cases of Chvátal's Conjecture—a long-standing open question in extremal combinatorics—compared to previous work.

We present HOPSCOTCH, a Lean 4 framework for mechanizing computationally sound, game-based cryptographic proofs. Security definitions are expressed as indistinguishability between stateful probabilistic oracles, and proofs follow the standard game-hopping paradigm. HOPSCOTCH uses a shallow embedding: oracles and reductions are ordinary Lean definitions, enabling direct integration with the full Lean ecosystem, including general mathematical theories from Mathlib, such as finite-group theory. A game-hopping proof in HOPSCOTCH is represented as an explicit formal object whose constructors correspond to the standard steps of a game-hopping argument, making proofs easier to construct, automate, and inspect. We prove a general computational soundness theorem that interprets these proof objects by constructing reductions against the assumptions they use and deriving a concrete bound on the advantage of any distinguisher. Observational equivalence between oracles is established using a state-abstraction methodology: a simple yet powerful approach that supports transformations such as adding or forgetting state and replacing eager sampling with lazy sampling. We illustrate the framework with formalized proofs of the IND-CCA security of encrypt-then-MAC, the security of ElGamal encryption from DDH, the implication from one-time secrecy to public-key IND-CPA security, and the GGM pseudorandom-function construction. To the best of our knowledge, the last is the first mechanized proof of GGM for non-constant depth.

Motivated by the need to reason about case statements quantitatively, we extend quantalic linear lambda-calculus with additive disjunction. We show that the resulting equational system is sound. We also show that when certain continuity properties (of the underlying quantale) are adopted, it is additionally (approximately) complete. We present several models of the extended calculus, involving for example meta-theoretical properties in categorical logic (gluing), probabilistic, and quantum computation. As a concrete application, we illustrate how a probabilistic model, based on Banach spaces, can be synergistically used with the calculus' equational system to reason about Cauchy sequences of random walks. This highlights the emergent shift from "program semantics as the science of program equivalence" to flexible, quantitative perspectives, involving functional analysis and beyond.

RTLola is a stream-based specification language designed for asynchronous real-time systems. While many temporal specifications naturally refer to future behavior, RTLola currently offers no mechanism to express such future-dependent properties. In this paper, we extend RTLola with two complementary mechanisms to reason about the future. First, we introduce a prediction operator that extrapolates future stream values at arbitrary timestamps based on past observations. Second, we add a discrete future offset operator, which provides access to precise future values by delaying the evaluation of the dependent stream expressions. While the former enables immediate, but possibly imprecise predictions, the latter ensures exact values once the required information becomes available. We formalize both extensions in the RTLola semantics and evaluate their implementation on runtime and memory consumption.

Stream-based monitoring enables the concise specification of complex temporal properties. However, existing stream-based monitors are limited when dealing with large external data sources, a task that is better handled by specialized data management systems. We address these limitations by extending stream-based monitors with the ability to query external data sources. We implement this approach in RTLola and investigate challenges such as handling delayed responses, type checking of returned data, and runtime error management. A unified interface enables the seamless integration of existing systems into our approach, such as static databases or dynamic endpoints, e.g. a weather API. Our evaluation using specifications from the aviation domain also shows that a custom geospatial backend based on k-d trees outperforms state-of-the-art database systems.

Prime implicants (PIs) are central in computer science, with applications in logic minimization, diagnosis, explainable formal methods and AI. Algorithms for the computation of PIs were first-and-foremost considered on the full input space, not considering the case where the input space might be constrained by context or structural dependencies. To filter out those PIs that do not fulfill the constraints, existing methods rely on an explicit post-processing step after computing all PIs, which leads to scalability issues due to the number of PIs being exponential. We propose end-to-end symbolic algorithms that implicitly represent the set of PIs under side constraints. For this, we extend the prominent method based on decision diagrams by Coudert and Madre and implement a modular tool chain that separates decision-diagram construction, PI computation, and filtering.

While most research on quantum programming considers an idealized, noise-free semantics for quantum programs, we reason about quantum programs that are executed on real, noisy hardware. We consider the error models published by quantum hardware vendors to give a hardware-dependent semantics to quantum programs. This work presents a comprehensive study of noise-aware quantum programming, ranging from logical foundations to automated verification and synthesis. We develop a noise-aware quantum Hoare logic, and use it to derive algorithmic methods for the bounded verification of quantum programs on specific hardware, and for the automatic synthesis of noise-optimal loop-free quantum programs. In this way, we synthesize hardware-dependent subroutines that commonly occur in quantum algorithms, such as parity checks, quantum state preparation, and quantum state discrimination. We evaluate our method on the hardware specifications provided by the IBM Qiskit toolkit. Besides finding different optimal subroutines for different noise models, our synthesis tool also shows that classical probabilistic branching is needed for optimality in quantum programming.

Fitting's finite Heyting-valued modal logic interprets modal formulas over a finite Heyting algebra. We use a relational bitopological representation to obtain a finite-state reduction. For a finite model and a finite vocabulary, the modal subalgebra generated by the atomic valuations determines a state-evaluation map. We prove that the observational quotient is isomorphic to its finite image in the bitopological dual and that the quotient relation is the restriction of the canonical dual relation. Hence every formula over the vocabulary preserves its exact truth value, and the quotient is minimal among surjective reductions through which all generated observations factor. In addition, for any formula and state, we construct a finite tree-like exact-value certificate whose depth is bounded by modal depth and whose branching depends only on the height of the truth-value algebra and the number of boxed subformulas. Failed formulas therefore admit bounded reduced counterexamples preserving their precise failure values.

Dataflow architectures have gained renewed interest due to their balance between power efficiency and performance. In (spatial) dataflow architectures, a program is represented as a set of entirely distributed and dynamically scheduled dataflow operators that communicate through asynchronous channels, which greatly improves data locality and parallelism. However, compiling to dataflow architectures remains an error-prone process, in order to maintain determinacy while enabling pipelining. Determinacy means that the result of a dataflow program is deterministic and independent of the schedule of operator execution, and pipelining is an important optimization in spatial dataflow that enables parallelism across loop iterations. In this work, we present Wavelet, the first effort to formally verify a compiler for asynchronous dataflow. We use a mix of techniques to achieve this goal. Our frontend uses a novel capability type system with fences to synchronize conflicting memory accesses and enable pipelining. We then verify a Lean formalization of two core passes of our compiler that translates elaborated programs from the type checker to dataflow graphs, proving important properties of forward simulation and determinacy. Notably, our formalization semantically propagates the soundness guarantees of the frontend type system, ensuring modularity between simulation and determinacy proofs. In evaluation, we show that dataflow graphs compiled by Wavelet have comparable sizes to those produced by an unverified optimizing compiler for the RipTide spatial dataflow architecture.

Sequential prediction naturally induces an innovation sequence consisting of the prediction errors produced by a causal predictor. We use the collection of all such innovation sequences to define the innovation spectrum of an individual binary sequence and, from it, a new reducibility based on sequential information extraction. We show that this reducibility refines truth-table reducibility while exhibiting a fundamentally different geometry. The degree structure decomposes into two canonical regions: a truth-table spine, whose induced order is isomorphic to the truth-table degrees, and a complementary reservoir-immune region, consisting of sequences from which no infinite computable predictable reservoir can be extracted. We establish bridge constructions connecting the two regions, prove that reservoir immunity is preserved under sequential innovation, and show that the Martin–Löf-random degrees form a proper downward-closed substructure inside the reservoir-immune region. These results reveal a new geometric organization of individual sequences based on causal predictability rather than classical oracle computation.

Large language models (LLMs) can generate text that resembles a mathematical proof, but resemblance does not establish correctness. A formal proof checker verifies whether each proof step follows established logical rules. Coq bases its rules on the Calculus of Inductive Constructions, a logical framework that defines which proof steps the system may accept. This pilot study evaluated six open-weight LLMs on the same 100 theorems from CoqStoq, a benchmark derived from real Coq projects. Each LLM received one attempt per theorem with the temperature set to 0, and Coq checked every proposed proof in the theorem's original project environment. We counted a proof as successful only if the Coq kernel accepted it. Gemma 4 verified 12 of 100 theorems, Llama 3.3 verified 8, and DeepSeek Coder V2 Lite verified 1. Qwen 3.5, Mistral Small 3.1, and GPT-OSS verified none. The 21 successful model-theorem results covered 15 distinct theorems, 11 of which were not solved by a baseline of standard Coq tactics. All verified theorems had short or medium human-written reference proofs; no model verified a theorem with a long reference proof. Because the proof-length analysis was exploratory, this pattern does not establish that proof length caused the difference. For the three models with at least one success, the total generation cost per verified proof ranged from 741 to 36,193 output tokens, 14.9 to 178.0 seconds, and 0.0167 to 0.2000 aggregate GPU hours. We could not calculate these ratios for models with no verified proofs. Across 600 attempts, the models produced 21 kernel-verified proofs, giving an overall success rate of 3.5%. The study reports descriptive differences among the models but does not statistically test whether one model outperforms another. Therefore, the results do not establish a universal ranking of the six models.

Deciding satisfiability of Constrained Horn Clauses (CHCs) modulo the theory of fixed-size bit-vectors ($\mathcal{T}_B$) is fundamental to bit-precise program verification. However, state-of-the-art CHC-solvers often struggle with $\mathcal{T}_B$, limiting scalability in bit-precise reasoning. We present Mosaic, a theory-modular framework for deciding satisfiability of CHCs modulo $\mathcal{T}_B$ by combining reasoning in $\mathcal{T}_B$ and the theory of Integer Arithmetic ($\mathcal{T}_I$). Given a CHC set modulo $\mathcal{T}_B$, Mosaic partitions it into two fragments interpreted over $\mathcal{T}_B$ and $\mathcal{T}_I$. Moreover, it implements an algorithm that reasons about the fragments in a modular fashion, exchanges information between them via sound translations across theories, and determines satisfiability w.r.t. the original CHC set. We implemented a prototype of Mosaic using Z3 and Spacer and evaluated it on bit-manipulating benchmarks. Our evaluation shows that Mosaic significantly outperforms Spacer on these benchmarks.

Probabilistic algorithms and data structures are widely used to obtain favourable expected performance guarantees. While their mathematical analysis is often well understood, mechanising expected-cost analyses remains challenging, requiring reasoning about probability distributions, expectations, and recursive stochastic behaviour. Existing formal approaches frequently require substantial manual proof effort, since expected costs are often encoded separately from probabilistic computations and must therefore be propagated explicitly throughout proofs. In this paper, we present a cost-aware probability monad for \LH/ that supports reasoning about probabilistic programs together with their expected costs. Our approach combines executable probabilistic programs with refinement-type-based verification and SMT-supported automation. The monad intrinsically tracks probability mass, expected values, and expected costs through refinement types, enabling many quantitative properties of probabilistic computations to be inferred compositionally from program structure. We evaluate our approach on several classical probabilistic algorithms and data structures, including meldable heaps, randomised quicksort and quickselect, randomised splay trees, random permutations, and the hiring problem. The case studies demonstrate different points along the spectrum between automated and interactive verification.

We ask whether asymptotic recursion depth determines the expressive strength of a bounded recursive algebra, and prove that it does not. We replace ordinary predecessor recursion by generalized-inverse descent along a fixed iterate $g_n^{[l]}$ and obtain classes $H^m_{n,l}$, where $m$ measures initial-function strength, $n$ the growth row, and $l$ the traversal stride. For all rows $n,n'\ge2$ we prove an exact inclusion criterion. At a fixed row $n\ge2$ three regimes occur: below the critical basis ($m<n$), equal-row inclusion is exactly reverse divisibility $l'\mid l$; at $m=n$ every stride collapses to one class; and from $m=n+1$ this class is ordinary bounded recursion $E^m$. Hence pairwise $\Theta$-equivalent descent depths can induce infinite descending chains, infinite antichains, and copies of every finite partial order. The separation is therefore controlled by traversal alignment rather than by growth rate or recursion depth alone. The proof combines exact-depth simulation, trace sparsity, and selected dependency chains. The exceptional doubling row has the same reverse-divisibility order at basis zero, but all strides collapse from basis one onward; from basis three it equals ordinary bounded recursion, while at basis two $H^2_{1,l}\subsetneq FP$. At basis zero the doubling-row classes are proper subclasses of deterministic functional logspace, so the same dual-divisibility order already occurs inside $FL$.

Incremental Linearization has previously been proposed for solving SMT problems over quantifier-free nonlinear integer arithmetic and has proven effective despite its conceptual simplicity. In this paper, we introduce a revised axiom set that improves convergence on polynomial constraints built from higher-degree monomials, such as powers and mixed products, a class of problems on which prior axiomatizations struggled. We present a standalone implementation built on top of Z3 for linear integer arithmetic and evaluate it on the NIA benchmark set from SMT-LIB. Our results show that the approach is competitive with state-of-the-art solvers overall and substantially outperforms them on benchmarks dominated by such polynomial constraints.

Category theory is a mathematical theory of composition, widely used in logic, computing, and physics. Here we apply it to give a theory of secure composition. In particular, we provide a categorical treatment of Canetti's Universal Composability (UC) framework for systems with a static number of parties and sessions, often termed UC for static systems, yielding four benefits. First, we present our results graphically yet retain rigor by applying a standard categorical technique known as string diagrams. In particular, our formulation of the composition theorem can be graphically verified with a short sequence of diagrams, while remaining translatable to equations and amenable to formal verification. Second, categories let us generalize so that our results extend beyond interactive Turing machines to other forms of computation, such as quantum computation or domain-specific languages. Third, categories help us drop some unnecessary restrictions of UC (e.g., our adversary can be a computational network rather than a single Turing machine); we prove equivalence between our variant and the usual UC, showing no expressiveness is lost. Finally, the categorical perspective leads us to identify and correct some minor technical oversights in the standard formulation of simple UC.

As "AI Scientists" emerge to drive research via the Model Context Protocol (MCP), systems relying on ephemeral scripts will fail. The sheer scale of stateful, interconnected evidence requires a machine-walkable warranty grounded in a purpose-built database architecture. Eigenius is an open-source, typed knowledge-graph DBMS built on a single premise: answering the audit question ("what do you know, and what is your warranty?") requires a unified kernel. By tightly coupling the type system, storage engine, and integration protocol, Eigenius turns data provenance into a structural invariant rather than a property reconstructed across subsystem boundaries. The kernel rests on three pillars: a dependent type theory woven through the core, institutions acting as strongly typed integration boundaries, and a content-addressed immutable storage layer. On this foundation, epistemic status (declared/observed/derived/verified) is enforced as a strict commit-time invariant. Cross-system translations (comorphisms) are checked at commit and materialized directly into the graph as durable, first-class resources. To eliminate O(N^2) polystore bottlenecks, shared on-chain intermediate representations (IRs) collapse multi-system translations to identity. Crucially, this architecture unifies both domains of scientific epistemology: it relies on justification logic for empirical science, while embedding a fast, in-process term checker to safely evaluate formal mathematical proofs (via Lean 4) without IPC overhead. In an end-to-end recomputation of a published Nature study from fragile scripts to a materialized evidence graph, all 52 derived conclusions hold from pinned data, surfacing four machine-checked discrepancies in the original study.

Gödel's ontological argument is modal by design. Possibility and necessity are among its central concerns, and connected interpretation decisions – extensions or intensions for the positive properties, constant or varying quantifier domains, the choice of modal logic, etc. – subtly shape the argument and, in particular, whether the modal collapse is implied or not. It is tempting to abstract the modality away and to read the positive properties as merely forming an ultrafilter – which, however, may replace Gödel's argument with a perhaps more manageable alternative that may have little to do with Gödel's original intention. In this spirit, Odifreddi and Gomes argue that modal collapse is an intrinsic structural feature of any theory that characterises positive properties as an ultrafilter and identifies God as its principal generator. This comment shows, with machine-verified counterexamples, that the structural claim is false: what drives the collapse is primarily not the filter structure but the rigidity of positivity – itself a thoroughly modal condition. Moreover, two claims of Odifreddi and Gomes are corrected: one on the derivability of Gödel's Theorem IV, one on the extensionality of positivity. All results are machine-checked in Isabelle/HOL.

Computational paths record the steps of an equality derivation. We give them a topological semantics that distinguishes derivable rewrites from arbitrary homotopies. Coherent representatives pair traces with paths homotopic to their realizations. We compare a topology retaining the entire trace with one observing only endpoints, length, and paths. Quotienting by the declared rewrites gives a groupoid. Multiplication is continuous when composable pairs carry the quotient topology inherited from composable representatives. This topology can differ from the usual subspace topology on pairs of quotient arrows. We characterize when they agree, give compact-Hausdorff and discrete sufficient conditions, and use the Hawaiian earring to exhibit a failure of agreement. The comparison with geometric homotopy classes is injective exactly when the presentation is geometrically complete. Normal-form certificates give a criterion for completeness. In the universal presentation, all paths are primitive steps and all endpoint-fixed homotopies are allowed rewrites; its quotient recovers the quotient-topologized fundamental groupoid. Circle and torus examples recover the classical based-loop classifications by $\mathbb Z$ and $\mathbb Z^2$. A Lean development supports the construction. A focused Lean 4.32.0 result registered in Palomar covers the topology comparison, additive circle and torus classifications, and a conditional Hawaiian-earring obstruction transfer. We distinguish that result from the earlier Lean 4.24.0 development and from the mathematical exposition.

Deploying pre-trained perception models in novel environments degrades their accuracy under distributional shift, and assembling them alone does not recover it: combiners such as majority voting trade recall for precision and are brittle to coordinated failures. Prior metacognitive methods learn logical rules that flag a model's errors, but rely on hand-authored domain-knowledge cues (object-size priors, segmentation masks) that do not transfer to genuinely novel scenes. We show that this metacognitive layer can be learned without any domain knowledge by exploiting vector-space geometry: per-model Label Vector Pools (LVP), built from each model's own training embeddings, yield error-detection rules from the geometry of detections relative to training-determined prototypes, reaching parity with domain-knowledge rules to within $0.002$ every F1 on test set. Because the approach remains neurosymbolic, these geometric rules share a single logical framework and can still be complemented by domain knowledge when available. We frame the fusion of multiple imperfect ViT-based detectors as a consistency-based abduction problem solved at test time by an exact Integer Program (IP) and a polynomial-time heuristic. On an aerial-imagery benchmark of 15 weather-shifted test sets and six ViT detectors, our domain-knowledge-free layer matches the strongest majority-vote variant on clean data (within $0.005$ F1) and, unlike every majority-vote baseline, retains its performance under a coordinated label-flipping attack: at a $90\%$ flip rate it averages $0.42$ F1 versus $0.35$ for MV-Plurality (a $22\%$ relative gain) and attains the highest F1 on every test set once the flip rate exceeds $0.4$

Analogy allows models to apply relational knowledge from one situation to another. Benchmarks of equivalent representations test different ways of expressing the same underlying problem, whereas analogy often links situations involving different objects and content. To evaluate the analogy ability of models, we introduce GEB-Bench, a benchmark centered on cross-voice motif matching. A voice presents a motif as a scene, story, mathematical statement, or programmatic skeleton. The first task is identification across these voices. The second is matching scenes to stories or mathematical statements, and stories to mathematical statements, by their shared motif. A complete construction pipeline generates items in these voices from the relation specified for each motif, checks the order and repetition of story units, and assembles paired questions. We evaluate current models on our benchmark. Results show that matching performance depends on the target voice. The paired scene-to-story study reveals that (1) evaluated models still make matching errors when they separately identify the source and every candidate correctly, and (2) identification improves more consistently than scene-to-story matching across the evaluated Qwen model sizes. These findings show that successful motif identification does not ensure reliable matching across voices.