Papers

Many exact Hamiltonian-cycle solvers use the same edge-level representation for every input, even when graph structure admits a smaller set of global decisions. We present StructHCP, a SAT–CEGAR pipeline that selects a representation through inexpensive structural recognizers. Specialized searches handle high-degree clusters and paired chains, while complete directed and undirected encodings handle cubic and general graphs. Every returned cycle is reconstructed when necessary and verified in the input graph. On the 1,001-instance FHCP Challenge Set, StructHCP solves 826 instances, compared with 741 when the same general SAT–CEGAR engine is applied directly to every unreduced input graph. Relative to this ablation, StructHCP reduces PAR-2 by 32.9 percent. Formulation selection solves 82 more instances than the contracted general encoding; high-degree-cluster and cubic graphs account for 81 of this difference. StructHCP also solves 34 of the 51 instances solved by neither HCup nor Cut-set CEGAR, raising the combined coverage of the three solvers from 950 to 984. Twelve of its solutions lie outside the union of published per-instance SAT results analyzed here, and six also lie outside the published exact result sets in our comparison. These results show that selecting the representation can complement connectivity refinement on structured HCP instances.

Camera-first agents must act on the visual world as it unfolds. We argue that the central obstacle for future camera-first agents is not recognition ability - multimodal models (vision-language and live/streaming alike) generalize well through language and remain the right tool for semantic reasoning - but time. Many visual targets are ephemeral: they appear, are query-relevant, and leave within a short window. Binding memory to the same end-to-end path as reasoning means that by the time a monolithic pipeline completes, the evidence is gone. We formalize this as Ephemeral-Target Interaction (ETI) and a Perceptual Deadline Contract separating a hard memory deadline from a soft reasoning deadline, grounded in the bounded, passive nature of sensory and working memory. We propose a two-deadline architecture: an always-on, bounded, non-semantic fast path; an active remembering mechanism that commits a moment to durable memory before it is overwritten (event-driven in v1); and a deferred deliberation layer (multimodal model + tools). We instantiate the contract on real MOT17 track windows, a consistency check, and calibrate the single-path baseline from measured frontier-model latency: even a short answer takes 1.2-9.3 s, and an agentic identify-and-search longer. Answers can be late; evidence cannot be missed.

The Distributed Flexible Job Shop Scheduling Problem (DFJSP) requires the joint determination of factory assignment, machine selection, and operation sequencing to minimize the makespan. This paper presents an exact SAT-based approach built on an efficient SAT formulation that exploits problem structure through propagation, symmetry breaking, and incremental SAT solving to effectively address these coupled decisions. The proposed method is evaluated on 76 standard benchmark instances from the Fattahi, Brandimarte, and rdata datasets under two- and three-factory configurations. Together with previously established results, the new SAT optimality certificates bring the total number of proven-optimal instances to 72 out of 76, including three newly certified instances; for two of these instances, SAT also improves the previous best-known makespans. Across the benchmark configurations, SAT achieves the best results on four of the five configurations and remains competitive with strong exact approaches such as CP and LBBD1_CPIL, as well as existing metaheuristic methods. These results demonstrate that the proposed SAT framework is an effective exact approach for the DFJSP, combining strong solution quality with rigorous optimality certification and offering a complementary exact method for future DFJSP studies and evaluations on additional benchmark instances.

AI systems are making rapid progress in mathematics, but this progress is hard to measure. Benchmarks of solved problems saturate, and in benchmarks of open problems each problem can be resolved for the first time only once. We present SqueezeBench, a benchmark that is resilient to saturation: a success raises the bar instead of removing the problem. Each problem fixes an integer function $f(n)$ whose values are known only for small $n$, and the benchmark keeps a lower and an upper record on it. A record is a computable Lean function with a machine-checked proof that it bounds $f$. A submission proposes a new function and proves that it bounds $f$, that it is no worse than the current record at any $n$, and that it is strictly better at some $n$. Once accepted, it becomes the record that the next submission has to beat. The system thus chooses the bound as well as its proof, and it may improve the record at a single $n$ or its growth rate. At every $n$, the gap between the two records shows how far the certified bounds are from determining $f(n)$. Every proof is checked by two independent Lean kernels, so no referee needs to check the mathematics. The checks also reject a function that computes $f$ by exhaustive search at small $n$, and a maintainer only reads the submitter's report and looks for such a search at larger $n$. We release ten problems from extremal combinatorics with twenty proved initial records and the admission tools. As a baseline, agents based on a frontier language model, with at most one hour per record, had 82 submissions accepted and improved every record, without going beyond the published literature. Agents based on two newer models then started from these records, had 60 more submissions accepted and improved 19 of the 20 records again. For eight of the ten problems, at least one record is still asymptotically behind the best published bound.

