dataesr/scientific-paragraphs-categorization huggingface dataset:
That being said, it is however important to keep in mind the observations made in this paper are related to the diversity of French vineyards, which may be less important in other vine-growing countries. Its great diversity of cultivars and pruning systems makes it harder to design acquisition systems suited for all the vineyards, even in the same vine-growing region (Bordeaux). The acquisition issue is closely related to the database size and variability problem. The most robust algorithm cannot be trained without an extensive database showcasing detailed spatial (from the region scale to the plot scale) and temporal (phenological stages) variability. Ways to automatize picture acquisition are thus crucial, notably, finding ways to systematically link agricultural machine passage (tractors, high-leg tractors, robots, etc.
) with picture acquisitions. This, however, means algorithms must be designed around huge image databases which, in the current research state, tend to favor deep-learning-based algorithms. In this paper, the projects' database sizes varied a lot (depending on the vehicle and the number of available vineyards) but the actual numbers of labeled images used to train the algorithms was similar. The image labeling step is thus a clear bottleneck here. This means existing pipelines to label the training images need to be strengthened to be more efficient, whether they use fully manual annotation or new techniques such as transfer learning (TL) or few-shot learning (FSL)  [37]. The specificity of manual annotations in the agricultural world is, however, that in certain cases, the user needs to be highly skilled at the task at hand.
However, given the sheer complexity of vineyards and well-known "black box" effects related to deep learning, we believe significant efforts in the understanding and the evaluation of these algorithms' robustness will be necessary in the future to properly scale up proximal sensing applications. Results also stressed the need for the creation of better databases representing the huge variability of configurations encountered in vineyards, a phenomenon with further repercussions on the choice of algorithms. Mounting the cameras on agricultural machinery in order to get repeated images from each plant in the vineyard is a promising approach in order to boost the augmentation of these databases. However, it highlights a lot of practical issues, related to the camera mounting point, farmer cooperation or the use of the device in extreme conditions (spraying, moving mechanical parts).
Acknowledgments: For each individual project: EARN: Data were acquired at  Domaine Giraudaut  and  Rouhaud  affiliated to  Vignerons de Tutiac. The agronomic supervision of the project was assured by Vitinnov. ADVANTAGE:  Project Advantage  involves nine partners, including private companies, institutes of technology and public-sector research units:  Agrauxine Lesaffre Plant Care, Bayer, Bordeaux Sciences-Agro, Cybeletech, IFV, INRA-UMR SAVE, Mercier, Telespazio  and  University of Reims Champagne-Ardenne. ProXiMaVi: the authors would like to thank the  French National Institute for Agricultural Research Experimental Unit "Vigne et Vin Bordeaux Grande Ferrade"  ( UE 1442 ) (INRAe,  UMR SAVE 1065  and  UMR EGFV 1287 ) and the  French National Institute of Vines and Wine (IFV)  who made available the vineyards and the farm equipment and who also provided data and expertise regarding the monitoring of agronomic parameters of the plots under study.
Data Availability Statement: Data availability for each individual project: EARN (yield estimation): available through the article author (barna. keresztes@ims-bordeaux. fr); ADVANTAGE (esca detection): available through the corresponding author (florian. rancon@agro-bordeaux. fr); Proxi-MaVi (downy mildew detection): available online through a published data article  [39] ; ProspectFD: available through the article author (malo. tardif@u-bordeaux. fr).
The failure of bifocal pose estimation using RANSAC on hypothesized correspondences, e. g. , using 5 points  [48] , is highlighted in a dataset of images of mugs, Figure  1  (similar to the dataset in  [51]  but without a calibration board), for which the failure rate using the standard SfM pipeline COLMAP  [63]  is 75%. The failure of just directly apply-ing the 5-point algorithm in this example is even higher. A similar situation exists for images containing repeated patterns where there are plenty of features, but determining correspondences is challenging. Most traditional multiview pipelines estimate the relative pose of the two best views and then register the remaining views using a P3P algorithm  [68]  to reduce the failure rate. The focus of this paper is to address the issue of failure of traditional bifocal algorithms in such cases.
Implementation We provide an optimized open source C++ package called MINUS -MInimal problem NUmerical Solver 1. This is a homotopy continuation code specialized for minimal problems, templated in C++, so that efficient specialization for different problems and different formulations are possible. The most reliable and high-quality solver according to our experiments uses a 14 × 14 minors-based formulation. Although other formulations have demonstrated further potential for speedup by orders of magnitude, there may be reliability tradeoffs (c. f. supplementary material).
Our first experiment studies the numerical stability of the solvers. The dataset provides true point correspondences, which inherit an orientation from the tangent to the analytic curve. For each sample set, three triplets of point correspondences are randomly selected with two endowed with the orientation of the tangent to the curve. The real solutions are selected from among the output, and only those that generate positive depth are retained. The unused tangent of the third triplet is used to verify the solution as it is an overconstrained problem. For each of the remaining solutions a pose is determined. The error in pose estimation is compared with groundtruth as the angular error between normalized translation vectors and the angular error between the quaternions. The process of generating the input to pose computation is repeated 1000 times and averaged.
This experiment demonstrates that: (i) pose estimation errors are negligible, Figure  5 (a); (ii) the number of real solutions is small: 35 real solutions on average, pruned down to 7 on average by enforcing positive depth, and even further to about 3-4 physically realizable solutions on average employing the unused tangent of the third point as verification, Figure  5(b);  (iii) the solver fails in about 1% of cases, which are detectable and, while not a problem for RANSAC, can be eliminated by running the solver for that solution path with higher accuracy or more parameters at a higher computational cost. The second experiment shows that we can reliably and accurately determine camera pose with correct but noisy correspondences. Using the same dataset and a subset of the selection of three triplets of points and tangents -200 in total -zero-mean Gaussian noise was added both to the feature locations with σ ∈ {0.
The ratio of outliers is varied over 10%, 25% and 40%, and the experiment is repeated 100 times for each. The resulting reprojection error is small and stable across outlier ratios, Figure  8. Computational efficiency: Each solve using our software MINUS takes 660ms on average (1. 9s in the worst case) as compared to over 1 minute on average for the best prototypes using general purpose software  [8, 41] , both on an Intel core i7-7920HQ processor and four threads. More aggressive but potentially unsafe optimizations towards microseconds are feasible, but require assessing failure rate, as reported in the supplementary materials. Real data experiments: Much like the standard pipeline, SIFT features are first extracted from all images. Pairwise features are found by rank-ordering measured similarities and making sure each feature's match in another image is not ambiguous and is above accepted similarity.
Pairs of features from the first and second views are then grouped with the pairs of features from the second and third views into triplets. A cycle consistency check enforces that the triplets must also support a pair from the first and third views. Three feature triplets are then selected using RANSAC and the relative pose of the three cameras is determined from two tangents with their assigned SIFT orientation and a third point without orientation. Figure  9  shows that camera pose is reliabily and accurately found using triplets of images taken from the EPFL dense multi-view stereo test image dataset  [70]. Our quantitative estimates on 150 random triplets from this dataset give pose errors of 1. 5 × 10 -3 radians in translation and 3. 24 × 10 -4 radians in rotation. The average reprojection error is 0.
31 pixels. These are comparable to or better than the trifocal relative pose estimation methods reported in  [31]. Our conclusion for this dataset, whose purpose is simply to validate the solver, is that our method is at least as good and often better than the traditional ones. See supplementary data for more examples and a substantiation of this claim. Note that we do not advocate replacing the traditional method for this dataset. We simply state that our method works just as well, of course at a higher cost. EPFL dataset is feature-rich, typically yielding on the order of 1000 triplet features per image triplet. As such it does not portray some of the typical problems faced in challenging situations when there are few features available. The Amsterdam Teahouse Dataset  [71] , which also has ground-truth relative pose data, depicts scenes with fewer features.
RF is supported by  UERJ Prociência  and  FAPERJ Jovem Cientista do Nosso Estado   E-26/201. 557/2014. TD and AL are supported by  NSF   DMS-1151297. JDH and MHR are supported by  NSF   CCF-1812746 , with additional support for JDH from ONR  N00014-16-1-2722  and for MHR from  Schmitt Leadership Fellowship  in Science and Engineering. BK and HF are supported by the  NSF  grant  IIS-1910530. TP is supported by the  EU Regional Development Fund   IMPACT CZ. 02. 1. 01/0. 0/0. 0/15003/0000468  and  EU   H2020  project  ARtwin 856994. This work was initiated while most authors were in residence at  Brown University's Institute for Computational and Experimental Research in Mathematics -ICERM , in Providence, RI, during the Fall 2018 and Spring 2019 semesters (NSF  DMS-1439786  and the  Simons Foundation  grant  507536 ).
Lookup tables (finite maps) are a ubiquitous data structure. In pure functional languages they are best represented using trees instead of hash tables. In pure functional languages within constructive logic, without a primitive integer type, they are well represented using binary tries instead of search trees. In this work, we introduce canonical binary tries, an improved binary-trie data structure that enjoys a natural extensionality property, quite useful in proofs, and supports sparseness more efficiently. We provide full proofs of correctness in Coq. We provide microbenchmark measurements of canonical binary tries versus several other data structures for finite maps, in a variety of application contexts; as well as measurement of canonical versus original tries in two big, real systems.
Introduction Lookup tables-finite maps from identifiers to bindings-are a central data structure in many kinds of programs. We are particularly interested in programs that are proved correctcompilers, static analyzers, program verifiers. Those programs are often written in pure functional languages, since the proof theory of functional programming is more tractable than those of imperative or object-oriented languages. Thus we focus on applications written in the functional languages internal to the logics of Coq or HOL. Such programs may be There are no conflicts of interest. Code is available at https://github. com/xavierleroy/canonical-binary-tries/tree/v2.
"extracted" to programming languages such as OCaml, Standard ML, or Haskell, and compiled with optimizing compilers for those languages; the CompCert C compiler  [13]  and the Verasco static analyzer  [11]  are examples. On the other hand, some programs, such as the Verified Software Toolchain program verifier  [2] , don't use extraction: those programs are reduced within the logic of a proof assistant, so that the program verifier can gracefully interact with user-driven interactive proof in the ambient logic. Many proved-correct programs of this kind deliberately use an impoverished set of primitives, so that fewer axioms need to be assumed (or equivalently, fewer lines of proof-checker kernel code need to be trusted). In particular, there may be no primitive integer type implemented in a machine word.
Instead, integers (or whatever type is used for keys, the domain of the finite maps) may be constructed from the inductive data types of the logic. Consequently, we cannot assume that a less-than comparison of two keys takes constant time; it will be logarithmic in the magnitude of the numbers. These criteria led to a preliminary design for a data structure and its algebraic interface: binary tries, also called positive trees (for reasons that will become clear). This data structure was used in the CompCert C compiler, the Verified Software Toolchain (VST), the Verasco verified static analyzer, and in other applications. In the process, we have learned to demand more and more criteria of efficiency and provability from them: Core Requirements 1. Basic operators: empty (the finite map with an empty domain), get (the lookup operator), and set (the update operator).
It has been integrated in CompCert in 2021  [15]. Source code for implementations and proofs may also be found in the Coq development accompanying this article  [14]. Extensionality could be achieved in other ways, such as sigma-types in Coq (the dependent pair of a data structure with a proof of its canonicity). We describe alternative implementations in section 6. Our benchmark measurements (section 7) show that our new variant, "canonical binary tries" performs well in all contexts, while each of the alternatives is problematic in at least some contexts. Related work. Many lookup-table data structures have been implemented and proved correct in proof assistants. The books Verified Functional Algorithms  [3]  and Functional Algorithms Verified  [18]  each describe several pure-functional tree data structures with proofs of correctness (in Coq and Isabelle/HOL, respectively).
For example, the natural numbers, and addition upon them, are constructed as, 2 Persistent arrays give a functional semantics layered on an imperative (destructive-update) implementation, but these are not suitable because they would require extending the logic's kernel of axioms. 3 In fact, no programming language has a primitive integer type with constant-time comparisons; they typically have a range-limited integer type -2 k ≤ i < 2 k or a modular integer type (i mod 2 k ). Most versions of Coq 2005-present have not had a built-in integer type with fast comparisons; and relying on them would increase the size of the trusted base, that is, Coq kernel code, Coq axioms, Coq extraction to OCaml, and OCaml operations upon which we rely. and then properties such as the associativity of add are proved as lemmas instead of being axiomatized.
That's a lot more than the single word in which a native OCaml program or a C++ program might use to represent an integer key, but it is efficient enough in practice, for the CompCert compiler and similar applications. The positive number p, represented within Coq, also has log p constructors, but each Coq construction is represented within the Coq kernel as two OCaml constructions that describe the Coq constructor. So the number p occupies 5 log p words (or 8 • 5 log p bytes on a 64-bit machine). In practice this is usually efficient enough. 4 iven that Coq has this natural way to represent binary numbers using inductive data types, it is natural to use binary tries to implement lookup tables. A trie is a directed tree in which every edge is labeled from a finite alphabet; a word (such as "cat") is looked up by traversing the path of edges labeled sequentially with the letters of the word (such as "c" then "a" then "t"); and the nodes contain values of the range type of the lookup table.
Functions that operate over two trees, such as the combine function from Section 2, are more difficult to write because of the high number of cases. Consider the recursive case of the combine function, the one that operates on two nonempty trees in parallel. A naive case analysis on m1 and m2 results in 49 cases. Each case is simple enough: we call combine' if there are two left subtrees or two right subtrees, combine' l if there is only a left subtree, combine' r if there is only a right subtree. Likewise, reasoning about these 49 cases is relatively easy, using Coq's tactic language for automation. But writing all the cases in the first place is a pain! Even so, proofs about the 49-case combine' function can be concise. Consider this theorem, about the interaction of combine' with get': Lemma gcombine': ∀ m1 m2 i, get i (combine' m1 m2) = f (get' i m1) (get' i m2).
The first line describes a goal: define a recursive function of a particular type by structural induction on m1. The "Proof" is a case analysis described in Coq's tactic language: the destruct builds a pattern-match into the "proof" (in this case, into the "program"). So we start with two nested 7-case matches, that is, a 49-case double pattern match. Each one of those has a right-hand-side that's an application of the Node pseudo constructor, so we say apply Node in the tactic language. Since Node is a 3-argument function, we have three subgoals remaining, separated by the punctuation [ | | ]. In each case, we try four different things (the exact tactics), in the order given. The first of the four that type-checks is the one that will be chosen for use in defining the function. The reader may not be confident that this defines the right function! Indeed, the author of the tactic may not be confident.
This produces a dense, perfectly balanced binary trie. This is representative of how binary tries are used in the back-end of the CompCert compiler to represent control-flow graphs, in particular. Sparse: As in the Dense test, we insert then look up a number of keys. The keys correspond to words randomly chosen from an English dictionary, then converted to positive numbers by viewing the words as strings of bits, with 8 bits per character and an ASCII encoding. We have 5064 words with length ranging from 1 to 18 characters (average 8 characters). This test produces sparse, poorly balanced tries with long, nearly empty branches. It is representative of some uses of binary tries in the VST infrastructure, where keys are encodings of program identifiers. The static analyses of the CompCert back-end also use sparse tries intensively.
Repeated: We insert the same seven keys (1 to 7) a million times in a trie. The purpose of this test is to check that the trie remains small (7 nodes) and does not grow at each insertion. It is representative of the use of binary tries as environments in a reference interpreter: there are few variables in the program being interpreted, but they are assigned many times. For execution within Coq, we use vm_compute as our primary evaluation mechanism. It implements call-by-value through compilation to a virtual machine. For comparison, we also give some numbers obtained with the cbv and lazy mechanisms. These are interpreters that follow either call-by-value (cbv) or call-by-need (lazy). These mechanisms are much slower than vm_compute, hence we report results for the Sparse benchmark only. We also extract the benchmarks to OCaml and compile them to native code using the ocamlopt compiler.
Coq execution times show no improvement compared with the Original implementation. Combined with the lack of extensionality, these results show that Node01 is not an interesting alternative to Canonical. The Sigma implementation performs exactly like the Original implementation after extraction to OCaml. This is unsurprising: the subset type is erased during extraction, resulting in very similar OCaml code for the Sigma and Original implementations. As expected, execution inside Coq is slowed down by the construction and propagation of proof terms for the well-formedness invariant: modestly so (5% to 37% depending on the Coq evaluation mechanism used) for the Sparse and Dense tests, but dramatically so (a 5-times increase) for the Repeated test. The GADT implementation avoids the dramatic degradations of the Sigma implementation, but runs 17% to 100% slower than the Original implementation, both within Coq and after extraction to OCaml.
8%. For finer analysis, we profiled two of the compilations using the Linux perf tool, focusing on the functions that account for more than 0. 5% of the total compilation time. For the Spass test, binary tries operations account for 14% of the CompCert 3. 9 compilation time, and slow down by about 20% when moving to 3. 10. (This is consistent with the 20% slowdown on dense maps after extraction to OCaml reported in table 1. ) However, memory management (allocation and GC) account for 25% of the CompCert 3. 9 time, and speed up by 6% in 3. 10, owing to the reduced memory usage. The two effects almost cancel each other, resulting in a small slowdown overall. For the Unit3 test, binary tries operations account for 26% of the 3. 9 compilation time, and take about the same time in 3. 10, while memory management accounts for 44% of the 3.
Efficiency improvements in VST The Verified Software Toolchain (VST)  [2]  comprises a program logic (Verifiable C) for the C programming language, proved sound in Coq with respect to the operational semantics of CompCert Clight, and a proof automation system (VST-Floyd)  [8]  to assist users in applying the program logic to their program. Like CompCert, VST heavily uses PTrees for many purposes: mapping function-names to function-bodies, function-names to their specifications, global variable names to their types, local variable names to their types, local variable names to their symbolic contents, and so on. Unlike CompCert, which runs in extracted OCaml, VST runs inside Coq's Gallina logic, because it must manipulate proof goals and proof terms, and even the PTrees must map names to values that contain fragments of Coq terms and proofs.
Therefore, unlike in extracted OCaml where propositions and proofs-of-propositions have been erased, computations inside VST are unerased. This means that the sigma-type representation would be much less efficient in VST than it would be in CompCert. 6  recent enhancement to VST is Verified Software Units, which allows modular verification of modular C programs  [5]. The VSU system uses PTrees even more heavily, in reasoning about linkage of programs, of specifications, and of proofs. Furthermore, in the VSU system it is often necessary to compare two PTrees for equivalence, which is much faster to do in a data structure with extensionality. Furthermore, VST theorem statements (and intermediate proof goals) often contain concrete PTrees, mapping C program identifiers to various program specifications and AST terms.
At first, we were worried about the increase in the number of cases for function definitions and for proofs, compared with the original binary tries where there are only two cases to consider. We demonstrated two approaches to synthesizing large case analyses instead of writing them by hand: one is based on Coq's tactic language and lets us fluidly combine synthesis-time case analysis, run-time case analysis, and synthesis-time symbolic analysis; the other is based on custom constructors and induction principles that lets us view the new data structure as the original, two-case data structure, combined with partial evaluation within Coq to eliminate the run-time overhead of the view. More generally, Coq offers powerful metaprogramming facilities that have great potential to facilitate not just the verification but also the implementation of complex data structures.