CyberSec Research

Conceptual modeling has been an important part of constructionist educational practices for many years, particularly in STEM (Science, Technology, Engineering and Mathematics) disciplines. What is not so common is using agent-based simulation to provide students feedback on model quality. This requires the capability of automatically compiling the concept model into its simulation. The VERA (Virtual Experimentation Research Assistant) system is a conceptual modeling tool used since 2016 to provide introductory college biology students with the capability of conceptual modeling and agent-based simulation in the ecological domain. This paper describes VERA and its approach to coupling conceptual modeling and simulation with emphasis on how a model's visual syntax is compiled into code executable on a NetLogo simulation engine. Experience with VERA in introductory biology classes at several universities and through the Smithsonian Institution's Encyclopedia of Life website is related.

A complete reduction $\phi$ for derivatives in a differential field is a linear operator on the field over its constant subfield. The reduction enables us to decompose an element $f$ as the sum of a derivative and the remainder $\phi(f)$. A direct application of $\phi$ is that $f$ is in-field integrable if and only if $\phi(f) = 0.$ In this paper, we present a complete reduction for derivatives in a primitive tower algorithmically. Typical examples for primitive towers are differential fields generated by (poly-)logarithmic functions and logarithmic integrals. Using remainders and residues, we provide a necessary and sufficient condition for an element from a primitive tower to have an elementary integral, and discuss how to construct telescopers for non-D-finite functions in some special primitive towers.

Traditional integral wood joints, despite their strength, durability, and elegance, remain rare in modern workflows due to the cost and difficulty of manual fabrication. CNC milling offers a scalable alternative, but directly milling traditional joints often fails to produce functional results because milling induces geometric deviations, such as rounded inner corners, that alter the target geometries of the parts. Since joints rely on tightly fitting surfaces, such deviations introduce gaps or overlaps that undermine fit or block assembly. We propose to overcome this problem by (1) designing a language that represent millable geometry, and (2) co-optimizing part geometries to restore coupling. We introduce Millable Extrusion Geometry (MXG), a language for representing geometry as the outcome of milling operations performed with flat-end drill bits. MXG represents each operation as a subtractive extrusion volume defined by a tool direction and drill radius. This parameterization enables the modeling of artifact-free geometry under an idealized zero-radius drill bit, matching traditional joint designs. Increasing the radius then reveals milling-induced deviations, which compromise the integrity of the joint. To restore coupling, we formalize tight coupling in terms of both surface proximity and proximity constraints on the mill-bit paths associated with mating surfaces. We then derive two tractable, differentiable losses that enable efficient optimization of joint geometry. We evaluate our method on 30 traditional joint designs, demonstrating that it produces CNC-compatible, tightly fitting joints that approximates the original geometry. By reinterpreting traditional joints for CNC workflows, we continue the evolution of this heritage craft and help ensure its relevance in future making practices.

Border complexity captures functions that can be approximated by low-complexity ones. Debordering is the task of proving an upper bound on some non-border complexity measure in terms of a border complexity measure, thus getting rid of limits. Debordering lies at the heart of foundational complexity theory questions relating Valiant's determinant versus permanent conjecture (1979) and its geometric complexity theory (GCT) variant proposed by Mulmuley and Sohoni (2001). The debordering of matrix multiplication tensors by Bini (1980) played a pivotal role in the development of efficient matrix multiplication algorithms. Consequently, debordering finds applications in both establishing computational complexity lower bounds and facilitating algorithm design. Recent years have seen notable progress in debordering various restricted border complexity measures. In this survey, we highlight these advances and discuss techniques underlying them.

In this paper, we present Ontolearn-a framework for learning OWL class expressions over large knowledge graphs. Ontolearn contains efficient implementations of recent stateof-the-art symbolic and neuro-symbolic class expression learners including EvoLearner and DRILL. A learned OWL class expression can be used to classify instances in the knowledge graph. Furthermore, Ontolearn integrates a verbalization module based on an LLM to translate complex OWL class expressions into natural language sentences. By mapping OWL class expressions into respective SPARQL queries, Ontolearn can be easily used to operate over a remote triplestore. The source code of Ontolearn is available at https://github.com/dice-group/Ontolearn.