Proofs in quantitative algebra are, generally, infinite objects due to the presence of infinitary rules in the deductive apparatus. A quantitative equational theory is called compact if all its consequences are derivable by means of finite proofs, that is, proofs not using any instances of the infinitary rules. This definition is purely logical. In this work we give an equivalent, but categorical, characterisation based on the notion of monad restriction.

Clef was created as a concurrent programming language whose compiler tracks state ownership, waiting computations and request dependencies. We develop a coexponential account of stateful services and their client pools within this design. Delimited continuations retain the computation and resources needed to complete each interaction. These structures give our compiler premises for verifying service composition and preserving it through native lowering to multiple hardware targets. We connect finite actor state transitions to the initial, service and final rules of a coexponential server. A separate operational account relates actor dispatch to single-use continuation frames. We prove state-ownership and reply preservation for that translation, give a finite communication-summary analysis, and circular-wait exclusion from the conditions needed. A further result identifies when changing service order preserves both state and replies. Our Program Semantic Graph retains these facts through compilation. We are researching reusable proofs to confirm the ownership and communication interfaces, while our BAREWire implementation connects message meaning to its unboxed representation across respective endpoints. A distributed worker example preserves request identity across suspension, reordered replies and boundary conversion. Urschel's elimination-growth bounds supply quantitative premises for a solver service, whose accuracy and failure budget compose with the protocol contract. The design we envision connects automatic structural analysis, reusable proof terms and native realization. Protocols determine the admissible interactions, continuations expose their storage requirements, and retained dependencies support differential compilation. Developers can express ordinary stateful services while the compiler carries the conditions for their correct composition across execution targets.

This paper presents a leakage-resistant framework and benchmark (LRFB) for measuring evaluators of AI-generated Oracle PL/SQL specifications. The benchmark contains 494 labelled source-specification pairs across 19 quality metrics grouped into seven dimensions; each metric contains 26 records divided into development and held-out subsets of 13 records each, with three clean and ten defective specifications per subset. Ground truth is mechanically sealed from inference and checked with canary and label-permutation tests. Three LLM judges were evaluated with three runs per record and compared against two trivial baselines. On 247 held-out records, GPT-4o, DeepSeek V4 Pro, and Claude Sonnet 4.5 reached balanced accuracies of 0.87, 0.89, and 0.81, respectively, while a specification-length baseline reached 0.88. Exact paired tests did not separate any judge from that baseline. The judges nevertheless provided information unavailable to length: the labelled defect category appeared among findings in 84%-92% of violated records, and quoted evidence overlapped the labelled span in 92%-93%. The study therefore reframes specification evaluation from binary issue detection toward evidence-linked, typed findings and benchmark-validity controls.

A fixed network of McCulloch-Pitts threshold units with weights in {-1,0,1} can hold other threshold networks in its state and run them: the state is a ring of banks of records, each record a unit of a stored network, and each step evaluates one record. We use such a network to carry out von Neumann's universal construction and self-reproduction exactly. As a cellular automaton keeps its rule, the fixed network keeps its weights, and what reproduces is a stored network. A constructor of 143 records reads the description of a network from its tape, builds that network in the next bank, copies the description onto the next tape and hands control to what it built; started on its own description, it rebuilds itself, weights included, in every generation. The scheme scales to a universal computer. A SUBLEQ computer of 17,598 ternary units, stored as 36,080 records and running a program of 27 instructions, builds any network that fits a bank and reproduces itself in the same way, at every word width from eight bits on; run directly, it emits the serialization of its own weights, memory and tape. Integer pre-activations give every orbit a margin of 1/2, and replicating each unit r times multiplies it by r. That suffices against noise of any size on the pre-activations, but against von Neumann's output flips only below a threshold inversely proportional to the fan-in. These results are proved in Rocq.

