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,742 papers · 148 categories

Trend · papers per month

51102153204 · Jun 202019922001200920172026
48 results for verification policies

Formalizes weak and strong verification for LLMs, controlling errors without assumptions.

problem Balancing cost and reliability in reasoning with LLMs.
method Formalizes weak-strong verification policies, introduces metrics, develops online algorithm.
result Optimal policies admit a two-threshold structure, and calibration and sharpness govern value of weak verifiers.

Revel tackles safe exploration in RL with verified symbolic policies.

problem Computational infeasibility of verifying neural networks in RL learning loops.
method Two policy classes: neurosymbolic with approximate gradients and symbolic policies for efficient verification. Mirror descent over policies to safely update and project policies.
result Revel discovers policies that outperform prior approaches to verified exploration.

New approach generates optimal disturbances for controller verification.

problem Optimizing disturbances for controller verification with blackbox access.
method Online learning approach that adaptively generates disturbances based on controller inputs.
result New algorithm (MOTR) outperforms existing methods in simulated examples.

We present a reinforcement learning framework, called Programmatically Interpretable Reinforcement Learning (PIRL), that is designed to generate interpretable and verifiable agent policies. Unlike the popular Deep Reinforcement Learning (DRL) paradigm, which represents policies by neural networks, PIRL represents polic…

2018-04-06abs ↗pdf ↗

We study the problem of programmatic reinforcement learning, in which policies are represented as short programs in a symbolic language. Programmatic policies can be more interpretable, generalizable, and amenable to formal verification than neural policies; however, designing rigorous learning approaches for such poli…

2019-07-11abs ↗pdf ↗

Despite the tremendous advances that have been made in the last decade on developing useful machine-learning applications, their wider adoption has been hindered by the lack of strong assurance guarantees that can be made about their behavior. In this paper, we consider how formal verification techniques developed for …

2019-07-16abs ↗pdf ↗

Reinforcement learning is a powerful paradigm for learning optimal policies from experimental data. However, to find optimal policies, most reinforcement learning algorithms explore all possible actions, which may be harmful for real-world systems. As a consequence, learning algorithms are rarely applied on safety-crit…

2017-05-23abs ↗pdf ↗

Enhances large language models' reasoning through simpler off-policy reinforcement learning.

problem Improving large language models' ability to reason and solve problems.
method EM Policy Gradient, optimizing expected return over reasoning trajectories using Expectation-Maximization (EM) optimization.
result Achieves comparable or slightly superior performance to state-of-the-art methods on reasoning datasets, with additional cognitive behaviors.

VERAFI improves financial AI by verifying calculations and compliance.

problem Financial AI systems generate errors and violations during reasoning.
method VERAFI combines dense retrieval, reranking, and automated reasoning policies.
result VERAFI achieves 94.7% factual correctness, 81% relative improvement.

In this paper, we assume an insure is allowed to purchase proportional reinsurance and can invest his or her wealth into the financial market where a savings account, stocks and bonds are available. Different from classical optimal investment and reinsurance problem, this paper studies the insurer's long-term investmen…

2014-06-30abs ↗pdf ↗

Hypothesis testing is an important problem with applications in target localization, clinical trials etc. Many active hypothesis testing strategies operate in two phases: an exploration phase and a verification phase. In the exploration phase, selection of experiments is such that a moderate level of confidence on the …

2018-12-04abs ↗pdf ↗

Accelerates DNN robustness verification with target labels.

problem Improving the robustness of deep neural networks against adversarial attacks.
method Guiding robustness verification with target labels, reducing search space and using symbolic interval propagation and linear relaxation.
result Significantly improves DNN verification speed by 36X, especially when perturbation distance is reasonable.

New methods combat data poisoning attacks in bandit algorithms using limited verification.

problem Data poisoning attacks on bandit algorithms, especially in the UCB and ETC types.
method Verification-based mechanisms to restore optimal regret with limited verifications.
result A simple modified ETC type bandit algorithm can restore optimal regret with O(logT)O(\log T) verifications.

In this paper we demonstrate that performance of a speaker verification system can be improved by concatenating electroencephalography (EEG) signal features with speech signal features or only using EEG signal features. We use state-of-the-art end-to-end deep learning model for performing speaker verification and we de…

2019-06-17abs ↗pdf ↗