Motivated by better understanding the bideterminant (=product of minors) basis on the polynomial ring in $n \times m$ variables, we develop theory \& algorithms for Gr\"obner bases in not only algebras with straightening law (ASLs or Hodge algebras), but in any commutative algebra over a field that comes equipped with a notion of "monomial" (generalizing the standard monomials of ASLs) and a suitable term order. Rather than treating such an algebra $A$ as a quotient of a polynomial ring and then "lifting" ideals from $A$ to ideals in the polynomial ring, the theory we develop is entirely "native" to $A$ and its given notion of monomial. When applied to the case of bideterminants, this enables us to package several standard results on bideterminants in a clean way that enables new results. In particular, once the theory is set up, it lets us give an almost-trivial proof of a universal Gr\"obner basis (in our sense) for the ideal of $t$-minors for any $t$. We note that here it was crucial that theory be native to $A$ and its given monomial structure, as in the standard monomial structure given by bideterminants each $t$-minor is a single variable rather than a sum of $t!$ many terms (in the "ordinary monomial" structure).

Automating the formalization of mathematical statements for theorem proving remains a major challenge for Large Language Models (LLMs). LLMs struggle to identify and utilize the prerequisite mathematical knowledge and its corresponding formal representation in languages like Lean. Current retrieval-augmented autoformalization methods query external libraries using the informal statement directly, but overlook a fundamental limitation: informal mathematical statements are often complex and offer limited context on the underlying math concepts. To address this, we introduce DRIFT, a novel framework that enables LLMs to decompose informal mathematical statements into smaller, more tractable ''sub-components''. This facilitates targeted retrieval of premises from mathematical libraries such as Mathlib. Additionally, DRIFT retrieves illustrative theorems to help models use premises more effectively in formalization tasks. We evaluate DRIFT across diverse benchmarks (ProofNet, ConNF, and MiniF2F-test) and find that it consistently improves premise retrieval, nearly doubling the F1 score compared to the DPR baseline on ProofNet. Notably, DRIFT demonstrates strong performance on the out-of-distribution ConNF benchmark, with BEq+@10 improvements of 37.14% and 42.25% using GPT-4.1 and DeepSeek-V3.1, respectively. Our analysis shows that retrieval effectiveness in mathematical autoformalization depends heavily on model-specific knowledge boundaries, highlighting the need for adaptive retrieval strategies aligned with each model's capabilities.

Direction of Arrival (DoA) estimation techniques face a critical trade-off, as classical methods often lack accuracy in challenging, low signal-to-noise ratio (SNR) conditions, while modern deep learning approaches are too energy-intensive and opaque for resource-constrained, safety-critical systems. We introduce HYPERDOA, a novel estimator leveraging Hyperdimensional Computing (HDC). The framework introduces two distinct feature extraction strategies -- Mean Spatial-Lag Autocorrelation and Spatial Smoothing -- for its HDC pipeline, and then reframes DoA estimation as a pattern recognition problem. This approach leverages HDC's inherent robustness to noise and its transparent algebraic operations to bypass the expensive matrix decompositions and ``black-box'' nature of classical and deep learning methods, respectively. Our evaluation demonstrates that HYPERDOA achieves ~35.39% higher accuracy than state-of-the-art methods in low-SNR, coherent-source scenarios. Crucially, it also consumes ~93% less energy than competing neural baselines on an embedded NVIDIA Jetson Xavier NX platform. This dual advantage in accuracy and efficiency establishes HYPERDOA as a robust and viable solution for mission-critical applications on edge devices.