We introduce a self-improvement loop for reasoning models based on the following observation: Even when the difficulty of a problem exceeds the model's current solving abilities, an additionally supplied solution might enable the model to extract useful solution ideas in hindsight. We operationalize this by jointly training the same model to exhibit the following three capabilities: predicting solution ideas from problems alone, reverse-engineering ideas from problems and known solutions, and solving problems using provided ideas. The loop alternates between reverse engineering such ideas from problems with supplied solutions and using these ideas as additional supervision for joint training of all three capabilities. We give a formal specification of our method and a concrete instantiation for interactive theorem proving in the Lean theorem prover; empirical evaluation remains future work.

Abstract argumentation frameworks (AFs) introduced by Dung provide a formal foundation for non-monotonic reasoning in artificial intelligence. While decision problems for general infinite AFs typically reside at high levels of the analytical hierarchy ($\Sigma_1^1$ or $\Pi_1^1$), restricting the framework to be computably finitary reduces some of the complexity to the arithmetical hierarchy. In this paper, we present a complexity mapping of grounded and preferred semantics in computably finitary AFs across standard decision problems: credulous acceptance ($\Cred$), skeptical acceptance ($\Skep$), extension existence ($\Ex$), uniqueness ($\Uni$), and non-empty existence ($\NE$). For grounded semantics, credulous and skeptical acceptance are already known to be $\Sigma_1^0$-complete. We show that non-empty existence is also $\Sigma_1^0$-complete, whereas existence and uniqueness are trivial. These classifications are understood within the domain of valid computably finitary representations. For preferred semantics, using a computably finitely branching computation tree, $\Cred_{\pref}$ is shown to be in $\Pi_1^0$-c and $\NE_{\pref}$ is $\Sigma_2^0$-c. However, it is insufficient to reduce universal quantification and global uniqueness, leaving $\Skep_{\pref}$ in $\Pi_1^1$ and $\UniPref$ in $\Sigma_2^1$-c. Our results show the precise boundary where finitarity succeeds to bring reasoning down to the arithmetical hierarchy and where second-order quantification forces problems back into the analytical hierarchy.

Many network protocols and distributed systems combine recursion, unbounded local state, and quantitative behaviour such as cost, latency, or reliability. Existing decidability results for networks of pushdown systems are largely qualitative, and do not extend to quantitative analyses, which must jointly track traces and weights. We present a framework for the quantitative verification of acyclic networks of weighted pushdown systems. Finitely summarising a recursive network component requires collapsing the infinite family of runs obtained by pumping its nested loops, and doing so exactly, rather than by over-approximation, is a standing difficulty. We give a class of weight domains where this is possible: pumping semirings, those in which the weights accumulated by such a family collapse to a closed form; informally, the domain must be unable to count iterations. The class admits domains with infinite ascending chains, such as the arctic semiring and downward-closed languages. Over these, we give a terminating saturation algorithm computing quantitative reachability exactly, resting on two ideas: segment tree algebras, a compositional representation of runs, and thermal extensions, which symbolically separate accelerated weights so that further acceleration remains exact. We use this to compute upward and downward closures of context-free languages uniformly, and to lift the algorithm to acyclic networks over "thin" pumping semirings, yielding the first quantitative safety and reachability analyses for networks of pushdown systems.

