Neural algorithmic reasoning has recently emerged as a popular research direction. It aims to train neural networks to mimic the step-by-step behavior of classical rule-based algorithms. More specifically, the execution of such algorithms can be abstracted as a sequence of states, where each state represents the intermediate outcome after an execution step. The training objective is to generate state sequences that replicate the underlying algorithmic process. A common framework for this task adopts an ``encoder-processor-decoder'' architecture, where the encoder learns representations of states, the processor simulates algorithmic steps, and the decoder reconstructs output states. While prior work has primarily focused on improving the processor, the role of the encoder in representation learning has received little attention. Most existing methods rely on simple MLP encoders, raising the question of whether such representations are sufficiently informative for supporting algorithmic reasoning. This paper investigates how to improve encoder representations for neural algorithmic reasoning. We propose a reconstruction module that aims to recover the input state from its encoded representation. This auxiliary reconstruction task encourages the encoder to retain critical information about the input. We demonstrate that incorporating this task during training improves the performance of existing neural architectures on standard benchmarks. Furthermore, we observe that current encoders often underutilize the correlations among features within a state. To address this, we draw inspiration from self-supervised learning and design an enhanced variant of the auxiliary task that encourages the encoder to capture intra-state feature dependencies. Experimental results show that our method enables the encoder to learn richer representations, thereby enhancing the performance of existing processors on algorithmic reasoning tasks.

Autoformalization aims to bridge the gap between human mathematical intuition and formal proof by automating the translation of informal reasoning into machine-verifiable languages.Despite significant breakthroughs catalyzed by Large Language Models (LLMs), autoformalizing Combinatorics remains a formidable challenge due to its intricate structural dependencies and the severe scarcity of high-quality formal datasets.To address these challenges, we propose SAIR-Comb, a Structure-Aware Iterative Refinement framework for Combinatorics powered by Lean 4 and LLMs.SAIR-Comb employs a multi-stage pipeline: first, it performs data augmentation and refinement by rectifying syntactic, semantic, and structural errors, guided by a curated manual combinatorics dataset.The model then undergoes a two-stage training regime: expert iteration with syntactic grounding, followed by reinforcement learning (RL) to align formal reasoning trajectories.Furthermore, we introduce Structural Consistency-a rigorous new metric designed to expose formalizing failures that elude traditional semantic-only evaluations.Experiments demonstrate that SAIR-Comb achieves strong performance on the specialized CombiBench while remaining highly competitive on general-domain benchmarks, including PutnamBench and ProverBench.

Abstract Safe controller synthesis with formal guarantees is widely employed in safety-critical systems. However, existing controller synthesis methods are subject to significant limitations in scalability and efficiency. This paper presents a novel controller incremental synthesis framework guided by barrier certificates (BCs), thereby generating a safe controller with BC verification. To enhance verification efficiency, we construct a learning-enabled polynomial BC combined with efficient post-verification, which is transformed into smaller-scale linear Programming (LP) subproblems for feasibility determination. Furthermore, we have implemented a tool called ISafeC and evaluated its performance over a set of benchmark examples. The comparative experimental results demonstrate the effectiveness and efficiency of our approach.

Safe controller synthesis is crucial for safety-critical applications. This paper presents a novel reinforcement learning approach to synthesize safe controllers for NN-controlled systems. The core idea leverages an iterative scheme that combines controller learning with neural barrier certificate (BC) verification, ultimately producing a provably safe deep neural network (DNN) controller with formal safety guarantees. The process begins by pre-training a well-performing DNN controller as an “oracle” via deep reinforcement learning (DRL). To formally verify the safety properties of the closed-loop system under the base controller, we devise a formal verification procedure that approximates the DNN controller using polynomial inclusion, followed by synthesizing neural BCs via sum-of-squares (SOS) relaxation. In cases where the base controller is insufficient to yield a real BC, the current spurious BC is incorporated as an additional penalty term to reshape the RL reward function, guiding the iterative refinement for new controllers. We implement an automated tool, NBCRL, and experimental results demonstrate the benefits of our method in terms of efficiency and scalability even for a nonlinear system with dimension up to 12.

