Papers

We introduce a novel method for verifying Lean formalizations that goes beyond LLM-judged faithfulness. Unlike most verification methods, which rely on LLMs or trained models, our method combines LLM-based semantic review with mechanical numerical and vacuity checks, providing checkable feedback and detecting errors missed by LLM judges. We apply this method, along with our Extract-Verify-Proof autoformalization pipeline, to construct the Formalized Library of Mathematical Functions (FLMF), a partial formalization of the NIST Digital Library of Mathematical Functions (DLMF). On three labeled datasets, our method achieves the lowest accepted-error rate among the evaluated methods, measured as the fraction of incorrect statements accepted by the verification method. Expert review of the results also identifies translation and source defects in existing datasets. Code available at https://github.com/annamei1/FLMF-Ch7ErrFunc-Release.git.

We study finite satisfiability of two-variable first-order logic over structures equipped with an arbitrary finite number of independent successor relations of linear orders. The number of successor relations is part of the input, and the vocabulary may contain further unrestricted unary and binary relations. We prove decidability in deterministic doubly exponential space together with a triply exponential bound on the size of a smallest finite model. This settles the unrestricted finite case beyond two successors.

We construct countable, stable, $\omega$-categorical structures with at most two binary relations whose CSPs exhibit three complexity regimes: NP-complete, decidable but not in NP, and undecidable. The templates arise from a controlled Hrushovski construction of stable $\omega$-categorical graphs $M_\alpha$ for suitable irrational parameters $\alpha>1$. Some of these graphs have NP-complete CSPs. Expanding the graphs $M_\alpha$ by the non-edge relation turns age membership into a restriction of the CSP. For every time-constructible bound $t$, there is such an expansion whose CSP is decidable but not in DTIME$(t)$. For an explicit parameter $\alpha$, the restriction to complete instances belongs to $\mathrm{coNP}$ and the full CSP belongs to $\Sigma_2^{\mathrm P}$. Separating the ages of the $M_\alpha$ using graphs with large girth and prescribed density yields $2^{\aleph_0}$ distinct CSPs of these expansions, all but countably many of which are undecidable.

Much of Ethereum's most consequential code is immutable bytecode: old output of unverified compilers, and protocol logic run as contract code. We show that such bytecode can be verified as it is, without trusting what produced it, without simplifying the machine it runs on, and with no axioms beyond Lean's own. Blanc, a Lean 4 verification stack, reads fixed runtime bytes via kernel-checked certificates and states every theorem against Jaune, an executable semantics of the EVM and block processing that passes all 34,205 blockchain-test cases of Ethereum's fixture release v20.0.2 that involve only forks that have governed mainnet since May 2025. Eight artifacts, deployed from 2017 to 2026, come from seven compiler versions and an assembler. For the EIP-7002 contract, we prove that the end-of-block call to it, whose failure would invalidate the block, succeeds whatever its storage holds, and that each block's withdrawal requests are exactly the oldest pending submissions; mainnet met these theorems' starting premises when Prague began. For a Uniswap V2 pair, we prove that after any valid history whose hashed slots stay apart, from any checkpoint representing its Solidity model's state, the storage represents that model replayed over exactly the committed calls, a balanced liquidity ledger stays balanced, and, under a premise on token answers, geometric-mean reserves per share fall only through the protocol fee. Exact gas makes liveness provable: a tracked WETH9 holder without code can withdraw by a transaction whose gas has a closed form, matching all 3,748 comparable mainnet receipts of its shape in 30,000 blocks. On Curve pool bytes compiled with the lock bug exploited in 2023, Jaune executes such a reentrancy from deployment; for bytes from a fixed compiler, we prove the lock excludes it. AI agents wrote the proofs in fifteen days under one author's direction, atop an existing stack.