The computation of the vertices of a polyhedron described by a system of linear inequalities is a central problem in polyhedral computation. It is a fundamental step in the conversion between H-representations, by linear inequalities, and V-representations, by vertices and extreme rays. This operation plays an important role both in the study of polyhedra and their combinatorics in mathematics and in applications to software and system verification. We present a certificate-based approach for formally verifying the computation of the vertices of a polyhedron. Given an informally computed list of vertices, our method allows to certify in the proof assistant Rocq that the list is complete, or even exact. The cornerstone of the method is a new completeness criterion based on an abstract simplicial complex that generalizes a triangulation of the normal fan of the polyhedron. A significant advantage over previous approaches is that the usually expensive numerical computations are essentially reduced to membership tests to the polyhedron, while the other steps are cheap combinatorial tests. We implement the certification method and prove its correctness in the proof assistant Rocq. We experiment with it on a variety of polyhedra, including Birkhoff polytopes, cross-polytopes, cubes, permutahedra, hypersimplices, and high-dimensional polytopes involved in the disproof of the Hirsch conjecture. Our experiments show that certification with the Rocq-to-OCaml extracted checker is typically 1.5x to over 5x faster than vertex enumeration by the state-of-the-art informal C implementation lrslib of the reverse search method.

Concurrent parameterized games involve a fixed yet arbitrary number of players. They are described by finite arenas in which the edges are labeled with languages that describe the possible move combinations leading from one vertex to another (n players yield a word of length n). Previous work showed that, when edge labels are regular languages, one can decide whether a distinguished player, called Eve, has a strategy to ensure a reachability objective, against any strategy profile of her arbitrarily many opponents. This decision problem is known to be PSPACE-complete. A basic ingredient in the PSPACE-membership proof is the reduction to the exponential-size knowledge game, a 2-player game that reflects the knowledge Eve has on the number of opponents. In this paper, we provide a symbolic approach, based on antichains, to compute Eve's winning region in the knowledge game. In words, it gives the minimal knowledge Eve needs at every vertex to win the concurrent parameterized reachability game. More precisely, we propose two fixed-point algorithms that compute, as an antichain, the maximal elements of the winning region for Eve in the knowledge game. We implemented these two algorithms in C++, as well as the one initially proposed, and report on their relative performances on various benchmarks.

Large Reasoning Language Models (LRLMs) enable multi-step reasoning for robotic task planning, but continued reasoning can overwrite valid intermediate plans or leave constraint violations unresolved, reducing planning reliability and wasting inference-time computation. We develop an inference-time monitor that exposes and verifies intermediate plans without disrupting the original decoding trajectory. Building on this monitor, we propose SafeInferCom, a formal verifier-guided framework that preserves valid intermediate plans and directs error correction during generation. Experiments across multiple LRLMs and planning domains reveal reasoning-response inconsistency and limited self-correction under one-shot inference. SafeInferCom improves planning success and accelerates error correction relative to one-shot inference. When combined with iterative refinement, it further improves success while reducing token usage compared with refinement alone. We additionally evaluate SafeInferCom in VirtualHome and provide a real-world robotic-arm demonstration.

The Weisfeiler-Leman (WL) algorithm tests graph isomorphism by assigning colours to $d$-tuples of vertices and iteratively refining the colouring according to neighbourhood configurations until it stabilizes. Increasing $d$ allows the test to detect finer structural differences between graphs, but the computational cost grows exponentially with $d$. The central question is which dimension allows us to distinguish nonisomorphic graphs. We relate a sufficient such dimension to the structure of a graph $G$ through a rank decomposition over $\mathbb F_2$. The two parameters governing the bound are the maximum cut rank $w$ and the fork load $\ell$, which is the largest sum of the parent and two child cut ranks at a fork in the decomposition tree. We prove that WL in dimension $\max\{\ell+1,2w+2\}$ distinguishes every finite nonempty vertex-coloured graph $G$ with such a decomposition from every graph not isomorphic to $G$. Consequently, for $k\geq1$, graphs of rank width at most $k$ can be distinguished from every nonisomorphic graph in dimension $3k+1$, graphs of linear rank width at most $k$ in dimension $2k+2$, and edgeless graphs in dimension one. Uncoloured Cai-Fürer-Immerman (CFI) constructions give linear lower bounds for both width parameters, so the upper bounds are tight up to constant factors.