Automated Theorem Proving is an important and challenging task.Although large language models (LLMs) have demonstrated remarkable potential in mathematical reasoning, their performance in formal theorem proving remains constrained by the scarcity of high-quality supervised fine-tuning (SFT) data.To address this limitation, we propose a Quality-Driven Theorem Synthesis method (QDTSynth) in Lean4.During the statement synthesis, we enhance Monte Carlo Tree Search (MCTS) with an adaptive adjustment mechanism that dynamically optimizes the search strategy based on the synthesis of statements.In addition, we propose diversity screening and the selfassessment method to select theorems that exhibit both diversity and high quality from the initially synthetic statements, enabling the synthesis of a high-quality Lean4 theorem dataset.After fine-tuning three open-source large language models on our synthetic dataset, experiments on the miniF2F benchmark demonstrate that QDTSynth significantly improves the performance of various open-source LLMs in theorem proving tasks.Our work offers a promising new direction for the future synthesis of highquality formal mathematical theorems.

Polynomial inequality proving is fundamental to many mathematical disciplines and finds wide applications in diverse fields. Current traditional algebraic methods are based on searching for a polynomial positive definite representation over a set of basis. However, these methods are limited by truncation degree. To address this issue, this paper proposes an approach based on reinforcement learning to find a Krivine-basis representation for proving polynomial inequalities. Specifically, we formulate the inequality proving problem as a linear programming (LP) problem and encode it as a basis selection problem using reinforcement learning (RL), achieving a non-negative Krivine basis. Moreover, a fast multivariate polynomial multiplication method based on Fast Fourier Transform (FFT) is employed to enhance the efficiency of action space search. Furthermore, we have implemented a tool called APPIRL (Automated Proof of Polynomial Inequalities via Reinforcement Learning). Experimental evaluation on benchmark problems demonstrates the feasibility and effectiveness of our approach. In addition, APPIRL has been successfully applied to solve the maximum stable set problem.

Polynomial Lyapunov function $\mathcal{V}({\mathbf{x}})$ provides mathematically rigorous that converts stability analysis into efficiently solvable optimization problem. Traditional numerical methods rely on user-defined templates, while emerging neural $\mathcal{V}({\mathbf{x}})$ offer flexibility but exhibit poor generalization yield from naive Square NNs. In this paper, we propose a novel learning-enabled polynomial $\mathcal{V}({\mathbf{x}})$ synthesis approach, where an automated machine learning process guided by goal-oriented sampling to fit candidate $\mathcal{V}({\mathbf{x}})$ which naturally compatible with the sum-of-squares (SOS) soundness verification. The framework is structured as an iterative loop between a Learner and a Verifier, where the Learner trains expressive polynomial $\mathcal{V}({\mathbf{x}})$ network via polynomial expansions, while the Verifier encodes learned candidates with SOS constraints to identify a real $\mathcal{V}({\mathbf{x}})$ by solving LMI feasibility test problems. The entire procedure is driven by a high-accuracy counterexample guidance technique to further enhance efficiency. Experimental results demonstrate that our approach outperforms both SMT-based polynomial neural Lyapunov function synthesis and traditional SOS method.

The design of controllers for safety-critical systems is an important research issue. Especially, the generation of controllers with formal safety guarantees is a challenging problem. Recently, for safety objectives of various system control tasks, machine learning technologies have been used to achieve ideal training and simulation performance, but formal guarantees are still lacking. This paper takes advantages of learning technology to assist safe controller synthesis with formal guarantees. On the one hand, the generation of verifiable safe controllers is aided by reinforcement learning; on the other hand, a set of barrier certificates (BC), i.e. a vector BC, is synthesized with the aid of deep learning to certify the safety of synthesized controllers. Vector BCs are more expressive than the conventional single BCs for safety verification. Compared with the existing work on vector BC generation, our method has two advantages: first, our method verifies a learned candidate vector BC, rather than directly generating a verified one, and thus has low computational complexity; second, the existing method has made relaxations to the non-convex vector BC constraints, which reduced the feasible region of solutions, while our method can deal with the original constraints. Furthermore, experiments fully demonstrate the effectiveness of our method on a series of benchmarks.

Controller synthesis for nonlinear systems is an important research issue. Deep Neural Network (DNN) control policies obtained through reinforcement learning (RL), though exhibiting good performance in simulations, cannot be applied to safety-critical systems for lack of formal guarantee. To address this, this paper considers fully utilizing the advantages of RL for complex control tasks to obtain a well-performing DNN controller. Then, using PAC (Probably Approximately Correct) techniques, a polynomial surrogate controller with probabilistically controllable approximation error is obtained. Finally, the safety of the control system under the designed polynomial controller is verified using barrier certificate generation. Experiments demonstrate the effectiveness of our method in generating controllers with safety guarantees for systems with high dimensions and degrees.