We introduce the formalism of non-wellfounded and cyclic linear nested sequent calculi, developing concrete systems for linear temporal logic (LTL). The paper addresses two central problems, which we call "cycle recognition" and "unraveling." Cycle recognition concerns identifying cycles in non-wellfounded proofs in order to extract corresponding cyclic proofs, while unraveling studies the converse transformation, from cyclic proofs to non-wellfounded ones. Although these processes are well understood for Gentzen sequents, they have received little attention for more expressive sequent formalisms and become more challenging in the linear nested sequent setting. To address cycle recognition, we show the completeness of non-wellfounded proofs relative to a particular normal form exhibiting a property we call "saturation recurrence," which enables the systematic extraction of cyclic proofs. To address unraveling, we introduce a specialized procedure that shifts rule applications forward along linear nested sequents, allowing non-wellfounded proofs to be reconstructed from cyclic ones. Overall, our work provides new proof-theoretic techniques for cycle recognition and unraveling in expressive multisequent formalisms.

We construct trees with perfect matchings and independence sequences that fail log-concavity near the independence number $\alpha$. For every integer $k\geq1$, one family fails at $\alpha-k$ and has a witness of order $O(k^2\log(k+2))$. For every integer $t\geq2$, a single tree has simultaneous failures at $\alpha-1,\alpha-3,\ldots,\alpha-(2t-1)$, with a witness of order $O(t^3)$. All these trees satisfy $\alpha=N/2$, where $N$ is the number of vertices, and contradict Conjecture 4.2 of Ramos and Sun. A sufficient condition uses a fixed tree and the numbers of attached leaves. For fixed $k$ or $t$, explicit bounds give geometric decay of $a_j^2/(a_{j-1}a_{j+1})$ at these indices as the trees grow; $a_j$ counts independent $j$-sets. The proofs count independent sets by empty matching pairs. The Lean proof assistant checks formal proofs of the parameterized results and their quantitative bounds; exact 90- and 180-vertex examples illustrate the constructions.