Probabilistic programs provide a rigorous programming-language foundation for expressing rich probabilistic models and offer language-level support for solving challenging statistical inference problems. A key theoretical challenge that probabilistic programs inherit from probability theory is conditioning a probability distribution on an observation that has probability zero. Many languages address this challenge by using computational rules for conditioning that may work well for some problems but are statistically unsound for others. This article introduces a principled mathematical approach for conditioning probabilistic programs. We first show that existing techniques based on "soft conditioning" and "neighborhood limits" exhibit semantic issues from the perspective of measure theory and produce inference results that disagree with sound statistical reasoning. By leveraging tools from geometric measure theory, we construct a novel disintegration-based semantics for probabilistic program traces that enables sound conditioning. The theory delivers an explicit Bayes rule representation of the conditional distribution, which is directly compatible with widely used probabilistic inference algorithms that require access to unnormalized posterior densities. Our Bayes rule handles probabilistic models with loops, branches, discrete, continuous, and mixed-type distributions, observations on manifolds, differentiable structure, and additional modeling motifs that arise in practice.

We give a direct and explicit construction of the homotopy span model of linear logic originally formulated by Melliès using abstract homotopy theory in the Quillen category Cat of small categories equipped with its natural model structure. Following the principles of homotopy theory, the formulas and proofs of linear logic are interpreted in the model as small categories up to categorical equivalence, the notion of weak homotopy equivalence underlying the natural Quillen model structure on Cat. Here, we explain how the original interpretation of proofs as fibrant spans can be replaced by a more liberal interpretation of proofs as separately fibrant spans. This relaxation from fibrant spans to separately fibrant spans enables us to give a simple and intuitive description of the homotopy span model, where the axiom and cut links are interpreted as identity spans, and where the symmetries of the exponential modality are captured by a shuffle structure on the interpretation of proofs.

Motivated by relevant epistemic logic, we extend Dunn's simple Kripke-style binary relational semantics for the semi-relevant logic RM to fit a modal extension of RM. It is shown that the modal axioms and rules that need to be added to RM to obtain a sound and complete axiomatisation of its modal extension give an axiomatisation of modal extensions of all logics in the family of generalised Nelson logics, also studied by Dunn.

Security monitoring of edge-IoT fleets faces three structural challenges. (i) A per-node monitor is cheap but cannot see attacks that coordinate across devices. (ii) A cloud monitor sees the full fleet but pays for that view in bandwidth. (iii) Even at the cloud, a monitor built on a single RV engine can be fooled by an attacker who compromises a device, raises one malicious request, and then goes silent: once the events stop, an event-triggered monitor has nothing left to evaluate. We propose a three-layer hierarchical runtime-verification framework that addresses all three. The edge layer classifies events as they happen, the gateway layer aggregates short windows of per-device behaviour, and the cloud layer runs two complementary RV engines. MonPoly handles first-order temporal correlation over the merged alert stream: coordinated overflow (which genuinely quantifies across devices) plus per-device multi-vector APT, escalation, and persistent-campaign patterns. RTLola handles a time-triggered silent-node property that an event-triggered engine cannot detect within a bounded delay under fleet silence. We evaluate the framework on a 15-actor Docker testbed covering eight attack profiles plus a silent-bypass scenario. In the controlled labelled testbed, every device-attributable incident the framework raises names an attacker-labelled device, and the RTLola tier catches silent-bypass attempts the event-triggered tier misses. Per-event monitoring stays in the microsecond range at the edge and gateway, with low end-to-end alert-to-incident latency at the cloud.

Cyber resiliency in edge-IoT deployments is fundamentally an economic problem: detection must keep critical processes operating under attack, but defender resources (compute, bandwidth, operator attention) are bounded. Centralised cloud monitoring offers expressive cross-device detection at prohibitive bandwidth cost; purely edge-local monitoring is cheap but blind to coordinated multi-device attacks where the asymmetric balance favours the attacker. We propose a lightweight hierarchical security-monitoring framework, built on formal runtime-verification methods, that occupies the practical middle ground at quantified cost. Each edge device runs a lightweight TeSSLa stream specification (size, payload validity, rate, and timestamp-drift predicates) that emits a four-valued verdict per aggregation window at sub-microsecond per-event cost; the gateway runs a parametric first-order MonPoly monitor over the per-device verdict streams at microsecond-scale per-verdict cost. The edge-to-gateway uplink carries roughly one Boolean per aggregation window per node, orders of magnitude smaller than the raw packet stream. The gateway tier detects coordinated attack patterns that no single-node monitor can see, shifting the asymmetric cost balance toward the defender. Every alert carries a witness set naming the device, the monitor tier, and the predicate that fired, providing an auditable record of the decision. We evaluate the framework on a container-host testbed spanning nominal and attacker nodes across four attack classes (buffer overflow, time spoofing, denial-of-service, and mixed advanced-persistent-threat patterns), and describe the edge- and gateway-tier specifications together with the cost-versus-coverage trade-off as monitor levels are added.

