skip to main content

Attention:

The NSF Public Access Repository (NSF-PAR) system and access will be unavailable from 11:00 PM ET on Thursday, October 10 until 2:00 AM ET on Friday, October 11 due to maintenance. We apologize for the inconvenience.


Search for: All records

Creators/Authors contains: "Shoukry, Yasser"

Note: When clicking on a Digital Object Identifier (DOI) number, you will be taken to an external site maintained by the publisher. Some full text articles may not yet be available without a charge during the embargo (administrative interval).
What is a DOI Number?

Some links on this page may take you to non-federal websites. Their policies may differ from this site.

  1. Constraints solvers play a significant role in the analysis, synthesis, and formal verification of complex cyber-physical systems. In this article, we study the problem of designing a scalable constraints solver for an important class of constraints named polynomial constraint inequalities (also known as nonlinear real arithmetic theory). In this article, we introduce a solver named PolyARBerNN that uses convex polynomials as abstractions for highly nonlinears polynomials. Such abstractions were previously shown to be powerful to prune the search space and restrict the usage of sound and complete solvers to small search spaces. Compared with the previous efforts on using convex abstractions, PolyARBerNN provides three main contributions namely (i) a neural network guided abstraction refinement procedure that helps selecting the right abstraction out of a set of pre-defined abstractions, (ii) a Bernstein polynomial-based search space pruning mechanism that can be used to compute tight estimates of the polynomial maximum and minimum values which can be used as an additional abstraction of the polynomials, and (iii) an optimizer that transforms polynomial objective functions into polynomial constraints (on the gradient of the objective function) whose solutions are guaranteed to be close to the global optima. These enhancements together allowed the PolyARBerNN solver to solve complex instances and scales more favorably compared to the state-of-the-art nonlinear real arithmetic solvers while maintaining the soundness and completeness of the resulting solver. In particular, our test benches show that PolyARBerNN achieved 100X speedup compared with Z3 8.9, Yices 2.6, and PVS (a solver that uses Bernstein expansion to solve multivariate polynomial constraints) on a variety of standard test benches. Finally, we implemented an optimizer called PolyAROpt that uses PolyARBerNN to solve constrained polynomial optimization problems. Numerical results show that PolyAROpt is able to solve high-dimensional and high order polynomial optimization problems with higher speed compared to the built-in optimizer in the Z3 8.9 solver. 
    more » « less
    Free, publicly-accessible full text available March 31, 2025
  2. Formal certification of Neural Networks (NNs) is crucial for ensuring their safety, fairness, and robustness. Unfortunately, on the one hand, sound and complete certification algorithms of ReLU-based NNs do not scale to large-scale NNs. On the other hand, incomplete certification algorithms are easier to compute, but they result in loose bounds that deteriorate with the depth of NN, which diminishes their effectiveness. In this paper, we ask the following question; can we replace the ReLU activation function with one that opens the door to incomplete certification algorithms that are easy to compute but can produce tight bounds on the NN's outputs? We introduce DeepBern-Nets, a class of NNs with activation functions based on Bernstein polynomials instead of the commonly used ReLU activation. Bernstein polynomials are smooth and differentiable functions with desirable properties such as the so-called range enclosure and subdivision properties. We design a novel Interval Bound Propagation (IBP) algorithm, called Bern-IBP, to efficiently compute tight bounds on DeepBern-Nets outputs. Our approach leverages the properties of Bernstein polynomials to improve the tractability of neural network certification tasks while maintaining the accuracy of the trained networks. We conduct experiments in adversarial robustness and reachability analysis settings to assess the effectiveness of the approach. Our proposed framework achieves high certified accuracy for adversarially-trained NNs, which is often a challenging task for certifiers of ReLU-based NNs. This work establishes Bernstein polynomial activation as a promising alternative for improving NN certification tasks across various NNs applications.

     
    more » « less
    Free, publicly-accessible full text available March 25, 2025
  3. Free, publicly-accessible full text available January 1, 2025
  4. Free, publicly-accessible full text available December 13, 2024
  5. Free, publicly-accessible full text available December 13, 2024
  6. To cut CO2emissions, we propose to directly convert shale gas into value-added products with a new H2/O2co-transport membrane (HOTM) reactor. A Multiphysics model has been built to simulate the membrane and the catalytic bed with parameters obtained from experimental validation. The model was used to compare C2 yield and CH4conversion rate between the membrane reactor and the state-of-the-art fixed-bed reactor with the same dimensions and operating conditions. The results indicate that (1) the membrane reactor is more efficient in consuming CH4for a given amount of fed O2. (2) The C2 selectivity of the membrane reactor is higher due to the gradual addition of O2into the reactor. (3) The current proposed membrane reactor can have a decent proton molar flux density but most of the proton molar flux will contribute to producing H2O on the feed side under the current operating conditions. The paper for the first-time projects the performance of the membrane reactor for combined H2O/H2removal and C2 production. It could be used as important guidance for experimentalists to design next generation natural gas conversion reactors.

     
    more » « less
  7. We consider the problem of whether a Neural Network (NN) model satisfies global individual fairness. Individual Fairness (defined in (Dwork et al. 2012)) suggests that similar individuals with respect to a certain task are to be treated similarly by the decision model. In this work, we have two main objectives. The first is to construct a verifier which checks whether the fairness property holds for a given NN in a classification task or provides a counterexample if it is violated, i.e., the model is fair if all similar individuals are classified the same, and unfair if a pair of similar individuals are classified differently. To that end, we construct a sound and complete verifier that verifies global individual fairness properties of ReLU NN classifiers using distance-based similarity metrics. The second objective of this paper is to provide a method for training provably fair NN classifiers from unfair (biased) data. We propose a fairness loss that can be used during training to enforce fair outcomes for similar individuals. We then provide provable bounds on the fairness of the resulting NN. We run experiments on commonly used fairness datasets that are publicly available and we show that global individual fairness can be improved by 96 % without a significant drop in test accuracy. 
    more » « less
  8. In this study, we simulated BZY electrolyte-supported proton-conducting solid oxide cell by coupling surface defect chemistry reaction with charged species transport. We validated the model parameters by concentration as a function of temperature, conductivity under dry and wet oxygen as a function of oxygen partial pressure and temperature. The results indicate that the high electron-hole mobility (diffusivity) is mainly responsible for the high leaking current under high temperatures. The Faradaic efficiency stays low or even negative under low operating voltage or high temperature and plateaus as the cell voltage increases. The model developed in this study is a useful tool to understand the leaking current in BZY electrolyte and provide design strategies to avoid/mitigate such significant inefficiency for water electrolysis operation. 
    more » « less