dataesr/scientific-paragraphs-categorization huggingface dataset:
✓ Non-integer computation × etc); and iv. so far, only integral types are allowed. A summary of the most relevant features and restrictions of CircGen can be found in Table  2. The fragment of C that we support is aligned with similar tools. Most of the limitations at this level are inherent to the problem of describing programs as (relatively small) Boolean circuits. Functions. The source C program can be structured in different functions, but the tool will force all function calls to be inlined (independently of the presence of the inline keyword in function headers). As a consequence, we exclude any form of recursion in source programs (either direct or indirect). In practical terms, we adapt the function inlining pass of CompCert, which refuses to inline any kind of recursive function (each time it inlines a function f, it removes f from the context).
These three sections of the RTL program are delimited by dummy external calls (to __circ-gen_fence); they block any optimization across these boundaries that could prevent the correct recognition of inputs and outputs in the next compilation pass. Loop unroll. The loop-elimination pass is split into two elementary transformations: i. one that unrolls the loop by an arbitrary number of iterations, but leaves the loop unchanged at the end; and ii. one that establishes that the loop kept after all the unrollings is indeed redundant (i. e. , that it is unreachable). By doing this, we simplify significantly the semantic preservation proof, since the first transformation follows directly from the operational semantics of loops and is always sound, independently of the number of unrolls. The second transformation can be seen as a specific instance of dead-code elimination.
We implement the first transformation as a new compiler pass in CompCert and prove its semantic preservation theorem. This pass is performed at the Cminor intermediate language since it has a unified treatment for all C loop constructors, but still retains enough structure in the loops to support a simple semantic preservation proof. The number of unfolds for each loop is received by the tool as external advice. For the second transformation we rely on the pre-existing dead code elimination pass of CompCert to remove the remaining loops that are kept after the unfolds. Note that dead code elimination is performed after loop unrolling, function inlining and constant propagation passes, which ensures that loops with simple control structure are successfully eliminated as dead-code (provided that sufficient large unroll estimates are given at the loop unroll pass; otherwise compilation will fail).
We have adopted Ordered-Reduced Binary Decision Trees  [23]  as canonical representatives of path-conditions, where nodes are tagged with propositional variables (branching points) and leaves are Boolean values. Figure  9  (left) shows the test program after the path-condition computation pass. Path-conditions are the guards shown at the end of each line (propositional variables are denoted by their index). From RTL to RTLC. The translation from RTL to RTLC amounts essentially to the computation of path-conditions for every instruction in the program. This computation is part of the RTL structural validation that occurs as the final pass of the compiler front-end component. This validation ensures that a Boolean circuit interpretation can be assigned to the RTL program, making it ready to be processed by the CircGen back-end.
An obvious topological constraint is imposed: the connector for a gate can only refer to wires appearing earlier in the circuit. Finally, we have a description of the outputs of the circuit (again, described by a connector). Figure  10  presents a circuit description for the example program. Handling of RTLC Memory Accesses. The main abstraction gap between SSA-RTLC and HLcirc is the use of memory. Recall that RTLC retains memory operations to access/update global variables and data stored on the stack. Hence, the translation into high-level circuits must keep track, at each program point, of which wires store the data for the relevant memory regions. To this end, we treat every memory region as a pool of wires, initialized in accordance with the original C program (lines 2-5 in Figure  10 , which hold the initial data of stack, a, b and result respectively).
This is indeed the main motivation for the constant-expansion pass mentioned earlier: memory accesses constitute the best example where the impact of unfolding constant alternatives can be significant. Reg-to-Wire Mapping and ϕ-node Placement. To finalize the translation from SSA-RTLC to HLcirc it now suffices to associate to each RTLC variable the correct number of wires and to insert explicit code to resolve ϕ-nodes. This transformation is justified via the facts that i. the SSA form ensures no cyclic dependencies in the wire definitions; and ii. that the explicit guards provided with ϕ-nodes naturally lead to a w-bit multiplexer (w being the bit-width of joined variables). This is clearly noted in lines 15-19 of Figure  10. Circuit generation. From a high-level circuit, the CircGen backend generates a Boolean circuit by obtaining instantiations of the high-level complex gates used in the HLcirc language from an external oracle, and expanding the entire circuit into Boolean gates.
A comparison of optimized CircGen with CBMC-GC shows that the two are relatively close for arithmetic operations, CMBC-GC is better in Hamming distance computations, and our tool is better in all programs that use arrays heavily, including the vanilla versions of tabled AES implementations. The global optimization passes are the subject of ongoing work. We do not envision any conceptual difficulty in verifying them, but they do imply reasonable effort to express cross-gate optimizations such as memoization and simplification. Indeed, early experiments reveal that these passes do exacerbate the memory usage of the compiler. The means that we likely will not be able to rely on the data structures made available by CompCert's infrastructure as we do in other passes (specifically, for Maps).
SFE SOFTWARE STACK EVALUATION In this section we present a performance evaluation of the entire SFE software stack based on FRESCO. The FRESCO framework is able to read circuit descriptions in the format produced by CircGen. We thus use the Boolean circuits generated in the micro-benchmarks reported in the previous section to feed two protocol suites supported by this framework. 17 The results are given in Table  4. The first protocol we test is the verified implementation of Yao's protocol described in Section 2, which has been integrated into FRESCO as a new protocol suite (shown in the table as Yao). The second is the Tiny Tables protocol of  [29] , which is provided in the vanilla distribution of FRESCO; this protocol operates in the preprocessing model, and includes XOR-specific optimizations.
High-assurance cryptography General-purpose tools. CryptoVerif  [19]  was among the first tools to support cryptographic security proofs in the computational model and it has been used for verifying primitives as well as protocols. More recently, Cadé and Blanchet  [24]  have complemented the work on CryptoVerif with a mechanism to generate functional code from CryptoVerif models and use it to generate a verified implementation of SSH. Swamy et al. [55]  build a type-based approach for reasoning about programs written in the typed functional programming language F ⋆. Bhargavan et al. [18]  subsequently use F ⋆ to develop highassurance implementations of TLS. Rastogi, Swamy and Hicks  [54]  also use F ⋆ as a host language for embedding Wysteria, a domainspecific language for multi-party computation.
Fairplay, Sharemind and TASTY are MPC frameworks alternative to FRESCO. Fairplay is a system originally developed to support two-party computation  [46]  and then extended to multiparty computation as FairplayMP  [15] : Fairplay implements a two party computation protocol in the manner suggested by Yao; FairplayMP is based on the Beaver-Micali-Rogaway protocol  [10]. Sharemind  [21]  is a secure service platform for data collection and analysis, employing a 3-party additive secret sharing scheme and provably secure protocols in the honest-but-curious security model with no more than one passively corrupted party. TASTY (Tool for Automating Secure Two-partY computations) is a tool suite addressing secure two-party computation in the semi-honest model  [37]  whose main feature is to allow the compilation and evaluation of functions using both garbled circuits and homomorphic encryption.
In this case we capture honest-butcurious (or semi-honest, or passive) adversaries. We consider each party's view of the protocol (typically containing its randomness and the list of messages exchanged during a run), and a notion of leakage for each party, modelling how much of that party's input may be leaked by the protocol execution (for example, its length). Informally, we say that such a protocol is secure if each party's view can be efficiently simulated using only its inputs, its outputs and precisely defined leakage about the other party's input. Formally, we express this security notion using two games (one for each party). We display one of them in Figure  12 , in the form of an EasyCrypt module. Note that modules are used to model games and experiments, but also schemes, oracles and adversaries.
Acknowledgments. This work is partially supported by  ONR  Grants  N000141210914  and  N000141512750 , by  Cátedra PT-FLAD em Smart Cities & Smart Governance , by  Fundação para a Ciência e a Tecnologia  grant  FCT-PD/BD/113967/2015 , by the  ERDF -European Regional Development Fund  through the  Operational Programme for Competitiveness and Internationalisation -COMPETE 2020 Programme  within project  «POCI-01-0145-FEDER-006961 », and by  National Funds through the Portuguese funding agency, FCT -Fundação para a Ciência e a Tecnologia  as part of project  «UID/EEA/50014/2013 ». The EasyCrypt definitions build on early work by  Guillaume Davy. We thank  Pierre-Yves Strub  for his role in the development of EasyCrypt.
The first algorithms implemented in this software relied on model linearisation to obtain an approximation of the likelihood, which cannot be computed easily in nonlinear mixed effect models. This approximation is then maximised through iterative Newton-Raphson minimisation, a general purpose algorithm involving the gradient of the function to be optimised. Different approximations to the likelihood have been proposed, including the first-order conditional method where the linearisation takes place around the current individual estimates at each iteration  (Lindstrom and Bates (1990) ). These estimation methods have also been implemented in mainstream statistical software such as SAS (proc NLMIXED, SAS Institute) and R (R Development Core  Team (2006) ), where the nlme (Pinheiro and  Bates (1995) ) library is now part of the base installation.
Over the past decade, new and powerful estimation algorithms have therefore been proposed to estimate the parameters of nonlinear mixed effect models  (Lavielle (2014) ). The alternative to model linearisation is to compute the likelihood through numerical or statistical approximations, to preserve the statistical properties of maximum likelihood estimators. An example is the Laplace approximation, which is equivalent to a one-point adaptive Gaussian quadrature, and has been implemented in NONMEM. In R, the lme4 library uses this approximation  (Bates, Maechler, and Bolker (2013) ) with a penalised least square approach for the estimation algorithm. A powerful alternative to gradient-based minimisation algorithms is the EM algorithm, also an iterative algorithm, which has been developed in the context of missing data  (Dempster, Laird, and Rubin (1977) ).
The Stochastic Approximation Expectation Maximization (SAEM) algorithm, combining a stochastic approximation to the likelihood with an EM algorithm, has proven very efficient for nonlinear mixed effect models, quickly converging to the maximum likelihood estimators  (Delyon, Lavielle, and Moulines (1999) ) and performing better than linearisation-based algorithms  (Girard and Mentré (2005) ). It has been implemented in the Monolix software  (Lavielle (2014) ), which has enjoyed increasingly widespread use over the last few years, more recently in the Statistics toolbox of MATLAB (nlmefitsa. m), and is also available in NONMEM version 7  (Boeckmann et al. (1994) ). In the present paper, we provide an implementation of the SAEM algorithm in the R software (R Development Core  Team (2006) ) through the saemix package.
Statistical models A typical longitudinal dataset consists of observations collected in N individuals (for instance, subjects in a clinical trial). We assume that n i observations y i = {y i1 ,. , y in i } have been collected in subject i, at design points x i = {x i1 ,. , x in i } (in a clinical trial, x will typically be time or doses). The statistical model for observation y ij is the following: y ij = f (ψ i , x ij ) + g(ψ i , σ, x ij ) ij (1) In Equation  1 , the function f represents the structural model, describing the evolution of the process being modelled, while the function g characterises the residual error model, more specifically its variance, and may depend on additional parameters σ. We assume that the variability between subjects is captured by the vector of individual parameters ψ i , and that the errors ij are random samples from the standard normal distribution, and are independent of the ψ i.
(1999) ). In practice, γ k is set equal to 1 during the first K 1 to let the algorithm explore the parameter space without memory and to converge quickly to a neighbourhood of the maximum likelihood estimator, and the stochastic approximation is performed during the final K 2 iterations where γ k = 1/(k -K 1 + 1), ensuring the almost sure convergence of the estimator. Also, the step size in the first few initial iterations (6 by default) is set to 0, as we are not interested in computing Q during the run-in sequence. The SAEM algorithm has been implemented in the MATLAB software under the name Monolix  (Kuhn and Lavielle (2005) ). It has been shown theoretically to converge to a maximum of the likelihood of the observations under very general conditions  (Delyon et al. (1999) ). To avoid local maxima, a simulated annealing step is implemented in a first series of iteration to ensure proper exploration of the parameter space, which confers a certain robustness with respect to the choice of initial parameter values to the SAEM algorithm.
Model evaluation Model evaluation is a vital part of model building. Detecting model deficiencies can help guide the next model to be tested. Basic model diagnostics compare model point predictions and observations, while more sophisticated diagnostics involve simulations under the model  (Brendel et al. (2006) ;  Comets, Brendel, and Mentré (2008, 2010) ). Other elements to assess model performance include predictive abilities on external datasets. Computing predictions requires estimates of subject-specific parameters. In nonlinear mixed effect models, two sets of predictions are generally considered. Population predictions use the estimates of the population parameters and the individual design, typically dose regimen and regressors in PK/PD, while individual predictions are obtained using the individual parameters.
Package structure The saemix package implements the SAEM algorithm in R using S4 object-oriented programming. The main function in the package is the saemix() function, which estimates the population parameters of a nonlinear mixed effect model. This function requires two mandatory arguments, the (structural and statistical) model, a saemixModel object, and the data, a saemixData object created by the saemixData() function. An optional list of settings can be passed on as a list. The syntax of the saemix() function is simply: saemix(model, data, control) where the control argument is optional. The model object is created by a call to the saemixModel() function, with the following main arguments: saemixModel  (model, psi0, description, error. model, transform. par, fixed. estim, covariate. model, covariance.
error. init a vector of size 2 giving the initial value of a and b in the error model. The data object is created by a call to the saemixData() function: saemixData(name. data, header, sep, na, name. group, name. predictors, name. response, name. X, name. covariates, units,. ) The first argument is the only mandatory argument, and gives the name of the dataset. All others have default values, provided the columns of the dataset have names which can be identified by the program, although the user is encouraged to provide the names of the group, predictors and response columns for safety: name. data name of the dataset (can be a character string giving the name of a file on disk or the name of a dataset in the R session. header whether the dataset/file contains a header. sep the field separator character.
Examples The objective of this section is to show how to use the saemix package through several examples. In the first example, we will show the main features of a typical longitudinal dataset used in all modelling software, the Orange tree dataset. This very simple example will allow us to explain the structure of the data object and to create a simple logistic model that we can fit with saemix(). We then show the main output from the package. In the second example, we will consider a well-known pharmacokinetic example, giving an example of a covariate model, and we will use this example to showcase the diagnostic plots provided in the package. In the third example, we will study the statistical performances of the SAEM algorithm in terms of parameter estimation through a simulation study, by applying saemix to an Emax model for dose-response data, and we show the influence of tuning the parameters in the algorithm.
Orange trees The data: the orange tree data was originally presented by Draper and Smith  (Draper and Smith (1981) ) and was used by  Pinheiro and Bates (1995)  to demonstrate the nlme package. It is now available in the datasets package distributed with R, and it is also distributed with other statistical programs, most notably SAS and WinBugs. The dataset contains measurements of the circumference at chest height of 5 orange trees, measured at seven time points during a period of 4 years. The data is available in R under the name Orange. The data object is created through the function saemixData. We need to specify the name of the dataframe, as well as the columns containing the grouping factor (indicating the subject), the predictor(s) and the response. Here, the grouping factor is Tree, and the number of the tree is given in the first column, while the second contains the age of the tree (the predictor) and the third its circumference (the response).
R> data("Orange") R> head(Orange) The units element is optional, but if given, will be used to label the plots. Note that it is also possible to give the number of the columns instead of the names, as in: R> orange <-saemixData(name. data = Orange, name. group = 1, + name. predictors = 2, name. response = 3) and that there is also some automatic name recognition built in the function (see the second example in Section 4. 2). A plot of the data can be obtained by a call to the plot function, yielding the graph shown in Figure  1. Modelling: different mathematical functions can be used to describe growth curves. Pinheiro and Bates used the following three-parameters logistic model to predict f (x), the circumference of the tree at age x:.
R> plot(orange) f (x) = λ 1 1 + e - (x -λ 2 ) λ 3 (6) They assumed an additive error model with constant variance ( ij ∼ N (0, σ 2 )). Since the dataset contained only 5 subjects, they assumed that only the intercept λ 1 varied across trees, and they set a normal distribution for λ 1 so that λ 1i ∼ N (µ 1 , ω 2 1 ). The individual vector of parameters is then λ i = {λ 1i , λ 2 , λ 3 } To set up this model in saemix, we first define a general model function. This function must have 3 arguments named psi (assumed to be a matrix with a number of columns equal to the number of parameters in the model, here 3), id (assumed to be a vector of indices matching observation number with subject index) and xidep (assumed to be a matrix with as many columns as predictors, here 1). The three arguments passed to the function will be generated automatically from the model and data object within the saemix code.
The function must return a vector of predictions, the length of which is equal to the number of rows in the predictor xidep. The following code snippet shows how to define the function f for the orange tree model as a saemix model function: R> logistic. model <-function(psi, id, xidep) { + age <-xidep[, 1] + lambda1 <-psi[id, 1] + lambda2 <-psi[id, 2] + lambda3 <-psi[id, 3] + resp <-lambda1 / (1 + exp( -(age -lambda2) / lambda3)) + return(resp) + } The user only needs to change the computation of the response, and adjust the number of predictors and parameters. More examples of model functions can be found in the documentation online, as well as in the other examples (Sections 4. 2 and 4. 3). We then build the statistical model through the function saemixModel: R> orange. model <-saemixModel(model = logistic.
By default, the likelihood is computed both by linearisation and by importance sampling, and the corresponding Akaike (AIC) and Schwarz (BIC) information criteria are computed. In this very simple model, both are pratically identical. For each parameter estimated in the model, estimates of the standard error are reported, as an absolute value (SE) and relative to the estimate, as a coefficient of variation (% CV). In the present case, all the fixed parameters are well estimated, with coefficients of variations less than 10%, and the standard deviation of parameter λ 1 (measuring its variability) is estimated to be about 33, with an estimation error somewhat higher (65%) reflecting the limited information available with only 5 subjects in the dataset. ---------------------------------------Results  ------------------------------------------------------------------------------------------------------------Fixed effects ---------------------------------------------------------------------   --------------------------------------------------------   --------------------------------------------------------- omega2.
Finally, we can check that the model is able to describe the observed data by producing plots of the individual fits: ---------------------------------------------------- -----------Variance of random effects ----------- ---------------------------------------------------- Parameter Estimate SE CV(%) lambda1 omega2. lambda1 1043 673 65 - R> plot(orange. fit, plot. type = "individual", smooth = TRUE) this code adds the smooth = TRUE argument to use more time-points on the X-axis for the plot, and computes the prediction at each time-point using the estimated individual parameters for each tree. The result is shown in Figure  3  and illustrates a very good fit of the model for all subjects. Corresponding code for nlme and nlmer: the same model can be fit to the Orange data using either nlmer from lme4 or nlme from nlme.
The following code, adapted from the online help for nlme, loads the two libraries and defines the model function as a user-defined function. It is also possible to use the built-in SSlogis function, but the purpose of this paragraph is to show how models in saemix relate to other modelling packages to facilitate switching from one to the other. The same function can be used for both nlmer and nlme, but nlmer needs the gradients to be defined in the function through the deriv function: R> library("nlme") R> library("lme4") R> modelform <-~lambda1 / (1 + exp( -(age -lambda2) / lambda3)) R> nlmer. orangemod <-deriv(modelform, namevec = c("lambda1", "lambda2", + "lambda3"), function. arg = c("age", "lambda1", "lambda2", "lambda3")) R> startvec <-c(lambda1 = 200, lambda2 = 800, lambda3 = 400) The following code performs the fit using nlmer: R> nlmer.