We study definability in fixed-point logic with counting (FPC) for a class of constraint satisfaction problems (CSPs) that simultaneously generalises finite-domain CSPs and temporal CSPs. The templates for the CSPs are first-order expansions of the structure $([k] \times {\mathbb Q};<_1,\dots,<_k,\sim)$ where $<_i \, := \{((i,x),(i,x')) \mid x<x'\}$ and $\sim \, := \{((i,x),(i,x')) \mid i \in [k], x,x' \in {\mathbb Q}\}$, i.e., $k$ copies of $({\mathbb Q};<)$. Such a CSP is definable in FPC precisely when the template pp-constructs neither the ternary temporal relation $X$, which holds on three elements if the minimum is attained exactly twice, nor a nontrivial finite affine structure. Equivalently, the template has global polymorphisms that witness the tractability of the temporal CSPs on the copies, and that provide 3-4 weak near-unanimity operations on the set of copies of ${\mathbb Q}$. In this case, we prove that the CSP is even expressible in the less expressive logic FP$^*$, which is the restriction of FPC without counting terms (i.e., the extension of first-order logic by a fixed point operator and an ordered auxiliary number sort). Our algorithm samples finitely many values in each copy and then performs nested constraint-singleton consistency tests (which is a uniform polynomial-time algorithm for finite-domain CSPs). The correctness proof uses finite-domain CSP theory to combine consistency certificates by a single polymorphism term, fixing each variable to one copy without destroying the certificates needed for the temporal algorithm. We then use a known normal form for algebraic products to control the remaining interactions between different copies.

This paper studies the complexity of model checking strategic abilities in multiagent systems under imperfect information, in particular systems represented succinctly. Such a representation can describe systems that are exponentially larger than their input and is particularly relevant to practical implementations of model checkers such as MCMAS. The logics we consider include epistemic strategy logic supporting partial binding $SLK_{P}$, and its syntactic fragments: epistemic strategy logic $SLK$ and variants of Alternating Time Temporal logics. We show that succinct model checking for $SLK_P$ and $SLK$ is $AEXP(poly)$-complete, while objective ATL and ATL$^{*}$ are $P^{NEXP}$-complete. The latter corrects a previous NEXP-completeness result for model checking succinct imperfect-information systems. Under subjective semantics, $P^{NEXP}$-completeness already holds for one-step Coalition Logic, and therefore also for ATL and ATL$^{*}$.

Connection-tableau provers typically construct closed tableaux by backtracking search. This gives lightweight proof procedures, but their low-memory search state leaves little derived information to reuse after a failed attempt. SATCoP addresses this by retaining grounded tableau clauses in an incremental SAT solver, allowing the prover to refute the problem once the accumulated ground clauses become propositionally unsatisfiable. We introduce SATResetCoP, which relies more directly on this persistent SAT state by not backtracking on unproductive tableaux and instead starting new ones to generate further ground clauses for the SAT solver. On TPTP, SATResetCoP improves over our leanCoP-style baseline by 54% and our SATCoP-style baseline by 18%. On the bushy MPTP2078 benchmark, it solves 616 problems, a 49% improvement over our leanCoP-style baseline and a 12% improvement over our SATCoP-style baseline. These results suggest that changing tableau guidance to accumulate useful ground clauses faster improves the performance of the prover.

Specification-Guided Reinforcement Learning (RL) has largely concerned itself with learning an optimal policy against a formal specification in an unknown Markov Decision Process (MDP). We take up the dual question. Given a policy already in hand, can one verify that it is correct against a formal specification in an unknown MDP, using sampling access alone? Such a question arises naturally in safety-critical systems. We investigate it for the almost-sure reachability property, whose correctness is witnessed by a ranking supermartingale (RSM) certificate. Our first finding is negative. In the absence of any further information about the MDP, one can neither learn such a certificate nor verify a candidate one with probabilistic guarantees. On the positive side, we show that, under a mild restriction, a known lower bound $p_{\min}$ on nonzero transition probabilities, a correct certificate can be learned with PAC-style guarantees. To the best of our knowledge, this is the first study of learning and verifying certificates for almost-sure reachability in unknown MDPs from sampling access alone. Finally, our experiments show that the $p_{\min}$-based sufficient condition, while sound, is conservative: the learned certificate often remains valid on the true MDP even when the condition fails.

AI systems now write long and difficult mathematical proofs, and checking their step-by-step validity is becoming a bottleneck. A learned verifier could check proofs cheaply, but training one requires a correctness label on every step, and such labels are hard to obtain for open-ended proofs. Existing methods take them from human annotators, which is costly, or derive them from final answers, which proofs do not have, and formalizing each proof in Lean requires expert effort. We introduce LeanPRM, a framework that uses the Lean proof assistant to create step-level labels for natural-language proofs. A model writes a natural-language proof together with a paired formal proof, without feedback from Lean. Lean then labels every step, and a second model discards failures caused only by the formal syntax, so that the negative labels mark errors in the mathematics. LeanPRM contains 10,634 proofs with 152K labeled steps and no human annotation. A Qwen3-4B verifier trained on LeanPRM raises exact step-label accuracy on a held-out set of 200 proofs (LeanPRM-Bench) from 48.2 to 74.7, as opposed to 60.3 when the same base model is trained on PRM800K. It also selects better proofs in best-of-N selection on IMO-level problems, and outperforms the PRM800K-trained verifier on three of four external verification benchmarks. Training on LeanPRM improves verifiers at every size from 0.6B to 8B parameters on LeanPRM-Bench, Hard2Verify and IMO-GradingBench. Given the labels need no human annotation, LeanPRM can grow with the supply of formal statements, offering a path to step-level feedback on AI-generated proofs that are hard for humans to check.

Safety verification of a Markov decision process (MDP) asks whether the probabilities of reaching several failure states jointly lie in a convex safe region under every scheduler. Watanabe and Unno (2026) prove safety by refining an outer approximation of the failure probabilities, where each query bounds a nonnegative weighted sum of the probabilities. Their rule selects weights by the largest Euclidean violation. We present a unified framework to measure violation in an explicitly chosen error unit: directions are scored by the support-function gap between the outer approximation and the safe region, normalized by the support function of the unit. We show that the maximal score, when positive, equals the smallest enlargement of the safe region in multiples of that unit that contains the outer approximation. The Euclidean unit recovers the earlier rule; two new rules are generated by the unit cube and the safe region itself. We experimentally evaluate how the choice of measurement rule affects the performance of safety verification for MDPs.

Financial Artificial Intelligence (AI) governance and model risk management (MRM) emphasize independent validation, transparency, and effective challenge of AI-generated computations. Text-to-SQL translates natural-language questions into Structured Query Language (SQL), but queries that agree on one database can still express different computations. We present VeriPIE, a neurosymbolic framework combining language-model generation with symbolic checks. It ensembles direct SQL generation with QuerySketch, a structured plan language checked by a backend implemented in Lean, a theorem prover and programming language. Plan diagnostics guide repair before SQL generation, while execution agreement and bounded searches for distinguishing databases inform candidate selection. These checks expose malformed plans and hidden disagreement without proving agreement with the user's intent. In single-run experiments on the complete Spider development set, VeriPIE achieves 72.05% test-suite accuracy (745/1,034), compared with DeepEye's 65.67% (679/1,034). Its two-query shortlist covers 78.43% (811 questions), compared with 74.66% for DIN-SQL (772) and 69.05% for DeepEye (714). On BIRD, VeriPIE reaches 68.90% execution accuracy and 73.73% two-query coverage. The central benefit is reviewable evidence about the generated computation: explicit plan checks, repair diagnostics, and concrete disagreements that support safer financial analysis.

General-purpose coding agents use standard shell and file interactions, yet formal theorem-proving agents often rely on specialized, ad-hoc tooling. This makes it difficult to determine which components of theorem-proving agents provide benchmark gains: an improved base model, a specialized harness, a specific tool, or a combination of any of them. We introduce mini-Lean-agent, a deliberately minimal agent for Lean tasks whose only model-visible tool is bash. The model must use bash to inspect and edit the repository, search local libraries, invoke Lean, and manage its own intermediate work, while a separate trusted evaluator verifies the final artifact. We compare mini-Lean-agent against AxProverBase and Numina-Lean-Agent on the Putnam 2025 benchmark. Experiments with Gemini 3.8 Flash as the base model show that mini-Lean-agent solves 7/12 problems at \$2 per problem limit, compared with AxProverBase's 4/12. With Astra as the base model, mini-Lean-agent solves 12/12 problems at an average cost of \$1.28 per problem. This suggests that a generic coding agent with a minimal harness can already achieve strong performance on Lean benchmarks. Our results motivate using mini-Lean-agent as a standard baseline when evaluating theorem-proving infrastructure.

This concise manuscript investigates the nonlocal nature of natural deduction, particularly the possibility of introducing assumptions at intermediate stages of a derivation after those stages have already been passed. By examining the structural correspondence between natural deduction and sequent calculus, we demonstrate how the structural rule of left-weakening (LW) permits the enlargement of an antecedent after its corresponding succedent has been derived, without modifying the original inference. Through a number of symmetrical derivations, we establish the proof-theoretic relationship between the introduction of assumptions in natural deduction and antecedent expansion in sequent calculus. On this basis, we formulate the principle of Nonlocal Assumption Introduction (NAI), according to which assumptions may be introduced at any intermediate stage prior to the final conclusion, provided that the corresponding structural expansion is proof-theoretically valid. We further specify the conditions governing this operation, including the preservation of inferential validity, assumption dependencies, and the scope and discharge requirements of the resulting derivation.

Tool-using LLM agents are increasingly used to automate workflows governed by procedural manuals, such as company rules for booking travel or procuring hardware. These manuals are written in natural language for humans and describe general requirements over such complex workflows. Ensuring compliance of LLM agents with these manuals is difficult, and state-of-the-art techniques use either LLM judges or manually written rules to forbid problematic tool-calls locally at runtime. This is insufficient because (i) only blocking tool calls keeps the agent clueless about how to make correct progress towards fulfilling its task, and (ii) can lead to overly conservative behavior of the agent, as tool calls might only be problematic in certain contexts. To overcome these challenges, we introduce MENTOR, which (i) additionally provides guidance for the agent to make procedural-compliant progress on the task, and (ii) ensures that this compliance is context-aware. We achieve these goals by building a novel history-dependent runtime shield that is obtained from the procedural manual via a multi-step autoformalization pipeline. At its core, MENTOR utilizes a game-based technique to ensure robustness against runtime uncertainty without over-resticting agents' behavior. This yields a formally assisted framework for procedural shielding of LLM agents that improves compliance well beyond existing methods. In particular, MENTOR lifts the compliance of shielded light-weight open-source LLMs above that of non-shielded proprietary models. Since a shield is synthesized once per manual and then serves every task, a MENTOR-shielded agent becomes a viable choice for repeatedly executed workflows, potentially reducing deployment costs when the offline construction cost is amortized over repeated tasks.

A landmark result states that the expressive power of graph neural networks (GNNs) is bounded from above by the 1-dimensional Weisfeiler-Leman (1-WL) test. We ask whether a constant-depth GNN can match the expressive power of 1-WL while using only rational weights. We prove that this is the case when Schanuel's conjecture, a famous open problem from transcendental number theory, is taken to be true. Our GNN construction works even with integer weights, and more generally with a broad range of rational weights. As the activation function, it may use logistic sigmoid, hyperbolic tangent, or related functions. It is uniform across all graph sizes. We also prove a partial converse: if a GNN with exponentiation, hyperbolic sine or hyperbolic cosine as activation matches the expressive power of the 1-WL test in a slightly more expressive setting where graphs may contain certain auxiliary vertices, then this implies Schanuel's conjecture restricted to the numbers that arise in computations of the GNN. We also conduct experiments showing that the constructed GNNs indeed match the 1-WL test.

Fix a finite alphabet $\Sigma$ having at least two letters, and natural numbers $n,k\geq 1$. We denote by $D_n(\mathbf{\Pi}^0_k)$ the class of differences of $n$ subsets of the Cantor space $\Sigma^\omega$ in $\mathbf{\Pi}^0_k$, and by $\checked{D}_n(\mathbf{\Pi}^0_k)$ the class of complements of sets in $D_n(\mathbf{\Pi}^0_k)$. We prove, for any natural numbers $n,k\geq 1$, the existence of a finite alphabet $\Sigma$ having at least two letters and a finitary language $U_{n,k}$ over $\Sigma$ accepted by a one-counter automaton such that the $\omega$-power $$U_{n,k}^\infty:=\{ w_0w_1\cdots\in\Sigma^\omega\mid\forall i\in\omega ~~w_i\in U_{n,k}\}$$ is $D_{2n-1}(\mathbf{\Pi}^0_k)$-complete. We also prove a conditional result for the dual classes $\checked{D}\_{2n}(\mathbf{\Pi}^0\_k)$: under the assumption that there exists a finitary language $V_{n,3}$ accepted by a one-counter automaton, such that its $\omega$-power $V_{n,3}^\infty$ is $\checked{D}_{2n}(\mathbf{\Pi}^0_3)$-complete, there would also exist, for any integer $k>3$, a finitary language $V_{n,k}$ accepted by a one-counter automaton, such that its $\omega$-power $V_{n,k}^\infty$ is $\checked{D}_{2n}(\mathbf{\Pi}^0_k)$-complete. Finally we add another conditionnal result about Wadge degrees of rational $\mathbf{\Delta}^0_2$ omega powers, which completes the recent results of [FGL26].

We describe Redhill, a Lean formalisation of the major results in Hölzl, Kleine and Stephan's "Improved Lower Bounds for Strong $n$-Conjectures" (arXiv:2409.13439). Design decisions regarding types and data structures are justified as enabling canonical versions of the paper's claims, and from there the most direct proofs of said claims. The formalisation process also uncovered many errors, omissions and optimisation opportunities in the informal proof, all of which are addressed in the final library. Although Redhill is meant to stand alone, a few lemmas were upstreamed to the primary Lean mathematics library mathlib. We discuss the tension between upstreaming and leaving lemmas in separate libraries. Unlike many other contemporary formalisation projects, Redhill was completed without any assistance from large language models (LLMs). We compare our work with LLM-assisted projects, in particular an extension of arXiv:2409.13439 to $n=4$, aiming to establish design and style guidelines that define good Lean formalisations.

Embedded platforms increasingly host safety-related streaming functions next to less critical ones. Whether a safety architecture pattern, such as a doer/checker pair, protects a function depends on the cores that run its components. Their schedule must meet the throughput requirement, and mixing safety integrity levels (SILs) on one core raises development cost. This report presents SafeDSE, a design space exploration framework for synchronous dataflow applications. One declarative constraint model decides the pattern of each actor, the placement that the fault model requires, the static-order schedule, and the platform, and prices SIL promotion. Guards activate the chosen patterns in a fixed graph that holds all of them, and node potentials encode throughput. An independent verifier re-checks every solution, and a generator turns its checks into evidence of a safety argument in Goal Structuring Notation. On 9 benchmark instances under period bounds, no rule that fixes patterns before mapping was both always feasible and never more expensive under conservative pricing, while joint exploration was. In the generated arguments, 49 to 62% of the leaves cite verifier checks; the rest are claims a mapping cannot discharge. Optimality within the model was proven for all synthetic graphs with up to 16 actors. This extended version adds the full model, the verifier and generator in detail, the complete catalog and parameters, and a proof of the potential characterization. It also reports every experiment per instance, a mutation analysis of the verifier, and the negative results of the development.

A first-order theory $T$ has the finite model property if every first-order sentence that is implied by $T$ has a finite model. We give a characterization of when a complete $\omega$-categorical theory $T$ has the finite model property. The characterization makes it possible to transfer stability theoretic results in [29] to certain classes of finite structures. This approach also gives information concerning properties that a sequence of finite “base structures” of ever larger size must have in order for its random expansions to a larger vocabulary to have a chance to satisfy a convergence law for first-order logic.

A hereditary graph class has strongly edge-sublinear separators if, for some constant $0 \leqslant b < 1$, every graph in the class with $m$ edges admits a balanced separator of size $\mathcal O(m^b)$. We show that Max Weight Independent Set (MWIS) admits a deterministic quasipolynomial-time approximation scheme (QPTAS) on every such class. In particular, this applies to graphs excluding any fixed graph as an induced minor, by a separator theorem of Korhonen and Lokshtanov [SODA 2024]. Our theorem generalizes the QPTASes for axis-parallel rectangles [Adamaszek and Wiese, FOCS 2013] and polygons [Adamaszek, Har-Peled, and Wiese, JACM 2019], or equivalently for packing connected subgraphs of a planar graph [Pilipczuk, van Leeuwen, and Wiese, Algorithmica 2020]. It also generalizes the QPTAS for MWIS on hereditary classes with strongly sublinear separators measured in vertices [Dvořák, EJC 2018; Dvořák and Lahiri, ESA 2021], as well as the QPTASes for graphs excluding particular induced minors [Chudnovsky et al., arXiv 2025; Bonnet et al., SWAT 2026; Czyżewska et al., arXiv 2026].

Many questions about large textual corpora concern patterns that unfold over time, such as a political group whose stance on a topic drifts from support to criticism over several years of debates. We present TL;QR (Too Long; Query with logical temporal Reasoning), a declarative query language and open-source engine for finding such temporal discursive patterns. In TL;QR, a single query combines natural-language predicates, whose truth is judged by a Large Language Model (LLM), with regular expressions and the operators of a temporal logic. The LLM answers only local questions about individual text passages; a symbolic engine then aggregates these judgments over time and links every match to the recorded passages and predicate decisions behind it. With this division of labor, the temporal and relational reasoning stays exact and auditable even over long time horizons. In addition, when a query includes a regular-expression pre-filter, only a small fraction of the corpus ever reaches the LLM. On a suite of controlled synthetic benchmarks with temporally and semantically complex patterns, TL;QR is substantially more accurate than LLM-only baselines. In a case study on ten years of European Parliament debates (442,593 multilingual speeches), TL;QR identifies candidate shifts in the political groups' stances on the GDPR privacy regulation.

Propositional Dynamic Logic (PDL) is a well-established modal logic of programs. Among its many extensions, the loop operator stands out for capturing the cyclic behaviour of programs: a world satisfies loop(pi) precisely when it can return to itself along a path matching the regular expression pi. While the satisfiability problem for the resulting logic LPDL was settled already in the 1980s, the decidability of its finite satisfiability problem has remained open ever since. The core difficulty is inherent to the finite setting: requiring and forbidding cycles at once is easily reconciled over arbitrary models, but over finite ones it defeats the existing finite-model-theoretic techniques. We make the first substantial progress towards closing this gap. We prove that finite satisfiability is ExpTime-complete for LPDL formulae (also in the presence of the converse operator) in negation normal form, under the restriction that every negated non-atomic loop has the form loop(pi^+) for some arbitrarily complex program pi – a generalised form of self-reachability; positive occurrences of loops remain unrestricted. At the heart of our approach lies a novel way of representing intended finite models as their infinite, cactus-like unravellings: these are recognisable by two-way tree automata and satisfy a tailored omega-regular foldability condition that lets us finitise the accepted structures.

Vision-Language-Action (VLA) models commonly generate robot actions token by token through Large Language Model (LLM) decoders, causing inference latency to grow with action sequence length and limiting closed-loop control frequency. We present Goal-Conditioned Vision-Predictor-Action (VPA), which replaces autoregressive decoders with a lightweight latent control loop. A shared vision encoder and a frozen text encoder embed observations, goal images, and instructions; a neuro-symbolic selector chooses a discrete skill; a Joint-Embedding Predictive Architecture (JEPA) predictor forecasts the next latent state; and a flow-matching solver generates an entire action chunk in a few integration steps, so that sequential network evaluations per decision step do not depend on the action horizon. We analyze inference complexity, regularization against representation collapse, and conditions under which latent sub-goal thresholding limits error accumulation across task phases. As an initial proof of concept, we evaluated VPA on the LIBERO-10 suite. The trainable model has under 20M parameters (checkpoint under 75 MB, excluding a frozen 63.4M-parameter CLIP text encoder); a decision step of a single-camera reference configuration takes 10-14 ms on an Apple M4; and trained only on LIBERO-10 demonstrations in under three hours on a single GPU, a two-camera policy succeeded in 40.0% of 200 evaluation episodes. These preliminary results from a single training run suggest the approach is workable. Code and weights are available at https://github.com/ylee-sling/Vision-Predictor-Action and https://huggingface.co/ylee-sling/vpa-libero10, and archived at https://doi.org/10.5281/zenodo.22960920.

One of the most well-known connections between logic and games is Pauly's representation theorem: the induced powers of individuals and coalitions in concurrent game frames correspond, in a precise sense, to a certain class of neighborhood frames. The precise sense here is what is called alpha effectivity (or alpha power): the power of a coalition is characterized by the sets of states in which it can ensure that the outcome lies by taking some joint action. This definition is inherently monotonic, and, as pointed out by van Benthem, Bezhanishvili, and Enqvist (2019), that fact can obscure relevant information about the power structure in the game: we do not know whether two sets that a coalition has the power to enforce correspond to the same joint action or to different joint actions. An alternative is to characterize the power of a coalition by its actual power (called basic power by van Benthem, Bezhanishvili, and Enqvist (2019)): the collection of sets of states, each of which corresponds to one joint action by the coalition and all possible joint actions by the other agents. It has recently been argued by Li and Ju (2025, 2026) that standard concurrent game frames rely on three assumptions that may, in some cases, be too strong: seriality, independence of agents, and determinism. This yields a total of eight different classes of general concurrent game frames. In this paper, assuming two agents, we prove that, in terms of actual powers, the eight classes of general concurrent game frames are represented by eight corresponding classes of neighborhood frames. This generalizes a result by van Benthem, Bezhanishvili, and Enqvist (2019).

Otto's Theorem characterises the bisimulation-invariant PTIME queries over graphs as exactly those that can be formulated in the polyadic mu-calculus. This extends to a characterisation of the full bisimulation-invariant exponential-time hierarchy, using a higher-order extension of the polyadic mu-calculus, called PHFL, which is naturally stratified by type order. The bisimulation-invariant fragment of k-EXPTIME is captured by the fragment of PHFL whose formulas have type order at most k. This is obtained using a generalisation of the Immerman-Vardi Theorem by Freire and Martins. Here we provide such a characterisation of the exponential-space hierarchy. We show that the bisimulation-invariant fragment of k-EXPSPACE is captured by the fragment of PHFL of type order k+1 whose formulas are tail-recursive. Tail recursion limits the interplay between fixpoints and higher-order functions so that model checking based on fixpoint iteration can be made more space efficient in a way comparable to tail recursion in programming languages. The capturing result makes use of a generalisation of Vardi's characterisation of PSPACE as first-order logic with partial fixpoints, namely that k-EXPSPACE is captured by higher-order logic of order k+1 with partial fixpoints.

Efficient neural architecture search (NAS) requires accurate performance estimation under limited evaluation budgets. Existing zero-cost proxies (ZCPs) provide fast training-free signals, but each proxy usually captures only a partial property of an architecture, leading to unstable rankings across datasets and search spaces. In contrast, GNN-based predictors can improve accuracy, but often depend on labeled architectures, graph encoders, and costly representation learning, which makes them less suitable for extreme few-shot settings. We propose FENAS, a topology-agnostic few-shot prediction framework that turns complementary initialization priors into robust ranking signals. Its core component, CAST, is a feature pipeline that combines copula alignment and synergy transformation. CAST maps heterogeneous ZCPs into a compact feature manifold, enabling lightweight meta-learners to produce reliable rankings from scarce supervision. On NAS-Bench-201, with only 0.5% labeled samples, FENAS achieves a Kendall's Tau ($\tau$) of 0.70, outperforming representative topology-based few-shot predictors in this low-label regime. In closed-domain search, FENAS evaluates the NAS-Bench-201 space in approximately 1138 seconds and achieves competitive test accuracy. By providing a fast, reliable, and structurally simple evaluation mechanism, FENAS supports the design of automated neural architectures under limited evaluation budgets.

We introduce Sequent-Prover, a family of verifier-using language-model agents, and the post-training framework that produces them. Agents reason in an executable SMT-LIB scratchpad: they write complete SMT-LIB programs, query Z3 across turns, inspect solver feedback, repair formalizations, and terminate with an explicit answer. Our recipe, verifier-conditioned trajectory distillation, bootstraps from a noisy teacher proposal policy by sampling multi-turn trajectories, retaining the successful tail that is correct, non-trivial, grounded, and executable, then applying supervised fine-tuning and trajectory-level preference optimization. Because solver success alone does not guarantee semantic faithfulness, we evaluate task accuracy, k-sample reliability, and SMT program quality. Across 37 benchmarks and 7,254 problems per model family, post-training raises the 4B model's per-attempt accuracy from 85.6% to 97.0% and four-sample all-correct reliability (pass^4}) from 64.1% to 91.7%. It also reduces average SMT calls from 4.10 to 2.52 and tokens per attempt from 18.97k to 12.72k. Sequent-Prover agents give answers backed by executable formal artifacts.

We present a typed proof-term calculus for intuitionistic intensional first-order logic with Hilbert's epsilon-operator and prove its soundness and completeness with respect to hyperdoctrinal models with thin bicartesian closed setoid categories (BiCCCs) as fibres and formula-indexed witness selections. The calculus provides an explicit internal language for these epsilon-hyperdoctrines: for each fixed typed signature, its syntactic term model is initial for syntax-indexed, interpretation-preserving model morphisms, with uniqueness up to setoid equality. The nested epsilon syntax is organized by a well-founded dependency relation on formula labels. Concrete countermodels exhibit failure of excluded middle and show that formula conversion need not identify the selected witnesses. We also compare the full calculus with its epsilon-free and epsilon-only fragments. The principal constructions and metatheorems are formalized in Rocq. With setoid BiCCCs, proof irrelevance is a choice of equality, not the erasure of proofs: the proofs and their categorical operations remain available as the basis for a future proof-relevant categorical semantics.