Tensors are fundamental in mathematics, computer science, and physics. Their study through algebraic geometry and representation theory has proved very fruitful in the context of algebraic complexity theory and quantum information. In particular, moment polytopes have been understood to play a key role. In quantum information, moment polytopes (also known as entanglement polytopes) provide a framework for the single-particle quantum marginal problem and offer a geometric characterization of entanglement. In algebraic complexity, they underpin quantum functionals that capture asymptotic tensor relations. More recently, moment polytopes have also become foundational to the emerging field of scaling algorithms in computer science and optimization. Despite their fundamental role and interest from many angles, much is still unknown about these polytopes, and in particular for tensors beyond $\mathbb{C}^2\otimes\mathbb{C}^2\otimes\mathbb{C}^2$ and $\mathbb{C}^2\otimes\mathbb{C}^2\otimes\mathbb{C}^2\otimes\mathbb{C}^2$ only sporadically have they been computed. We give a new algorithm for computing moment polytopes of tensors (and in fact moment polytopes for the general class of reductive algebraic groups) based on a mathematical description by Franz (J. Lie Theory 2002). This algorithm enables us to compute moment polytopes of tensors of dimension an order of magnitude larger than previous methods, allowing us to compute with certainty, for the first time, all moment polytopes of tensors in $\mathbb{C}^3\otimes\mathbb{C}^3\otimes\mathbb{C}^3$, and with high probability those in $\mathbb{C}^4\otimes\mathbb{C}^4\otimes\mathbb{C}^4$ (which includes the $2\times 2$ matrix multiplication tensor). We discuss how these explicit moment polytopes have led to several new theoretical directions and results.

We develop a Koopman operator framework for studying the {computational properties} of dynamical systems. Specifically, we show that the resolvent of the Koopman operator provides a natural abstraction of halting, yielding a ``Koopman halting problem that is recursively enumerable in general. For symbolic systems, such as those defined on Cantor space, this operator formulation captures the reachability between clopen sets, while for equicontinuous systems we prove that the Koopman halting problem is decidable. Our framework demonstrates that absorbing (halting) states {in finite automata} correspond to Koopman eigenfunctions with eigenvalue one, while cycles in the transition graph impose algebraic constraints on spectral properties. These results provide a unifying perspective on computation in symbolic and analog systems, showing how computational universality is reflected in operator spectra, invariant subspaces, and algebraic structures. Beyond symbolic dynamics, this operator-theoretic lens opens pathways to analyze {computational power of} a broader class of dynamical systems, including polynomial and analog models, and suggests that computational hardness may admit dynamical signatures in terms of Koopman spectral structure.

Symbolic regression promises readable equations but struggles to encode unit-aware thresholds and conditional logic. We propose logistic-gated operators (LGO) -- differentiable gates with learnable location and steepness -- embedded as typed primitives and mapped back to physical units for audit. Across two primary health datasets (ICU, NHANES), the hard-gate variant recovers clinically plausible cut-points: 71% (5/7) of assessed thresholds fall within 10% of guideline anchors and 100% within 20%, while using far fewer gates than the soft variant (ICU median 4.0 vs 10.0; NHANES 5.0 vs 12.5), and remaining within the competitive accuracy envelope of strong SR baselines. On predominantly smooth tasks, gates are pruned, preserving parsimony. The result is compact symbolic equations with explicit, unit-aware thresholds that can be audited against clinical anchors -- turning interpretability from a post-hoc explanation into a modeling constraint and equipping symbolic regression with a practical calculus for regime switching and governance-ready deployment.

Vision Language Models (VLMs) show strong potential for visual planning but struggle with precise spatial and long-horizon reasoning. In contrast, Planning Domain Definition Language (PDDL) planners excel at long-horizon formal planning, but cannot interpret visual inputs. Recent works combine these complementary advantages by enabling VLMs to turn visual planning problems into PDDL files for formal planning. However, while VLMs can generate PDDL problem files satisfactorily, they struggle to accurately generate the PDDL domain files, which describe all the planning rules. As a result, prior methods rely on human experts to predefine domain files or on constant environment access for refinement. We propose VLMFP, a Dual-VLM-guided framework that can autonomously generate both PDDL problem and domain files for formal visual planning. VLMFP introduces two VLMs to ensure reliable PDDL file generation: A SimVLM that simulates action consequences based on input rule descriptions, and a GenVLM that generates and iteratively refines PDDL files by comparing the PDDL and SimVLM execution results. VLMFP unleashes multiple levels of generalizability: The same generated PDDL domain file works for all the different instances under the same problem, and VLMs generalize to different problems with varied appearances and rules. We evaluate VLMFP with 6 grid-world domains and test its generalization to unseen instances, appearance, and game rules. On average, SimVLM accurately describes 95.5%, 82.6% of scenarios, simulates 85.5%, 87.8% of action sequence, and judges 82.4%, 85.6% goal reaching for seen and unseen appearances, respectively. With the guidance of SimVLM, VLMFP can generate PDDL files to reach 70.0%, 54.1% valid plans for unseen instances in seen and unseen appearances, respectively. Project page: https://sites.google.com/view/vlmfp.

