dataesr/scientific-paragraphs-categorization huggingface dataset:
(2015) , JPrIME-DLTRS was run on the sequence alignments with JC69 with a gamma distribution as model of evolution (GTR is not available in JPrIME-DLTRS), 100 000 iterations, a thinning factor of 10 and a time out of 10h. Finally, TERA and ALE were run on the set of bootstrap trees with default parameters, except for the weight of amalgamation c A , fixed to 0. 1 for TERA as for ecceTERA. The accuracy -defined as normalized Robinson-Foulds distance to the true gene tree -of TERA, ecceTERA and ALE is comparable and higher than the one of JPrIME-DLTRS and RAxML (see Figure  2 ). The method that outperforms the others in this case is TreeFix-DTL. This is possibly due to the fact that the synthetic data set was simulated on the same model used to estimate the gene trees with TreeFix-DTL, making the task easier for the method.
Cyanobacteria Data sets The biological and simulated cyanobacteria data sets used here have been made public by  Szöllősi et al. (2013)  at http://datadryad. org/ resource/doi:10. 5061/dryad. pv6df. Their construction consisted in selecting 1099 gene families from 36 cyanobacteria species, related by a known dated species tree. These families were retrieved from HOGENOM  (Penel et al. , 2009) , and selected for their reasonable size and representativity. To obtain the biological data set, multiple-alignments on these families were computed with Muscle  (Edgar, 2004). To obtain the simulated data set, from each multiple-alignment of the real data set, a sample of 1000 trees was computed with PhyloBayes  (Lartillot et al. , 2009) , and an amalgamated tree was reconstructed with ALE  (Szöllősi et al.
8, 0. 7 and 0. 6). We report the results of ALE and PhyML from  Scornavacca et al. (2015) , plus the results for MowgliNNI for the same thresholds used for ecceTERA. Both ecceTERA and Mowgli were given the "simulated" PhyML trees with SH branch supports. Finally, we report the accuracy of ALE when using as input 100 sample trees (ALE 100 in Figure  4 ) among the 10k trees provided, mimicking the information contained in a set of bootstrap trees. Figure  4  shows that, for this data set, ecceTERA with a threshold of 0. 8 achieves a slightly better accuracy than all other methods, while with a threshold of 0. 7-0. 6 the accuracy is comparable to that of ALE. Moreover, the accuracy of ecceTERA increases with the threshold for weak edges, while this is not the case for MowgliNNI. It is also worth noting that the accuracy of ALE decreases considerably when used on small samples of trees.
134 for a threshold of 0. 8 for weakly supported edges (the average is 0. 24 if the costs are respectively 2,3 and 1, see Figure  4 ); the average stays at 0. 133 if the costs are 2,3 and 1 but all tripartitions are considered equiprobable, while it goes down to 0. 151 for unitary costs and equiprobable tripartitions. Tests on the biological data set. From each multiple alignment, a maximum-likelihood tree was computed with PhyML  (Guindon et al. , 2010)  with SH branch supports. These PhyML trees were corrected using ecceTERA with a threshold for weak edges equal to 0. 8. The weight of amalgamation c A was estimated, with starting value 1. Gene trees were considered as unrooted and the species tree as dated. We measured the quality of the corrected trees compared to that of the maximum-likelihood trees in two ways.
This paper has a focused goal. We aim to demystify the interaction between compiler transformations and deoptimization. When are two versions compiled under different assumptions equivalent? How should traditional optimizations be adapted when operating on code containing deoptimization points? In what ways does deoptimization inhibit optimizations? In this work we give compiler writers the formal tools they need to reason about speculative optimizations. To do this in a way that is independent of the specific language being targeted and of implementation details relative to a particular compiler infrastructure, we have designed a high-level compiler intermediate representation (IR), named sourir, that is adequate for many dynamic languages without being tied to any one in particular. Sourir is inspired by our work on RIR, an IR for the R language.
A sourir program is made up of functions, and each function can have multiple versions. We equip the IR with a single instruction, named assume, specific to speculative optimization. This instruction has the role of describing what assumptions are being used to perform speculative optimization and what information must be preserved for deoptimization. It tests if those assumptions hold, and in case they do not, transfers control to another, less optimized version of the code. Reifying assumptions in the IR makes the interaction with compiler transformations explicit and simplifies reasoning. The assume instruction is more than a branch: when deoptimizing it replaces the current stack frame with a stack frame that has the variables and values expected by the target version, and, in case the function was inlined, it synthesizes missing stack frames.
Furthermore, unlike a branch, its deoptimization target is not followed by the compiler during analysis and optimization. The code executed in case of deoptimization is invisible to the optimizer. This simplifies optimizations and reduces compile time as i = i, j = i + 1] a[i] ← a[i + 1] a[i + 1] ← t i ← i + 1 goto Lt Lrt. Vbase. Lt branch i < limit Lo Lrt Lo call j = add(i, 1) Ls call t1 = get(a, i) call t2 = get(a, j) call t3 = store(a, i, t2) call t4 = store(a, j, t1) i ← j goto Lt Lrt. analysis remains local to the version being optimized and the deoptimization metadata is considered to be a stand-in for the target version. As an example consider the function from Figure  1. A possible translation to sourir is shown in Figure  2  (less relevant code elided). Vbase contains the original version.
Helper functions get and store implement JavaScript (JS) array semantics, and the function add implement JS addition. Version Vnative contains only primitive sourir instructions. This version is optimized under the assumption that the variable a is an array of primitive numbers, which is represented by the first assume instruction. Further, JS arrays can be sparse and contain holes, in which case access might need to be delegated to a getter function. For this example HL denotes such a hole. The second assume instruction reifies the compiler's speculation that the array has no holes, by asserting the predicate t HL. It also contains the associated deoptimization metadata. In case the predicate does not hold, we deoptimize to a related position in the base version by recreating the variables in the target scope.
Our work makes several simplifying assumptions. We use the same IR for optimized and unoptimized code. We ignore the issue of generation of versions: we study optimizations operating on a program at a certain point in time, on a set of versions created before that time. We do not model the low-level details of code generation. Correctness of runtime code generation and code modification within a JIT compiler has been addressed by  Myreen [2010]. Sourir is not designed for implementation, but to give a reasoning model for existing JIT implementations. We do not intend to implement a new JIT engine. Instead, we evaluated our work by discussing it with JIT implementers; the V8 team [Chromium 2017] confirmed that intuitions and correctness arguments could be ported from sourir to their setting.
RELATED WORK The SELF virtual machine pioneered dynamic deoptimization  [Hölzle, Chambers, and Ungar 1992]. The SELF compiler implemented many optimizations, one of which was aggressive inlining, yet the language designers wanted to give end users the illusion that they were debugging source code. They achieved this by replacing optimized code and the corresponding stack frames with non-optimized code and matching stack frames. When deoptimizing code that had been inlined, the SELF compiler synthesized stack frames. The HotSpot compiler followed from the work on SELF by introducing the idea of speculative optimizations  [Paleczny, Vick, and Click 2001]. HotSpot supported very specific assumptions related to the structure of the class hierarchy and instrumented the class loader to trigger invalidation.
The paper also introduces the idea of being able to transfer control at any point. We support both the update of metadata and unconstrained deoptimization. Modern virtual machines have all incorporated some degree of speculation and support for deoptimization. These include implementations of Java (HotSpot, Jikes RVM), JavaScript (WebKit Core, Chromium V8, Truffle/JS, Firefox), Ruby (Truffle/Ruby), and R (FastR), among others. Anecdotal evidence suggests that the representation adopted in this work is representative of the instructions found in the IR of production VMs: the TurboFan IR from V8 [Chromium 2017] represents assume with three distinct nodes. First a checkpoint, holding the deoptimization target, marks a stable point, to where execution can be rolled back. In sourir this corresponds to the original location of an assume.
Alternatively,  Wang, Lin, Blackburn, Norrish, and Hosking [2015]  propose an IR that supports restricted primitives for hot-patching code in a JIT. There is a rich literature on formalizing compiler optimizations. The CompCert project  [Leroy and Blazy 2008]  for example implements many optimizations, and contains detailed proof arguments for a data-flow optimization used for constant folding that is similar to ours. In fact, sourir is close to CompCert's RTL language without versions or assumptions. There are formalizations for tracing compilers  [Dissegna, Logozzo, and Ranzato 2014; Guo and Palsberg 2011 ], but we are unaware of any other formalization effort for speculative optimizations in general. Béra, Miranda, Denker, and Ducasse [2016]  present a verifier for a bytecode-to-bytecode optimizer.
SOURIR: SPECULATIVE COMPILATION UNDER ASSUMPTIONS This section introduces our IR and its design principles. We first present the structure of programs and the assume instruction. Then, Section 3. 2 and following explain how sourir maintains multiple equivalent versions of the same function, each with a different set of assumptions. This enables the speculative optimizations presented in Section 4. All concepts introduced in this section are formalized in Section 5. Sourir is an untyped language with lexically scoped mutable variables and first-class functions. As an example the function in Figure  3  queries a number n from the user and initializes an array with values from 0 to n-1. By design, sourir is a cross between a compiler representation and a high-level language.
Sourir in a Nutshell var n = nil read n array t[n] var k = 0 goto L1 L1 branch k < n L2 L3 L2 t[k] ← k k ← k + 1 goto L1 L3 drop k stop We have equipped it with sufficient expressive power so that it is possible to write interesting programs in a style reminiscent of dynamic languages. 1 The only features that are critical to our result are versions and assumptions. Versions are the counterpart of dynamically generated code fragments. Assumptions, represented by the assume instruction, support dynamic deoptimization of speculatively compiled code. The syntax of sourir instructions is shown in Figure  4. Sourir supports defining a local variable, removing a variable from scope, variable assignment, creating arrays, array assignment, (unstructured) control flow, input and output, function calls and returns, assumptions, and terminating execution.
Case Study We conclude with an example. In dynamic languages code is often dispatched on runtime types. If types were known, code could be specialized, resulting in faster code with fewer checks and branches. Consider Figure  12 (a) which implements a generic binary division function that expects two values and their type tags. No static information is available; the arguments could be any type. Therefore, multiple checks are needed before the division; for example the slow branch will require even more checks on the exact value of the type tag. Suppose there is profiling information that indicates numbers can be expected. The function is specialized by speculatively pruning the branches as shown in Figure  12(b). In certain cases, sourir's transformations can make it appear as though checks have been reordered.
SPECULATIVE COMPILATION FORMALIZED A sourir program contains several functions, each of which can have multiple versions. This highlevel structure is described in Figure  13. The first version is considered the currently active version and will be executed by a call instruction. Each version consists of a stream of labeled instructions. We use an indentation-based syntax that directly reflects this structure and omit unreferenced instruction labels. Besides grammatical and scoping validity, we impose the following well-formedness requirements to ease analysis and reasoning. The last instruction of each version of the main function is stop. Two variable declarations for the same name cannot occur in the same instruction stream. This simplifies reasoning by letting us use variable names to unambiguously track information depending on the declaration site.
Say x is not accessed after the store in this optimized version. In sourir, it is obvious why dead store elimination of x would be unsound: the deoptimization metadata indicates that x is needed for deoptimization and the store operation can only be removed it can be replayed. In this specific example, a constant propagation pass could update the metadata to materialize the write of 0, only when deoptimizing at the second assume. But, before the code can be reduced, loop unrolling might result in intermediate versions that are much larger than the original program. In contrast, tracing JITs can handle this case without the drastic expansion in code size  [Gal et al. 2009 ], but lose more information about instructions outside of the trace. Speculative optimizations are key to just-in-time optimization of dynamic languages.
ACKNOWLEDGMENTS Jean-Marie Madiot  provided guidance on the use and limitations of various notions of bisimulation. In particular, he suggested adding a non-silent stop transition to recover equi-termination from weak bisimilarity. Francesco Zappa Nardelli  helped with the motivation and presentation of our work. We thank  Sewell, Nardelli, Owens, Peskine, Ridge, Sarkar , and Strniša [2007] for writing and maintaining Ott. Our work supported by the  National Science Foundation  under Grants  CCF-1544542 ,  CCF-1318227 ,  CCF-1618732 ,  ONR  award  503353 , and the  European Research Council (ERC)  under the European Union's  Horizon 2020 research and innovation program  (grant agreement  695412 ). Any opinions, findings, and conclusions expressed in this material may be those of the authors and likely do not reflect the views of our funding agencies.
Background: High-throughput technologies produce huge amounts of heterogeneous biological data at all cellular levels. Structuring these data together with biological knowledge is a critical issue in biology and requires integrative tools and methods such as bio-ontologies to extract and share valuable information. In parallel, the development of recent whole-cell models using a systemic cell description opened alternatives for data integration. Integrating a systemic cell description within a bio-ontology would help to progress in whole-cell data integration and modeling synergistically. Results: We present BiPON, an ontology integrating a multi-scale systemic representation of bacterial cellular processes. BiPON consists in of two sub-ontologies, bioBiPON and modelBiPON. bioBiPON organizes the systemic description of biological information while modelBiPON describes the mathematical models (including parameters) associated with biological processes.
Description of biological processes, corpus building and entity tagging In the absence of an exhaustive controlled vocabulary in systems biology, we use hereafter the notion of a "biological process", which comprises the notions of (a) "biological reaction" and "biochemical reaction" as in KEGG (Kyoto Encyclopedia of Genes and Genomes  [22] ) Reactions database, (b) "biological phenomenon", "biological pathway" and "biochemical pathway" as in PW or KEGG Pathway database, and finally (c) "biological process" as in GO-BP. Moreover, we use the notion of a "chemical entity" to denote any type of biological compound, including metabolites, proteins, protein complexes, polymers, to cite a few. To develop a dedicated systemic representation for each biological process involved in the bacterial gene expression, we applied the standard state-of-art approach of system engineering.
BiPON design BiPON is a bio-ontology that is composed of two subontologies: bioBiPON and modelBiPON. bioBiPON organizes the systemic description of biological information, while modelBiPON describes the mathematical models associated with biological processes. In the following, a class that has no sub-class for the property is_a is called a leaf-class. BiPON has been designed using the software editor Protégé 5 and the Description Logic Manchester syntax  [27].
Main classes BioBiPON contains four main classes, which corresponds to the main structure of major bio-ontologies: Biological process (GO:0008150), Chemical entity (CHEBI:24,431), Sequence feature (SO:0000110) and Cellular component (GO:0005575). The classes Biological process and Cellular component include a selection of GO classes, while the Chemical entity class includes a selection of ChEBI classes for small molecules, of SO classes for gene products (e. g. primary transcript), and terms of the KEGG database orthology (KO) for proteins  [22]. The Sequence feature class includes a selection of SO classes for sequence patterns. Finally, classes which were not present in existing bio-ontologies were created manually. The Biological process class contains as subclasses the biological processes and sub-processes (irrespective of their granularity level).
Importation and interoperability For all classes and properties that were imported from other bio-ontologies (e. g. translation initiation; see Fig. 3 ), we kept the original references, such as the Internationalized Resource Identifier (IRI) and Identifier (id) in bioBiPON, to ensure interoperability. In BiPON, the SO classes of gene products are now considered as subclasses of the Chemical entity class instead of the Sequence feature class. Due to this semantic change, we considered these SO classes as new classes: we gave a new IRI and kept the original one with the hasDbXref annotation (e. g. hasDbXref SO_0000185). When a class refers to a term in an existing database (such as KO), the original id is also kept with the hasDbXref annotation (e. g. prokaryote translation initiation factor IF-3: hasDbXref K02520; see Fig.
We provided an example of such a reasoning in the toyBiPON ontology (see Additional file 3). Altogether, this illustrates the usefulness of bio-ontologies through the ability of inferring new relations by automatic reasoning. Beyond that, ontologies are also widely used to organize data warehouses  [36] [37] [38]. BiPON is currently used to drive the development of a data warehouse for the bacterial gene expression processes. BiPON supports the design of the relational model of the database that stores and connects biological knowledge, heterogeneous multi-omics data  [2, 25, 39, 40] , static data such as sequence patterns, and mathematical models  [23, 24]. Highthroughput technologies already enable the acquisition of data at a large scale: transcriptome, proteome (including post-translational modifications), fluxome, interactome, metabolome, degradome, etc.
Contracts act as a glue between the structure levels, properties and V&V techniques. Classifying the properties enables us to select the adequate technique to cover the V&V requirements; model checking, theorem proving, model testing. The interaction properties are verified using model checking; the consistency properties are checked using theorem proving and the behaviour conformance against the functional contract is checked using a specific model testing technique. We assume a modelling language which is formal enough to specify SbC elements and contracts. We experiment this method on an embedded system using the Kmelia modelling language and its associated COSTO toolbox  (André et al. , 2010). Applying the proposed method increases confidence in the SbC models early in the development process: they are correct and embed passed test where contracts are reinforced.
Thus the method helps to obtain correct software as soon as possible and allows one to apply thereafter advanced development techniques such as agile ones (thanks to the qualified test cases and data we constructed) or Design-by-Contract techniques (thanks to the used contracts). In the remaining of the article, we sketch the Service-based Component model in Section 2; multilevel contracts are introduced in Section 3. Section 4 describes the combination of V&V techniques. We illustrate the proposed method and framework with the Kmelia/COSTO toolbox in Section 5. Section 6 discusses related works and we conclude in Section 7.
Functional Correctness by Model Testing The basic idea of Functional correctness (FC) is to evaluate all paths of a service behaviour and to determine whether it is compliant with the post-condition or not. This is a non-trivial problem similar to the one of model-checking a program. As soon as the modelling language includes high level data types and computation statements (e. g. loops) the provers reach their limits to prove. Model testing is used here to supply the missing verifications of automatic and interactive provers. In  (André et al. , 2013)  we argued for early testing at the model level to detect platform independent errors without melting them with implementation errors. Indeed plunging the model in a middleware decreases the testability and is often a burden to the V&V process.
Modelling with the Kmelia language Kmelia is an abstract formal component model dedicated to the specification and development of correct components  (André et al. , 2010; André et al. , 2010). A Kmelia component system is an assembly of components, which can themselves be composite. A component is a container of services; it is described with a state space constrained by an invariant. A service describes a functionality; it is more than a simple operation; it has a pre-condition, a post-condition and a behaviour described with a labelled transition system (LTS). Moreover a Kmelia service may give access to other (sub)services. The behaviour supports communication interactions, dynamic evolution rules and service composition. Kmelia is supported with an Eclipse-based analysis platform called COSTO (see Figure  6 ).
In the following we will detail the process that allows us to create test applications like the one we presented in Figure  8. The testing process is a sequence  The first model transformation is a model-tomodel transformation. It builds the test harness as an assembly of selected parts of the SUT with test components (mocks, test driver), and returns a Test Specific Model (TSM). It is semi-automatic transformation: the test intention is provided by the tester and COSTOTest asks her/him to make choices that are selected on the basis of static analysis of the PIM. During this first step, the aim for the tester is to build a harness such as the one illustrated in the bottom of Figure  8. The second transformation is a model-to-code transformation; COSTOTest generates the code to simulate the behaviour of the harness, then it merges the harness with a Platform Description Model (PDM) to get code (Java code in this case).