There is a pressing need to ensure the safety of closed-loop systems with neural network controllers, as they are often incorporated into safety-critical applications. To address this issue, we propose a novel approach for generating barrier certificates, which combines counterexample-guided learning with efficient Sum-Of-Squares (SOS) based verification. By leveraging barrier certificate candidates obtained from the learning phase, our proposed method offers an efficient verification procedure that solves three Linear Matrix Inequality (LMI) constraint feasibility testing problems, instead of relying on an SMT solver to verify the barrier certificate conditions. We conduct comparison experiments on a set of benchmarks, demonstrating the advantages of our method in terms of efficiency and scalability, which enable effective verification of high-dimensional systems.

Neural algorithmic reasoning is an emerging area of machine learning that focuses on building neural networks capable of solving complex algorithmic tasks. Recent advancements predominantly follow the standard supervised learning paradigm -- feeding an individual problem instance into the network each time and training it to approximate the execution steps of a classical algorithm. We challenge this mode and propose a novel open-book learning framework. In this framework, whether during training or testing, the network can access and utilize all instances in the training dataset when reasoning for a given instance. Empirical evaluation is conducted on the challenging CLRS Algorithmic Reasoning Benchmark, which consists of 30 diverse algorithmic tasks. Our open-book learning framework exhibits a significant enhancement in neural reasoning capabilities. Further, we notice that there is recent literature suggesting that multi-task training on CLRS can improve the reasoning accuracy of certain tasks, implying intrinsic connections between different algorithmic tasks. We delve into this direction via the open-book framework. When the network reasons for a specific task, we enable it to aggregate information from training instances of other tasks in an attention-based manner. We show that this open-book attention mechanism offers insights into the inherent relationships among various tasks in the benchmark and provides a robust tool for interpretable multi-task training.

This article presents a novel approach to the safety verification of hybrid systems by synthesizing neural barrier certificates (BCs) via counterexample-guided neural network (NN) learning combined with sum-of-square (SOS)-based verification. We learn more easily verifiable BCs with NN polynomial expansions in a high-accuracy counterexamples guided framework. By leveraging the polynomial candidates yielded from the learning phase, we reformulate the identification of real BCs as convex linear matrix inequality (LMI) feasibility testing problems, instead of directly solving the inherently NP-hard nonconvex bilinear matrix inequality (BMI) problems associated with SOS-based BC generation. Furthermore, we decompose the large SOS verification programming into several manageable subprogrammings. Benefiting from the efficiency and scalability advantages, our approach can synthesize BCs not amenable to existing methods and handle more general hybrid systems.

Bayesian neural networks (BNNs) retain NN structures with a probability distribution placed over their weights. With the introduced uncertainties and redundancies, BNNs are proper choices of robust controllers for safety-critical control systems. This paper considers the problem of verifying the safety of nonlinear closed-loop systems with BNN controllers over unbounded-time horizon. In essence, we compute a safe weight set such that as long as the BNN controller is always applied with weights sampled from the safe weight set, the controlled system is guaranteed to be safe. We propose a novel two-phase method for the safe weight set computation. First, we construct a reference safe control set that constraints the control inputs, through polynomial approximation to the BNN controller followed by polynomial-optimization-based barrier certificate generation. Then, the computation of safe weight set is reduced to a range inclusion problem of the BNN on the system domain w.r.t. the safe control set, which can be solved incrementally and the set of safe weights can be extracted. Compared with the existing method based on invariant learning and mixed-integer linear programming, we could compute safe weight sets with larger radii on a series of linear benchmarks. Moreover, experiments on a series of widely used nonlinear control tasks show that our method can synthesize large safe weight sets with probability measure as high as 95% even for a large-scale system of dimension 7.