Improves neural network verification by merging abstract domains and Lagrangian methods.

problem Prove provable bounds for neural network outputs given input ranges.
method Uses zonotopes within a Lagrangian decomposition to verify deep neural networks.
result Yields bounds that improve upon existing techniques in both time and tightness.

This paper explores formal verification for autonomous systems, identifying limitations and proposing improvements.

problem Ensuring safety of autonomous systems like self-driving cars and drones.
method Formal verification techniques based on formal methods, analyzing three assumptions and their limitations.
result Preliminary work to improve the strength of evidence provided by formal verification.

Paper develops a model for verifying facts in tables without pre-retrieved evidence.

problem Verification of factual claims in structured data, especially in open-domain settings.
method Joint reranking-and-verification model that fuses evidence documents.
result Model achieves comparable performance to closed-domain state-of-the-art on TabFact dataset.

Fraud detection is a difficult problem that can benefit from predictive modeling. However, the verification of a prediction is challenging; for a single insurance policy, the model only provides a prediction score. We present a case study where we reflect on different instance-level model explanation techniques to aid …

2018-06-19abs ↗pdf ↗

Efficiently verifies neural networks by handling neuron splits, improving speed and accuracy.

problem Handling neuron split constraints in incomplete neural network verification.
method β-CROWN, which optimizes parameters β to encode neuron splits and uses them in bound propagation.
result β-CROWN significantly speeds up verification while maintaining high accuracy.

Semantify-NN verifies neural network robustness against semantic perturbations.

problem Verifying robustness of neural networks against semantic adversarial attacks.
method Inserting semantic perturbation layers (SP-layers) into neural networks to verify robustness.
result Semantify-NN significantly improves robustness verification performance over p\ell_p-norm-based methods.

Researchers find floating point errors can mislead neural network verifiers.

problem Floating point arithmetic inaccuracies mislead neural network verifiers.
method Efficiently searches inputs and constructs neural network architectures to exploit verification errors.
result Floating point errors can systematically mislead neural network verifiers.

We study the robustness verification problem for tree-based models, including decision trees, random forests (RFs) and gradient boosted decision trees (GBDTs). Formal robustness verification of decision tree ensembles involves finding the exact minimal adversarial perturbation or a guaranteed lower bound of it. Existin…

2019-06-10abs ↗pdf ↗

This study extends verifiable learning to boosted tree ensembles, enabling efficient security verification.

problem Efficiently verifying the robustness of boosted tree ensembles against norm-based attackers.
method Formal verification of robustness for large-spread boosted tree ensembles, considering LL_\infty-norm and pseudo-polynomial time for LpL_p-norm verification.
result Polynomial time verification for LL_\infty-norm attackers, NP-hard for other norms, and pseudo-polynomial time for LpL_p-norm verification.

This paper tackles robustness of ensemble stumps and trees under general ℓ_p norm perturbations.

problem The vulnerability of ensemble stumps and trees to small input perturbations under the ℓ_∞ norm.
method Developed dynamic programming algorithms for robustness verification and certified defense under general ℓ_p norm perturbations.
result First certified defense method for ensemble stumps and trees under ℓ_p norm perturbations.

A neural network learns to improve verification of neural networks.

problem Efficient verification of neural networks for safety-critical applications.
method A graph neural network (GNN) learns to imitate strong branching heuristics for effective branching in the Branch and Bound (BaB) formulation.
result Reduces the number of branches and verification time by roughly 50% compared to hand-designed strategies.

New spoofing strategies show PoL verification is more vulnerable than previously thought.

problem Vulnerability of Proof-of-Learning verification mechanisms.
method Developed new spoofing strategies that can be reproduced across different configurations and are more cost-effective.
result Current PoL verification is not robust to adversaries and requires further understanding of optimization in deep learning.

We present a scoring approach for speaker verification that mimics the standard PLDA-based backend process used in most current speaker verification systems. However, unlike the standard backends, all parameters of the model are jointly trained to optimize the binary cross-entropy for the speaker verification task. We …

2019-11-26abs ↗pdf ↗

NeuroDiff improves neural network equivalence verification with fine-grained approximations.

problem Verifying the equivalence of compressed neural networks.
method Symbolic and fine-grained approximation technique for differential verification.
result NeuroDiff achieves up to 1000X speedup and 5X accuracy improvement.