Towards Automated Functional Equation Proving: A Benchmark Dataset and A Domain-Specific In-Context Agent

• URL: http://arxiv.org/abs/2407.14521v1
• Date: Fri, 5 Jul 2024 15:59:16 GMT
• Title: Towards Automated Functional Equation Proving: A Benchmark Dataset and A Domain-Specific In-Context Agent
• Authors: Mahdi Buali, Robert Hoehndorf,
• Abstract summary: Automated Theorem Proving (ATP) faces challenges due to its complexity and computational demands. Recent work has explored using Large Language Models (LLMs) for ATP action selection, but these methods can be resource-intensive. This study introduces FEAS, an agent that enhances the COPRA in-context learning framework within Lean.
• Score: 1.006303657343407
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Automated Theorem Proving (ATP) faces challenges due to its complexity and computational demands. Recent work has explored using Large Language Models (LLMs) for ATP action selection, but these methods can be resource-intensive. This study introduces FEAS, an agent that enhances the COPRA in-context learning framework within Lean. FEAS refines prompt generation, response parsing, and incorporates domain-specific heuristics for functional equations. It introduces FunEq, a curated dataset of functional equation problems with varying difficulty. FEAS outperforms baselines on FunEq, particularly with the integration of domain-specific heuristics. The results demonstrate FEAS's effectiveness in generating and formalizing high-level proof strategies into Lean proofs, showcasing the potential of tailored approaches for specific ATP challenges.

Related papers

• Learning dynamical systems from data: Gradient-based dictionary optimization [0.8643517734716606]
  We present a novel gradient descent-based optimization framework for learning suitable basis functions from data. We show how it can be used in combination with EDMD, SINDy, and PDE-FIND.
  arXiv  Detail & Related papers  (2024-11-07T15:15:27Z)
• Entropy-Regularized Token-Level Policy Optimization for Language Agent Reinforcement [67.1393112206885]
  Large Language Models (LLMs) have shown promise as intelligent agents in interactive decision-making tasks. We introduce Entropy-Regularized Token-level Policy Optimization (ETPO), an entropy-augmented RL method tailored for optimizing LLMs at the token level. We assess the effectiveness of ETPO within a simulated environment that models data science code generation as a series of multi-step interactive tasks.
  arXiv  Detail & Related papers  (2024-02-09T07:45:26Z)
• TRIGO: Benchmarking Formal Mathematical Proof Reduction for Generative Language Models [68.65075559137608]
  We propose TRIGO, an ATP benchmark that not only requires a model to reduce a trigonometric expression with step-by-step proofs but also evaluates a generative LM's reasoning ability on formulas. We gather trigonometric expressions and their reduced forms from the web, annotate the simplification process manually, and translate it into the Lean formal language system. We develop an automatic generator based on Lean-Gym to create dataset splits of varying difficulties and distributions in order to thoroughly analyze the model's generalization ability.
  arXiv  Detail & Related papers  (2023-10-16T08:42:39Z)
• Transport Equation based Physics Informed Neural Network to predict the Yield Strength of Architected Materials [0.0]
  The PINN model showcases exceptional generalization capabilities, indicating its capacity to avoid overfitting with the provided dataset. The research underscores the importance of striking a balance between performance and computational efficiency while selecting an activation function for specific real-world applications.
  arXiv  Detail & Related papers  (2023-07-29T12:42:03Z)
• On the Integration of Physics-Based Machine Learning with Hierarchical Bayesian Modeling Techniques [0.0]
  This paper proposes to embed mechanics-based models into the mean function of a Gaussian Process (GP) model and characterize potential discrepancies through kernel machines. The stationarity of the kernel function is a difficult hurdle in the sequential processing of long data sets, resolved through hierarchical Bayesian techniques. Using numerical and experimental examples, potential applications of the proposed method to structural dynamics inverse problems are demonstrated.
  arXiv  Detail & Related papers  (2023-03-01T02:29:41Z)
• Offline Reinforcement Learning with Differentiable Function Approximation is Provably Efficient [65.08966446962845]
  offline reinforcement learning, which aims at optimizing decision-making strategies with historical data, has been extensively applied in real-life applications. We take a step by considering offline reinforcement learning with differentiable function class approximation (DFA) Most importantly, we show offline differentiable function approximation is provably efficient by analyzing the pessimistic fitted Q-learning algorithm.
  arXiv  Detail & Related papers  (2022-10-03T07:59:42Z)
• Data-Driven Reachability analysis and Support set Estimation with Christoffel Functions [8.183446952097528]
  We present algorithms for estimating the forward reachable set of a dynamical system. The produced estimate is the sublevel set of a function called an empirical inverse Christoffel function. In addition to reachability analysis, the same approach can be applied to general problems of estimating the support of a random variable.
  arXiv  Detail & Related papers  (2021-12-18T20:25:34Z)
• Scalable Gaussian Processes for Data-Driven Design using Big Data with Categorical Factors [14.337297795182181]
  Gaussian processes (GP) have difficulties in accommodating big datasets, categorical inputs, and multiple responses. We propose a GP model that utilizes latent variables and functions obtained through variational inference to address the aforementioned challenges simultaneously. Our approach is demonstrated for machine learning of ternary oxide materials and topology optimization of a multiscale compliant mechanism.
  arXiv  Detail & Related papers  (2021-06-26T02:17:23Z)
• Tesseract: Tensorised Actors for Multi-Agent Reinforcement Learning [92.05556163518999]
  MARL exacerbates matters by imposing various constraints on communication and observability. For value-based methods, it poses challenges in accurately representing the optimal value function. For policy gradient methods, it makes training the critic difficult and exacerbates the problem of the lagging critic. We show that from a learning theory perspective, both problems can be addressed by accurately representing the associated action-value function.
  arXiv  Detail & Related papers  (2021-05-31T23:08:05Z)
• Removing Bias in Multi-modal Classifiers: Regularization by Maximizing Functional Entropies [88.0813215220342]
  Some modalities can more easily contribute to the classification results than others. We develop a method based on the log-Sobolev inequality, which bounds the functional entropy with the functional-Fisher-information. On the two challenging multi-modal datasets VQA-CPv2 and SocialIQ, we obtain state-of-the-art results while more uniformly exploiting the modalities.
  arXiv  Detail & Related papers  (2020-10-21T07:40:33Z)
• Feature Quantization Improves GAN Training [126.02828112121874]
  Feature Quantization (FQ) for the discriminator embeds both true and fake data samples into a shared discrete space. Our method can be easily plugged into existing GAN models, with little computational overhead in training.
  arXiv  Detail & Related papers  (2020-04-05T04:06:50Z)

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.