We study two-variable first-order logic with a finite, input-dependent number of distinguished successor relations and arbitrary additional unary and binary predicates. Each distinguished relation must be the exact immediate-successor relation of some linear order on the common domain; the orders themselves are not available in the language and may have arbitrary order types. We prove that satisfiability belongs to 2NEXPTIME, uniformly in the number of successors. The proof gives finite certificates for possibly infinite models. A closure operation separates local neighbourhood descriptions, called star types, into those of bounded multiplicity and those that can be realized infinitely often. The bounded part is represented explicitly. Outside it, integer height vectors allow overlapping successor requirements to be matched without creating cycles or unintended identifications. Ordering the resulting path components densely then recovers exact successor relations. Consistent assignments of the additional binary predicates handle witnesses involving the bounded part. The same certificates decide infinite satisfiability in 2NEXPTIME and give a doubly exponential threshold above which a finite model guarantees an infinite model. A doubly exponentially large finite core can be forced with only two successors and unary predicates. For finite models, we prove that satisfiability subject to a bound on the total number of reference adjacencies lost by the other orders is NEXPTIME-complete, even when the budget is encoded in binary and the number of successors is part of the input.

Program verification establishes software correctness through machine-checkable proofs constructed in theorem provers. It's a guarantee especially valuable for code generated by large language models (LLMs), which is fluent but carries no assurance of correctness. Almost all existing provers, however, pursue pass rates alone at whatever sampling or search budget it takes, and overlook the success-vs-cost frontier; yet real software often carries hundreds of interdependent proof obligations, so what matters at scale is not whether one theorem can be proved, but how many can be proved economically. We introduce CoCo-Prover, which formalizes cost-efficient program proving as metalevel decision-making under cost, grounded on two-level proof graphs: an AND/OR proof hypergraph within each declaration is joined to a lemma-dependency graph across declarations; and at each step, it answers two questions: which open goals to select, and which actions to purchase on these goals. Selection stays symbolic as a topological pass over the proof graphs. Action choice is agent orchestration via metalevel decision-making: an agentic router treats every bounded specialist invocation as a separately priced, best-effort computation, matching heterogeneous specialist agents together with configurations, under evolved routing rules as evidence accumulates. On five program verification benchmarks in Lean 4 including function-level CLEVER, VERINA, and AlgoVeri, and repository-level NTP4VC and Vero, we show that CoCo-Prover achieves a better success-vs-cost frontier than baselines including frontier coding agents and state-of-the-art LLM-based provers: it achieves the best solve rate on every benchmark and up to 100% on two benchmarks. It also reduces cost by up to 30.9% compared to the strongest baseline with the strongest LLM in our evaluation.

This paper proposes a new method for proving the confluence of an abstract reduction system (ARS) by clarifying the sufficient conditions, called compatibility and edge commutativity, for expanding a given finite sub-ARS into a confluent one by adding rewrite edges. This method can be regarded as an extension of our earlier work, which showed that a weakly non-overlapping, shallow, and non-collapsing term rewriting system (TRS) is confluent. Furthermore, we apply our method to demonstrate that a non-$E$-overlapping and weakly shallow TRS is confluent. Here, a term is weakly shallow if each defined function symbol occurs either at the root or in the ground subterms, and a TRS is weakly shallow if both sides of all its rewrite rules are weakly shallow. This drops the non-collapsing condition assumed in our previous work on weakly shallow TRSs. Moreover, since a weakly shallow TRS is non-$E$-overlapping whenever it is non-$\omega$-overlapping, and the latter property is decidable, we also obtain a decidable sufficient condition for confluence: non-$\omega$-overlapping and weakly shallow TRSs are confluent.

