Research
On-device research index

arXiv research

A locally-built, LLM-digested index of recent arXiv papers in quant finance, geometry/topology, and statistical ML — keyword search served straight from SQLite on this machine.

168,694 papers · 148 categories

Trend · papers per month

129257386514 · Jun 202019922001200920172026
48 results for large formal libraries

New method selects facts in proofs using stateful recurrent neural networks.

problem Selecting facts for proving new goals over large formal libraries.
method Stateful architecture based on recurrent neural networks with data augmentation.
result Significantly better performance and solving many new problems compared to previous methods.

Lean 4 library formalizes mathematical finance, verifying over 200 theorems.

problem Formal verification of complex financial mathematics.
method Lean 4 proof assistant, Mathlib, BrownianMotion package, formal verification of over 200 theorems.
result Formal verification yields certified unification of known financial results.

We consider the problem of developing suitable learning representations (embeddings) for library packages that capture semantic similarity among libraries. Such representations are known to improve the performance of downstream learning tasks (e.g. classification) or applications such as contextual search and analogica…

2019-03-27abs ↗pdf ↗

This paper presents LIBTwinSVM, a free, efficient, and open source library for Twin Support Vector Machines (TSVMs). Our library provides a set of useful functionalities such as fast TSVMs estimators, model selection, visualization, a graphical user interface (GUI) application, and a Python application programming inte…

2020-01-27abs ↗pdf ↗

SOL is an open-source library for scalable online learning algorithms, and is particularly suitable for learning with high-dimensional data. The library provides a family of regular and sparse online learning algorithms for large-scale binary and multi-class classification tasks with high efficiency, scalability, porta…

2016-10-28abs ↗pdf ↗

Many (but not all) approaches self-qualifying as "meta-learning" in deep learning and reinforcement learning fit a common pattern of approximating the solution to a nested optimization problem. In this paper, we give a formalization of this shared pattern, which we call GIMLI, prove its general requirements, and derive…

2019-10-03abs ↗pdf ↗

Picasso is a new library for sparse learning problems in R and Python.

problem Sparse learning problems in high-dimensional data analysis.
method Unified framework of pathwise coordinate optimization with efficient active set selection strategies.
result picasso can efficiently handle large-scale problems.

LibAUC optimizes X-risks for AI tasks like CID, LTR, and CLR.

problem Optimizing risk functions in AI for tasks like classification, ranking, and representation learning.
method Developed a new mini-batch pipeline for deep X-risk optimization (DXO) algorithms.
result Achieved great success in solving CID, LTR, and CLR tasks with faster convergence and scalable performance.

Mango automates hyperparameter tuning for large-scale ML training.

problem Manual hyperparameter tuning is tedious and inefficient for large-scale machine learning.
method Parallel hyperparameter tuning with intelligent search strategies and flexible abstractions.
result Mango achieves comparable performance to Hyperopt while supporting distributed computing.

We consider the problem of finding the minimizer of a function f:RdRf: \mathbb{R}^d \rightarrow \mathbb{R} of the finite-sum form minf(w)=1/ninfi(w)\min f(w) = 1/n\sum_{i}^n f_i(w). This problem has been studied intensively in recent years in the field of machine learning (ML). One promising approach for large-scale data is to use a stoc…

2017-10-27abs ↗pdf ↗

We study the problem of using low computational cost to automate the choices of learners and hyperparameters for an ad-hoc training dataset and error metric, by conducting trials of different configurations on the given training data. We investigate the joint impact of multiple factors on both trial cost and model erro…

2019-11-12abs ↗pdf ↗

LeanDojo removes barriers to theorem proving with open-source tools and data.

problem Difficulty in reproducing and building on existing theorem proving methods.
method Introduces LeanDojo, an open-source Lean playground with toolkits, data, models, and benchmarks.
result ReProver, an LLM-based prover augmented with retrieval, outperforms non-retrieval baselines and GPT-4.

AlphaLogics mines market logic to generate interpretable alpha factors.

problem Complex, opaque alpha factors from factor mining overlook market logic.
method Market Logic Mining, Factor Generation and Optimization, Market Logic Generation and Optimization.
result AlphaLogics improves predictive metrics and risk-adjusted returns over baselines.

Deep Learning has established itself to be a common occurrence in the business lexicon. The unprecedented success of deep learning in recent years can be attributed to: abundance of data, availability of gargantuan compute capabilities offered by GPUs, and adoption of open-source philosophy by the researchers and indus…

2019-09-30abs ↗pdf ↗

Proposes qPO, a new acquisition strategy for batched Bayesian optimization that maximizes the probability of including the optimum.

problem Efficiently identifying top-performing compounds from a large chemical library.
method qPO (multipoint Probability of Optimality) acquisition strategy that maximizes the probability of including the true optimum.
result Empirical evidence shows that qPO is competitive with and complements other state-of-the-art methods in batched Bayesian optimization.

Training modern deep learning models requires large amounts of computation, often provided by GPUs. Scaling computation from one GPU to many can enable much faster training and research progress but entails two complications. First, the training library must support inter-GPU communication. Depending on the particular …

2018-02-15abs ↗pdf ↗

TrueLearn Python library for personalized educational recommendations.

problem Building educational recommendation systems with humanly-intuitive user representations.
method Online learning Bayesian models and open learner concept.
result Library includes models and representations for user control and interpretability.

IllinoisSL is a Java library for learning structured prediction models. It supports structured Support Vector Machines and structured Perceptron. The library consists of a core learning module and several applications, which can be executed from command-lines. Documentation is provided to guide users. In Comparison to …

2015-09-23abs ↗pdf ↗

Orthogonium offers unified, efficient layers for robust deep learning.

problem Fragmented and computationally demanding implementations of orthogonal and 1-Lipschitz layers.
method Unified, efficient PyTorch library providing orthogonal and 1-Lipschitz layers.
result Reduced overhead and standardized tools for robust experimentation.

A new algorithm speeds up sparse regression for discovering equations from data.

problem Learning governing equations from vast data with unsatisfying descriptions.
method SPRINT: a fast algorithm using bisection and analytic bounds to identify optimal rank-1 modifications.
result A calculation that would take millions of years can be done in a day.

In the past decades, spectral clustering (SC) has become one of the most effective clustering algorithms. However, most previous studies focus on spectral clustering tasks with a fixed task set, which cannot incorporate with a new spectral clustering task without accessing to previously learned tasks. In this paper, we…

2019-11-27abs ↗pdf ↗

Modified BFGS and LBFGS++ libraries boost performance for non-parallelizable functions.

problem Improving performance of non-parallelizable functions using SIMD and AAD.
method Modifications to BFGS and LBFGS++ libraries, utilizing SIMD and Automatic Differentiation (AAD).
result Up to 3.8 times faster for European Swaption curve calibration and 1.4 times faster for LMM model calibration.