Abstract There is a pressing need for learning controllers to endow systems with properties of safety and goal-reaching, which are crucial for many safety-critical systems. Reinforcement learning (RL) has been deployed successfully to synthesize controllers from user-defined reward functions encoding desired system requirements. However, it remains a significant challenge in synthesizing provably correct controllers with safety and goal-reaching requirements. To address this issue, we try to design a special hybrid polynomial-DNN controller which is easy to verify without losing its expressiveness and flexibility. This paper proposes a novel method to synthesize such a hybrid controller based on RL, low-degree polynomial fitting and knowledge distillation. It also gives a computational approach, by building and solving a constrained optimization problem coming from verification conditions to produce barrier certificates and Lyapunov-like functions, which can guarantee every trajectory from the initial set of the system with the resulted controller satisfies the given safety and goal-reaching requirements. We evaluate the proposed hybrid controller synthesis method on a set of benchmark examples, including several high-dimensional systems. The results validate the effectiveness and applicability of our approach.

In recent years, there has been an increasing demand for real-time super-resolution networks on mobile devices. To address this issue, many lightweight super-resolution models have been proposed. However, these models still contain time-consuming components that increase inference latency, limiting their real-world applications on mobile devices. In this paper, we propose a novel model for single-image super-resolution based on Equivalent Transformation and Dual Stream network construction (ETDS). ET method is proposed to transform time-consuming operators into time-friendly operations, such as convolution and ReLU, on mobile devices. Then, a dual stream network is designed to alleviate redundant parameters resulting from the use of ET and enhance the feature extraction ability. Taking full advantage of the advance of ET and the dual stream network structure, we develop the efficient SR model ETDS for mobile devices. The experimental results demonstrate that our ETDS achieves superior inference speed and reconstruction quality compared to previous lightweight SR methods on mobile devices. The code is available at https://github.com/ECNUSR/ETDS.

There is a pressing need to synthesize provable safety controllers for nonlinear systems as they are embedded in many safety-critical applications. In this paper, we propose a safe Meta Reinforcement Learning (Meta-RL) approach to synthesize deep neural network (DNN) controllers for nonlinear systems subject to safety constraints. Our approach incorporates two phases: Meta-RL for training the controller network, and formal safety verification based on polynomial optimization solving. In the training phase, we provide a training framework which pre-trains a unified meta-initial controller for control systems by meta-learning. An important benefit of the proposed Meta-RL approach lies in that it is much more effective and succeeds in more controller training tasks compared with existing typical RL methods, e.g., Deep Deterministic Policy Gradient (DDPG). To formally verify the safety properties of the closed-loop system with the learned controller, we develop a verification procedure by using polynomial inclusion computation in combination with barrier certificate generation. Experiments on a set of benchmarks, including systems with dimension up to 12, demonstrate the effectiveness and applicability of our method.

Blind super-resolution, different from conventional non-blind super-resolution based on the assumption of fixed degradation, handles various unknown Gaussian blur kernels, and thus is closer to real-world application. The accuracy of kernel estimation and deconvolution directly influences the performance of overall super-resolution results, but recent works usually introduce artifacts during the process. In this paper, we propose our methods of a more accurate kernel estimation module (KEM) and deconvolution module (DM). Additionally, KEM and DM are embedded in kernel estimation and deconvolution structure (KEDS), which improves the results to a large extent once combined with non-blind networks.

Deep convolutional neural networks (CNNs) have achieved unprecedented success in single image super-resolution over the past few years. Meanwhile, there is an increasing demand for single image super-resolution with arbitrary scale factors in real-world scenarios. Many approaches adopt scale-specific multi-path learning to cope with multi-scale super-resolution with a single network. However, these methods require a large number of parameters. To achieve a better balance between the reconstruction quality and parameter amounts, we proposes a learnable interpolation method that leverages the advantages of neural networks and interpolation methods to tackle the scale-arbitrary super-resolution task. The scale factor is treated as a function parameter for generating the kernel weights for the learnable interpolation. We demonstrate that the learnable interpolation builds a bridge between neural networks and traditional interpolation methods. Experiments show that the proposed learnable interpolation requires much fewer parameters and outperforms state-of-the-art super-resolution methods.