Genetic programming was conceived as a way of evolving solutions: the program is the answer, and fitness is the error of its own output. A substantial line of work instead makes the program an input to a separate learner, so fitness measures the learner's output rather than the program's. Which learner to attach matters, with no account of what decides it. What makes a target hard for genetic programming is how much nonlinearity the program must build by composing primitives; whatever nonlinearity the learner supplies, the program need not. The quantity to measure is therefore how much of a target's nonlinearity a learner can take over, though on continuous benchmarks it can only be estimated. Here we show that how much the program must still build is decided by which learner is attached, and is measurable on the programs themselves. Moving to Boolean domains, where a target's nonlinearity is exactly its Fourier degree, we tune that degree from one to six with everything else fixed. Conditioned on success, a linear learner forces the evolved program to the target's degree exactly, at one through six without exception over thirty runs per setting, while tree ensembles succeed with far simpler programs and four times as often. This gives the field two things: a learner can be chosen from a target's structure instead of its reputation for difficulty, and the degree of the evolved program is a diagnostic free to compute during any run. Our control target has lower degree than the parity problems yet gains nothing from a nonlinear learner, while targets reducible to a simple statistic gain a great deal. The latter comes with a warning: evolution internalises what the learner supplies in only four of sixty-three conditions, and grows more dependent on it in forty-four, so the more capable the learner, the less of the model is legible in the program.

Rapid advances in AI have opened a new era for physics, enabling unprecedented capabilities in research and discovery. However, these advances also bring challenges in verifying, trusting, and reusing the results they so rapidly produce. Formalization is a necessary part of the solution to these challenges. In this paper, as well as giving an overview of the role of AI and formalization in physics, we make the case that: (1) formalization is an essential layer for AI-driven discoveries in both computational and theoretical physics; (2) AI is lowering the barrier to, and increasing the efficiency of, formalization in physics, though it remains weaker at choosing definitions and designing libraries than at writing proofs; (3) the speed AI brings to formalization in physics currently comes at the cost of trust, credit, and community; (4) shared, community-reviewed formal libraries such as Physlib should be central in making progress in this field, both as a trusted, reusable foundation for physics results and as the environment in which AI systems can reason about physics; (5) formalizing physics raises challenges beyond those in mathematics, most importantly that a checked proof does not establish that its definitions faithfully capture the intended physics. We also give our perspectives on near-term and long-term directions in these areas.

Fault and error detection is crucial for ensuring the correctness of safety-critical systems. Safety verification often addresses reachability of bad system states, where exhaustive state inspection may be intractable due to the large state spaces of complex systems. We propose a reachability relaxation for hybrid trace nets, a useful mathematical model for analyzing concurrent event systems, to efficiently verify system safety. We further use our relaxation to effectively identify invariants, expressions that hold in all reachable states, allowing state-space reduction for efficient verification. Empirically, our approach proves unsafe states unreachable in 1.5x more instances, generates 2.5x more invariants with up to 2 orders of magnitude faster generation times than the baselines in the tested problems.

As autonomous coding agents get increasingly deployed, the risk that accidental or adversarially injected misspecifications in tasks lead to dangerous agent behavior is critical to address. Prior work has shown that agents given such tasks rarely flag the conflict and instead cheat, editing tests or hard-coding expected outputs, and the actions taken to cheat can cause real damage, such as deleting a security defense to make a corrupted test pass. It remains unclear whether such conflicts can be established with independently verifiable evidence before the agent acts. We present SpecGuard, which detects and formally certifies these conflicts between task intent and tests. Given only the task description and codebase, SpecGuard autoformalizes the intended behaviour into a Lean 4 specification. The tests are formalized independently, and the Lean kernel checks whether any implementation could satisfy both formalizations, producing a machine-checked certificate when none can. On conflicted SWE-bench tasks, SpecGuard detects up to 72.8% of conflicts and formally certifies up to 51.1%, with a nearly five-fold lower conflict miss rate than model-based judgment. SpecGuard provides a pre-execution safety check that identifies reward-hacking opportunities through formal certification of task-level conflicts, before any agent behavior is observed. Our code is available at https://github.com/prmbiy/specguard.