An efficient method is proposed for computing the structure of Jordan blocks of a matrix of integers or rational numbers by exact computation. We have given a method for computing Jordan chains of a matrix with exact computation. However, for deriving just the structure of Jordan chains, the algorithm can be reduced to increase its efficiency. We propose a modification of the algorithm for that purpose. Results of numerical experiments are given.

This paper presents a novel approach to finding analytical approximations for bright-soliton solutions in strongly magnetized plasmas. We leverage Physics-Informed Symbolic Regression (PISR) to discover closed-form expressions for the vector potential and number density profiles, governed by a reduced-order model derived from Maxwell-fluid equations. The PISR framework combines symbolic regression with physics-based constraints, boundary conditions, and available simulation data to guide the search for solutions. We demonstrate the effectiveness of the approach by rediscovering approximate solutions consistent with previously published numerical results, showcasing the potential of PISR for reducing simulation costs of reduced-order models in plasma physics.

This paper presents a novel algorithm for constructing a sum-of-squares (SOS) decomposition for positive semi-definite polynomials with rational coefficients. Unlike previous methods that typically yield SOS decompositions with floating-point coefficients, our approach ensures that all coefficients in the decomposition remain rational. This is particularly useful in formal verification and symbolic computation, where exact arithmetic is required. We introduce a stepwise reduction technique that transforms a given polynomial into a sum of ladder-like squares while preserving rationality. Experimental results demonstrate the effectiveness of our method compared to existing numerical approaches. This artical is an extension of the following Chinnese paper: HUANG Yong , ZENG Zhenbing , YANG Lu , RAO Yongsheng. An Algorithm to Represent Positive Semi-Definite Polynomials to Sum of Lader-Like Squares of Polynomials with Rational Coefficients (in Chinese). Journal of Systems Science and Mathematical Sciences, 2024, 44(5): 1241-1271 https://doi.org/10.12341/jssms23584CM

The symmetric product of two ordinary linear differential operators $L_1,L_2$ is an operator whose solution set contains the product $f_1f_2$ of any solution $f_1$ of $L_1$ and any solution $f_2$ of~$L_2$. It is well known how to compute the symmetric product of two given operators $L_1,L_2$. In this paper we consider the corresponding division problem: given a symmetric product $L$ and one of its factors, what can we say about the other factors?

We develop an effective version of Kronecker's Theorem on the splitting of polynomials, based on asymptotic arguments proposed by the Chudnovsky brothers, coming from Hermite-Pad\'e approximation. In conjunction with Honda's proof of the $p$-curvature conjecture for order one equations with polynomial coefficients we use this to deduce an effective version of the Grothendieck $p$-curvature conjecture for order one equations. More precisely, we bound the number of primes for which the $p$-curvature of a given differential equation has to vanish in terms of the height and the degree of the coefficients, in order to conclude it has a non-zero algebraic solution. Using this approach, we describe an algorithm that decides algebraicity of solutions of differential equation of order one using $p$-curvatures, and report on an implementation in SageMath.

Modern Vision-Language Models (VLMs) have achieved impressive performance in various tasks, yet they often struggle with compositional reasoning, the ability to decompose and recombine concepts to solve novel problems. While neuro-symbolic approaches offer a promising direction, they are typically constrained by crisp logical execution or predefined predicates, which limit flexibility. In this work, we introduce NePTune, a neuro-symbolic framework that overcomes these limitations through a hybrid execution model that integrates the perception capabilities of foundation vision models with the compositional expressiveness of symbolic reasoning. NePTune dynamically translates natural language queries into executable Python programs that blend imperative control flow with soft logic operators capable of reasoning over VLM-generated uncertainty. Operating in a training-free manner, NePTune, with a modular design, decouples perception from reasoning, yet its differentiable operations support fine-tuning. We evaluate NePTune on multiple visual reasoning benchmarks and various domains, utilizing adversarial tests, and demonstrate a significant improvement over strong base models, as well as its effective compositional generalization and adaptation capabilities in novel environments.