With the increasing availability of devices that support ultra-high-definition (UHD) images, Single Image Super Resolution (SISR) has emerged as a crucial problem in the field of computer vision. In recent years, CNN-based super resolution approaches have made significant advances, producing high-quality upscaled images. However, these methods can be computationally and memory intensive, making them impractical for real-time applications such as upscaling to UHD images. The performance and reconstruction quality may suffer due to the complexity and diversity of larger image content. Therefore, there is a need to develop efficient super resolution approaches that can meet the demands of processing high-resolution images. In this paper, we propose a simple network named PCEVAnet by constructing the PCEVA block, which leverages Partial Convolution and Efficient Variance Attention. Partial Convolution is employed to streamline the feature extraction process by minimizing memory access. And Efficient Variance Attention (EVA) captures the high-frequency information and long-range dependency via the variance and max pooling. We conduct extensive experiments to demonstrate that our model achieves a better trade-off between performance and actual running time than previous methods.

This paper presents a novel approach to safety verification based on neural barrier certificates synthesis for continuous dynamical systems. We construct the synthesis framework as an inductive loop between a Learner and a Verifier based on barrier certificate learning and counterexample guidance. Compared with the counterexample-guided verification method based on the SMT solver, we design and learn neural barrier functions with special structure, and use the special form to convert the counterexample generation into a polynomial optimization problem for obtaining the optimal counterexample. In the verification phase, the task of identifying the real barrier certificate can be tackled by solving the Linear Matrix Inequalities (LMI) feasibility problem, which is efficient and makes the proposed method formally sound. The experimental results demonstrate that our approach is more effective and practical than the traditional SOS-based barrier certificates synthesis and the state-of-the-art neural barrier certificates learning approach.

Adversarial training is an efficacious defense approach to protect classification model against adversarial attacks. In this paper, we reveal that a significant difference exists between the feature map of the original sample and that of its corresponding adversarial version. Based on this main insight, we propose a novel robust training on feature-based adversarial examples approach called FPAT, where training examples are generated by maximizing the loss function between the clean and the adversarial feature maps. We show via extensive experiments on MNIST, SVHN and CIFAR-10, that our proposed method is as effective as the state-of-the-art robust training methods. Especially, when the adversarial perturbation is of a large radius or the number of adversarial steps of training samples is small, FPAT achieves leading robustness.

Abstract In this paper, we propose a safe reinforcement learning approach to synthesize deep neural network (DNN) controllers for nonlinear systems subject to safety constraints. The proposed approach employs an iterative scheme where alearnerand averifierinteract to synthesize safe DNN controllers. Thelearnertrains a DNN controller via deep reinforcement learning, and theverifiercertifies the learned controller through computing a maximal safe initial region and its corresponding barrier certificate, based on polynomial abstraction and bilinear matrix inequalities solving. Compared with the existing verification-in-the-loop synthesis methods, our iterative framework is a sequential synthesis scheme of controllers and barrier certificates, which can learn safe controllers with adaptive barrier certificates rather than user-defined ones. We implement the tool SRLBC and evaluate its performance over a set of benchmark examples. The experimental results demonstrate that our approach efficiently synthesizes safe DNN controllers even for a nonlinear system with dimension up to 12.

The paper presents a barrier certificate based approach to verifying safety properties of closed-loop systems using neural networks as controllers. It deals with the verification problem in the infinite time horizon and exploits the approximated system of the original one to synthesize the candidate barrier certificates, where the behavior of a neural network controller is approximated by a polynomial with a bounded error. Satisfiability Modulo Theories solvers are then utilized to identify real barrier certificates from those candidates. As a barrier certificate can separate the over-approximation of the reachable set from the unsafe region, once it is constructed, the safety property gets proved. We show the advantage of our approach in barrier certificates synthesis by comparing it with the state-of-the-art work on a set of benchmarks.

Barrier certificates provide safety guarantees for hybrid systems. In this paper, we propose a novel approach to synthesizing neural networks as barrier certificates. Candidate networks are trained from a special structure: ReLU neural networks consisting of two hidden layers. Then, the problem of identifying real barrier certificates from candidates is transformed into a group of mixed integer linear programming problems and a mixed integer quadratically constrained problem. Taking full advantage of the recent advance in optimization, barrier certificates validation can be performed effectively. We implement the tool SyntheBC and evaluate its performance over 3 hybrid systems and 8 continuous systems up to 12-dimensional state space. The experimental results show that our method is more scalable and effective than the classical polynomial barrier certificate method and the existing neural network based method.