SAT solvers are empirically known to perform poorly when reasoning about multiplication. Yet for over a decade we have lacked a theoretical explanation for this phenomenon. CDCL SAT solvers implicitly search for resolution proofs, and no lower bound on proof size has ruled out the existence of short proofs that solvers simply fail to find. We give the first lower bound of this kind by showing that general resolution proofs of the associativity of $n$-bit multiplication require size $2^{\Omega((n/\log n)^{1/4})}$. This lower bound holds for a broad class of multiplier encodings based on partial product summation, including the standard array and Wallace-tree multipliers used to bit-blast multiplication in SMT solvers. This result resolves an open problem of Beame and Liew. The proof constructs a reduction from a perfect-matching principle on bounded-degree bipartite expander graphs to multiplier associativity. Itsykson, Slabodkin, and Sokolov proved that this principle is hard for resolution. The lower bound for multiplier associativity follows. The same reduction, when combined with Håstad's recent lower bound for the perfect-matching principle of the odd grid, yields an exponential lower bound for multiplier associativity in the stronger bounded-depth Frege proof systems.

Let N(T) count the nontrivial zeros of the Riemann zeta function up to height T with multiplicity, N_d(T) the distinct ones, and N_0^s(T) those that are simple and on the critical line. We prove liminf N_d(T)/N(T) >= 1645064/1960733 = 0.83900...; earlier work proves 0.83699..., and a report we have not verified claims 0.83805.... Hence more than 67.80% are simple. Also liminf N_0^s(T)/N(T) >= 0.67353...; earlier work proves 0.67250..., and reports we have not verified claim 0.673492. Two estimates of Lamzouri are improved: at least 88.93% of the zeros are simple or on the critical line, and the proportions of simple zeros and of zeros on the line average at least 83.67%. By the unconditional form of Montgomery's pair-correlation theorem the energy, a sum of a test function over pairs of zeros, is known asymptotically. A zero of multiplicity d contributes d^2 to it and nearby zeros contribute too, so a lower bound for such pairs leaves less energy for multiple zeros. The proof has three steps. First, for zeros at least a fixed fraction of the mean spacing apart, a large sieve inequality lets their pairs be used in full, with multiplicities. Second, their contribution is bounded below by a computer-assisted inequality for seven or eight consecutive zeros which distinguishes simple and double zeros. Its correction terms telescope, as increments of a storage function. Third, the test function is chosen to make this contribution large, at the cost of more energy. We also prove upper limits for what such inequalities can give with the two main test functions. The lower bounds and these limits are proved in Lean 4, analytic inputs included. The proofs use three axioms beyond those of Mathlib, one per inequality. Each records that a search program returned true; Lean's kernel does not check the run itself. This work is an experiment in AI-assisted mathematical research.

LLM-based agents are entering decision-support roles in defence staff work, where the obligations they must respect are already written down and binding, and where retraining is not available as a control because models arrive as procured components. What can be placed under engineering control is the interface between the agent and the systems it acts on. Those obligations are at once spatial, temporal and text-semantic, and a violation typically lives in the composition of a multi-step interaction, which is why per-event guardrails miss sequential tool-attack chains. We present a multi-aspect runtime-verification framework that decomposes a natural-language policy clause into a typed spatial/temporal/semantic triple over one canonical event stream, checks each aspect with its own monitoring specification, and fuses the verdicts through a four-valued algebra that carries provenance. The spatial aspect is interpreted over a weighted two-sorted location graph in which mission geometry and information-release topology are one object; we show that these spatial obligations are not in general subsumed by a first-order temporal specification. The past-time aspect runs on the unmodified MonPoly engine, which agrees with our reference monitor at every time point. Across two mission domains, casualty evacuation and contested sustainment, and one civil domain, composition under the precautionary blocking policy drives attack success to zero with no observed false positives and microsecond-scale per-event cost, while every single aspect and every pair leaves a substantial share of attacks succeeding. In a closed-loop experiment a policy-naive planner reaches a violating state in most unshielded missions and in none when shielded, and four refused episodes in five still recover to a compliant outcome.