Revisiting Variable Ordering for Real Quantifier Elimination using Machine Learning

• URL: http://arxiv.org/abs/2302.14038v1
• Date: Mon, 27 Feb 2023 18:48:33 GMT
• Title: Revisiting Variable Ordering for Real Quantifier Elimination using Machine Learning
• Authors: John Hester, Briland Hitaj, Grant Passmore, Sam Owre, Natarajan Shankar, Eric Yeh
• Abstract summary: We apply symmetries to create a new dataset containing more than 41K MetiTarski challenges designed to remove bias. We evaluate issues of information leakage, and test the generalizability of our models on the new dataset.
• Score: 0.7388859384645262
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Cylindrical Algebraic Decomposition (CAD) is a key proof technique for formal verification of cyber-physical systems. CAD is computationally expensive, with worst-case doubly-exponential complexity. Selecting an optimal variable ordering is paramount to efficient use of CAD. Prior work has demonstrated that machine learning can be useful in determining efficient variable orderings. Much of this work has been driven by CAD problems extracted from applications of the MetiTarski theorem prover. In this paper, we revisit this prior work and consider issues of bias in existing training and test data. We observe that the classical MetiTarski benchmarks are heavily biased towards particular variable orderings. To address this, we apply symmetries to create a new dataset containing more than 41K MetiTarski challenges designed to remove bias. Furthermore, we evaluate issues of information leakage, and test the generalizability of our models on the new dataset.

Related papers

• ReasonAgain: Using Extractable Symbolic Programs to Evaluate Mathematical Reasoning [54.70811660561151]
  Existing math datasets evaluate the reasoning abilities of large language models (LLMs) by either using the final answer or the intermediate reasoning steps derived from static examples. We seek to use symbolic programs as a means for automated evaluation if a model can consistently produce correct final answers across various inputs to the program. We observe significant accuracy drops using our proposed evaluation compared with original static examples, suggesting the fragility of math reasoning in state-of-the-art LLMs.
  arXiv  Detail & Related papers  (2024-10-24T18:02:37Z)
• CorDA: Context-Oriented Decomposition Adaptation of Large Language Models for Task-Aware Parameter-Efficient Fine-tuning [101.81127587760831]
  Current fine-tuning methods build adapters widely of the context of downstream task to learn, or the context of important knowledge to maintain. We propose CorDA, a Context-oriented Decomposition Adaptation method that builds learnable task-aware adapters. Our method enables two options, the knowledge-preserved adaptation and the instruction-previewed adaptation.
  arXiv  Detail & Related papers  (2024-06-07T19:10:35Z)
• Robust Capped lp-Norm Support Vector Ordinal Regression [85.84718111830752]
  Ordinal regression is a specialized supervised problem where the labels show an inherent order. Support Vector Ordinal Regression, as an outstanding ordinal regression model, is widely used in many ordinal regression tasks. We introduce a new model, Capped $ell_p$-Norm Support Vector Ordinal Regression(CSVOR), that is robust to outliers.
  arXiv  Detail & Related papers  (2024-04-25T13:56:05Z)
• Boarding for ISS: Imbalanced Self-Supervised: Discovery of a Scaled Autoencoder for Mixed Tabular Datasets [1.2289361708127877]
  The field of imbalanced self-supervised learning has not been extensively studied. Existing research has predominantly focused on image datasets. We propose a novel metric to balance learning: a Multi-Supervised Balanced MSE.
  arXiv  Detail & Related papers  (2024-03-23T10:37:22Z)
• Lessons on Datasets and Paradigms in Machine Learning for Symbolic Computation: A Case Study on CAD [0.0]
  This study reports lessons on the importance of analysing datasets prior to machine learning. We present results for a particular case study, the selection of variable ordering for cylindrical algebraic decomposition. We introduce an augmentation technique for systems that allows us to balance and further augment the dataset.
  arXiv  Detail & Related papers  (2024-01-24T10:12:43Z)
• Data Augmentation for Mathematical Objects [0.0]
  We consider a dataset of non-linear problems and a problem of selecting a variable ordering for cylindrical decomposition. By swapping the variable names in already labelled problems, we generate new problem instances that do not require any further labelling. We find this augmentation increases the accuracy of ML by 63% on average.
  arXiv  Detail & Related papers  (2023-07-13T16:02:45Z)
• Machine Learning Capability: A standardized metric using case difficulty with applications to individualized deployment of supervised machine learning [2.2060666847121864]
  Model evaluation is a critical component in supervised machine learning classification analyses. Items Response Theory (IRT) and Computer Adaptive Testing (CAT) with machine learning can benchmark datasets independent of the end-classification results.
  arXiv  Detail & Related papers  (2023-02-09T00:38:42Z)
• Automatic Data Augmentation via Invariance-Constrained Learning [94.27081585149836]
  Underlying data structures are often exploited to improve the solution of learning tasks. Data augmentation induces these symmetries during training by applying multiple transformations to the input data. This work tackles these issues by automatically adapting the data augmentation while solving the learning task.
  arXiv  Detail & Related papers  (2022-09-29T18:11:01Z)
• Toward Learning Robust and Invariant Representations with Alignment Regularization and Data Augmentation [76.85274970052762]
  This paper is motivated by a proliferation of options of alignment regularizations. We evaluate the performances of several popular design choices along the dimensions of robustness and invariance. We also formally analyze the behavior of alignment regularization to complement our empirical study under assumptions we consider realistic.
  arXiv  Detail & Related papers  (2022-06-04T04:29:19Z)
• Provable Continual Learning via Sketched Jacobian Approximations [17.381658875470638]
  A popular approach to overcome forgetting is to regularize the loss function by penalizing models that perform poorly on previous tasks. We show that, even under otherwise ideal conditions, it can provably suffer catastrophic forgetting if the diagonal matrix is a poor approximation of the Hessian matrix of previous tasks. We propose a simple approach to overcome this: Regularizing training of a new task with sketches of the Jacobian matrix of past data.
  arXiv  Detail & Related papers  (2021-12-09T18:36:20Z)
• Supervised Quantile Normalization for Low-rank Matrix Approximation [50.445371939523305]
  We learn the parameters of quantile normalization operators that can operate row-wise on the values of $X$ and/or of its factorization $UV$ to improve the quality of the low-rank representation of $X$ itself. We demonstrate the applicability of these techniques on synthetic and genomics datasets.
  arXiv  Detail & Related papers  (2020-02-08T21:06:02Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.