Barrier certificates generation is widely used in verifying safety properties of hybrid systems because of the relatively low computational complexity it costs. Under sum of squares (SOS) relaxation, the problem of barrier certificate generation is equivalent to that of solving a bilinear matrix inequality (BMI) with a particular type. The paper reveals the special feature of the problem, and adopts it to build a novel computational method. The proposed method introduces a sequential iterative scheme that is able to find analytical solutions, rather than the nonlinear solving procedure to produce numerical solutions used by general BMI solvers and thus is more efficient than them. In addition, different from popular LMI solving based methods, it does not make the verification conditions more conservative, and thus reduces the risk of missing feasible solutions. Benefitting from these two appealing features, it can produce barrier certificates not amenable to existing methods, which is supported by a complexity analysis as well as the experiment on some benchmarks.

There is a pressing need to verify robustness of classification deep neural networks (CDNNs) as they are embedded in many safety-critical applications. Existing robustness verification approaches rely on computing the over-approximation of the output set, and can hardly scale up to practical CDNNs, as the result of error accumulation accompanied with approximation. In this paper, we develop a novel method for robustness verification of CDNNs with sigmoid activation functions. It converts the robustness verification problem into an equivalent problem of inspecting the most suspected point in the input region which constitutes a nonlinear optimization problem. To make it amenable, by relaxing the nonlinear constraints into the linear inclusions, it is further refined as a linear programming problem. We conduct comparison experiments on a few CDNNs trained for classifying images in some state-of-the-art benchmarks, showing our advantages of precision and scalability that enable effective verification of practical CDNNs.

In this paper, we present a study on building a special SAARA (Self-Aware Automated Reasoning Agent) system for solving Freudenthal's Sum and Product puzzle, aimed to train the "self-reflection" and "subjective experience" abilities as in the Three Wise Men test performed by the Nao robots in Rensselaer Polytechnic Institute in July 2015. We show the dynamic evolution of corresponding knowledge sets in the automated reasoning process for the Sum and Product puzzle.

An algorithm for interpolating a polynomial f from evaluation points whose running time depends on the sparsity t of the polynomial when it is represented as a sum of t Chebyshev Polynomials of the First Kind with non-zero scalar coefficients is given by Lakshman Y. N. and Saunders [SIAM J. Comput., vol. 24, nr. 2 (1995)]; Kaltofen and Lee [JSC, vol. 36, nr. 3--4 (2003)] analyze a randomized early termination version which computes the sparsity t. Those algorithms mirror Prony's algorithm for the standard power basis to the Chebyshev Basis of the First Kind. An alternate algorithm by Arnold's and Kaltofen's [Proc. ISSAC 2015, Sec. 4] uses Prony's original algorithm for standard power terms. Here we give sparse interpolation algorithms for generalized Chebyshev polynomials, which include the Chebyshev Bases of the Second, Third and Fourth Kind. Our algorithms also reduce to Prony's algorithm. If given on input a bound B >= t for the sparsity, our new algorithms deterministically recover the sparse representation in the First, Second, Third and Fourth Kind Chebyshev representation from exactly t + B evaluations. Finally, we generalize our algorithms to bases whose Chebyshev recurrences have parametric scalars. We also show how to compute those parameter values which optimize the sparsity of the representation in the corresponding basis, similar to computing a sparsest shift.

The paper investigates a notion of sub asynchronous pi-calculus in asynchronous communication. The emphasises of the research are the basic operation and encoding theory of this novel subcalculus. We focus on behavioural equivalences, accurately on barbed congruence and bisimilarity. The congruence of bisimilarity and characterisation of barbed congruence in sub asynchronous pi-calculus are novel and directly proved. The encoding from pi-calculus to sub asynchronous pi-calculus is validated to be complete and sound. Consequently, the results in this paper bring out theoretical foundations for constructing fully abstract encodings from synchronous to asynchronous.

In safety verification of hybrid systems, barrier certificates are generated by solving the verification conditions derived from non-negative representations of different types. This paper presents a new computational method, sequential linear programming projection, for directly solving the set of verification conditions represented by the Krivine-Vasilescu-Handelman's positivstellensatz. The key idea is to decompose it into two successive optimization problems that refine the desired barrier certificate and those undetermined multipliers, respectively, and solve it in an iterative scheme. The most important benefit of the proposed approach lies in that it is much more effective than the LP relaxation method in producing real barrier certificates, and possesses a much lower computational complexity than the popular sum of square relaxation methods, which is demonstrated by the theoretical analysis on complexity and the experiment on a set of examples gathered from the literature.

Hybrid systems with non-polynomial components are widely used in modeling safety critical applications. Due to the complexity arisen from the non-polynomial expression, safety verification for such systems presents a grand challenge. In this paper, we present a new general approach to synthesizing rational invariants for safety verification of non-polynomial hybrid systems (NPHSs). Through system transformation and rational approximation, a NPHS is transformed into an over-approximate hybrid system in rational form. Then, for the over-approximate rational hybrid system, the proposed framework exploits a symbolic-numeric computation method to generate its exact rational invariants, which guarantees the safety property of the original NPHS. The test results show that the rational invariants yield better performances than those obtained from polynomial invariants.

The problem of probabilistic safety verification of stochastic hybrid systems is to check whether the probability that a given system will reach an unsafe region from certain initial states can be bounded by some given probability threshold. The paper considers stochastic hybrid systems where the behavior is governed by polynomial equalities and inequalities, as for usual hybrid systems, but the initial states follow some stochastic distributions. It proposes a new barrier certificate based method for probabilistic safety verification which guarantees the absolute safety in a infinite time horizon that is beyond the reach of existing techniques using either statistical model checking or probabilistic reachable set computation. It also gives a novel computational approach, by building and solving a constrained optimization problem coming from verification conditions of barrier certificates, to compute the lower bound on safety probabilities which can be compared with the given threshold. Experimental evidence is provided demonstrating the applicability of our approach on several benchmarks.

Benefit from less computational difficulty, barrier certificate based method has attracted much attention in safety verification of hybrid systems. Barrier certificates are inherent existences of a hybrid system and may have different types. A set of well-defined verification conditions is a prerequisite for successfully identifying barrier certificates of a specific type. Therefore, how to define verification conditions that can identify barrier certificates invisible to existing conditions becomes an essential problem in barrier certificate based verification. This paper proposes a set of verification conditions that helps to construct a new type of barrier certificate, namely, the Darboux-type barrier certificate made of Darboux polynomial. The proposed verification conditions provide powerful aids in non-linear hybrid system verification as the Darboux-type barrier certificates can verify systems that may not be settled by existing verification conditions.

In this article, we address the problem of safety verification of nonlinear hybrid systems. A hybrid symbolic-numeric method is presented to compute exact inequality invariants of hybrid systems efficiently. Some numerical invariants of a hybrid system can be obtained by solving a bilinear SOS programming via the PENBMI solver or iterative method, then the modified Newton refinement and rational vector recovery techniques are applied to obtain exact polynomial invariants with rational coefficients, which exactly satisfy the conditions of invariants. Experiments on some benchmarks are given to illustrate the efficiency of our algorithm.

In [Kaltofen and Yang, Proc. ISSAC 2013] we have generalized algebraic error-correcting decoding to multivariate sparse rational function interpolation from evaluations that can be numerically inaccurate and where several evaluations can have severe errors ("outliers"). Here we present a different algorithm that can interpolate a sparse multivariate rational function from evaluations where the error rate is 1/q for any q > 2, which our ISSAC 2013 algorithm could not handle. When implemented as a numerical algorithm we can, for instance, reconstruct a fraction of trinomials of degree 15 in 50 variables with non-outlier evaluations of relative noise as large as 10-7 and where as much as 1/4 of the 14717 evaluations are outliers with relative error as small as 0.01 (large outliers are easily located by our method).

Error-correcting decoding is generalized to multivariate sparse rational function recovery from evaluations that can be numerically inaccurate and where several evaluations can have severe errors ("outliers"). The generalization of the Berlekamp-Welch decoder to exact Cauchy interpolation of univariate rational functions from values with faults is by Kaltofen and Pernet in 2012. We give a different univariate solution based on structured linear algebra that yields a stable decoder with floating point arithmetic. Our multivariate polynomial and rational function interpolation algorithm combines Zippel's symbolic sparse polynomial interpolation technique [Ph.D. Thesis MIT 1979] with the numeric algorithm by Kaltofen, Yang, and Zhi [Proc. SNC 2007], and removes outliers ("cleans up data") through techniques from error correcting codes. Our multivariate algorithm can build a sparse model from a number of evaluations that is linear in the sparsity of the model.

In this paper, we propose two algorithms for verifying the existence of real solutions of positive-dimensional polynomial systems. The first one is based on the critical point method and the homotopy continuation method. It targets for verifying the existence of real roots on each connected component of an algebraic variety V ∩ Rn defined by polynomial equations. The second one is based on the low-rank moment matrix completion method and aims for verifying the existence of at least one real roots on V ∩ Rn. Combined both algorithms with the verification algorithms for zero-dimensional polynomial systems, we are able to find verified real solutions of positive-dimensional polynomial systems very efficiently for a large set of examples.

The problem of blind image deconvolution can be solved by computing approximate greatest common divisors (GCD) of polynomials. The bivariate polynomials corresponding to the z-transforms of several blurred images have an approximate GCD corresponding to the z-transform of the original image. Since blurring functions as cofactors have very low degree in general, this GCD will be of high degree. On the other hand, if we only have one blurred image and want to identify the original scene, the blurred image can be partitioned such that each part completely contains the blurring function, hence the blurring function becomes the GCD which is of low degree. Therefore, we design a specialized algorithm for computing GCDs of polynomials to recover true images in two different cases. The new algorithm is based on the fast GCD algorithm for univariate polynomials and the Fast Fourier Transform (FFT) algorithm. The complexity of our specialized algorithm for identifying both the true image and the blurring functions from blurred images of size n x n is O(n2 log(n)) in the case of blurring functions of very low degree. The algorithm has been implemented in Maple and can extract true images of hundreds by hundreds pixel images from blurred images in a few seconds.

We generalize the technique by Peyrl and Parillo [Proc. SNC 2007] to computing lower bound certificates for several well-known factorization problems in hybrid symbolic-numeric computation. The idea is to transform a numerical sum-of-squares (SOS) representation of a positive polynomial into an exact rational identity. Our algorithms successfully certify accurate rational lower bounds near the irrational global optima for benchmark approximate polynomial greatest common divisors and multivariate polynomial irreducibility radii from the literature, and factor coefficient bounds in the setting of a model problem by Rump (up to n = 14, factor degree = 13.

The black box algorithm for separating the numerator from the denominator of a multivariate rational function can be combined with sparse multivariate polynomial interpolation algorithms to interpolate a sparse rational function. domization and early termination strategies are exploited to minimize the number of black box evaluations. In addition, rational number coefficients are recovered from modular images by rational vector recovery. The need for separate numerator and denominator size bounds is avoided via correction, and the modulus is minimized by use of lattice basis reduction, a process that can be applied to sparse rational function vector recovery itself. Finally, one can deploy sparse rational function interpolation algorithm in the hybrid symbolic-numeric setting when the black box for the function returns real and complex values with noise. We present and analyze five new algorithms for the above problems and demonstrate their effectiveness on a mark implementation.

We consider the problem of computing minimal real or complex deformations to the coefficients in a list of relatively prime real or complex multivariate polynomials such that the deformed polynomials have a greatest common divisor (GCD) of at least a given degree k. In addition, we restrict the deformed coefficients by a given set of linear constraints, thus introducing the linearly constrained approximate GCD problem. We present an algorithm based on a version of the structured total least norm (STLN) method and demonstrate on a diverse set of benchmark polynomials that the algorithm in practice computes globally minimal approximations. As an application of the linearly constrained approximate GCD problem we present an STLN-based method that computes a real or complex polynomial the nearest real or complex polynomial that has a root of multiplicity at least k. We demonstrate that the algorithm in practice computes on the benchmark polynomials given in the literature the known globally optimal nearest singular polynomials. Our algorithms can handle, via randomized preconditioning, the difficult case when the nearest solution to a list of real input polynomials actually has non-real complex coefficients.

The input to our algorithm is a multivariate polynomial, whose complex rational coefficients are considered imprecise with an unknown error that causes f to be irreducible over the complex numbers C. We seek to perturb the coefficients by a small quantitity such that the resulting polynomial factors over C. Ideally, one would like to minimize the perturbation in some selected distance measure, but no efficient algorithm for that is known. We give a numerical multivariate greatest common divisor algorithm and use it on a numerical variant of algorithms by W. M. Ruppert and S. Gao. Our numerical factorizer makes repeated use of singular value decompositions. We demonstrate on a significant body of experimental data that our algorithm is practical and can find factorizable polynomials within a distance that is about the same in relative magnitude as the input error, even when the relative error in the input is substantial (10-3).