3D-Prover: Diversity Driven Theorem Proving With Determinantal Point Processes

• URL: http://arxiv.org/abs/2410.11133v2
• Date: Tue, 28 Oct 2025 00:10:02 GMT
• Title: 3D-Prover: Diversity Driven Theorem Proving With Determinantal Point Processes
• Abstract summary: A key challenge in automated formal reasoning is the intractable search space, which grows exponentially with the depth of the proof.<n>We propose a novel filtering mechanism which leverages semantically diverse and high quality tactics.<n>We show that our approach leads to an increase in the overall proof rate, as well as a significant improvement in the tactic success rate, execution time and diversity.
• Score: 17.379356401253986
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: A key challenge in automated formal reasoning is the intractable search space, which grows exponentially with the depth of the proof. This branching is caused by the large number of candidate proof tactics which can be applied to a given goal. Nonetheless, many of these tactics are semantically similar or lead to an execution error, wasting valuable resources in both cases. We address the problem of effectively pruning this search, using only synthetic data generated from previous proof attempts. We first demonstrate that it is possible to generate semantically aware tactic representations which capture the effect on the proving environment, likelihood of success, and execution time. We then propose a novel filtering mechanism which leverages these representations to select semantically diverse and high quality tactics, using Determinantal Point Processes. Our approach, 3D- Prover, is designed to be general, and to augment any underlying tactic generator. We demonstrate the effectiveness of 3D-Prover on the miniF2F and LeanDojo benchmarks by augmenting popular open source proving LLMs. We show that our approach leads to an increase in the overall proof rate, as well as a significant improvement in the tactic success rate, execution time and diversity. We make our code available at https://github.com/sean-lamont/3D-Prover.

Related papers

• CoverPrune: Coverage-Driven Token Pruning for 3D VLMs via Optimal Transport [50.2610873651284]
  Existing token pruning methods rely on diversity-based selection, discarding similar tokens to maximize dispersion.<n>In 3D environments, this approach frequently drops representative prototype tokens in favor of outliers.<n>We propose a paradigm shift for 3D VLM token pruning: from maximizing OT to preserving visual evidence coverage.
  arXiv  Detail & Related papers  (2026-08-13T13:29:15Z)
• Learning to Reason Efficiently with A* Post-Training [119.18396754931602]
  We investigate whether large language models can learn to generate correct and efficient proofs with guidance from A* search.<n> Empirically, we find that Llama-3.2 models in the 1B--3B range benefit substantially from A* post training.<n>On larger search spaces, models trained with imperfects exhibit superior accuracy.
  arXiv  Detail & Related papers  (2026-05-23T14:28:57Z)
• A3R: Agentic Affordance Reasoning via Cross-Dimensional Evidence in 3D Gaussian Scenes [115.37391672369914]
  Affordance reasoning aims to identify the region that supports the action specified by a given text instruction in complex environments.<n>We propose A3R, an agentic affordance reasoning framework that enables an MLLM-based policy to iteratively select evidence acquisition actions.<n>Experiments on scene-level benchmarks show that A3R consistently surpasses static one-shot baselines.
  arXiv  Detail & Related papers  (2026-04-02T10:40:51Z)
• PointCoT: A Multi-modal Benchmark for Explicit 3D Geometric Reasoning [82.55361351483005]
  We present PointCoT, a novel framework that empowers MLLMs with explicit Chain-of-Thought (CoT) reasoning for 3D data.<n>By leveraging a dual-stream multi-modal architecture, our method synergizes semantic appearance with geometric truth.
  arXiv  Detail & Related papers  (2026-02-27T11:47:45Z)
• Prism: Efficient Test-Time Scaling via Hierarchical Search and Self-Verification for Discrete Diffusion Language Models [96.0074341403456]
  Inference-time compute has re-emerged as a practical way to improve LLM reasoning.<n>Most test-time scaling (TTS) algorithms rely on autoregressive decoding.<n>We propose Prism, an efficient TTS framework for dLLMs.
  arXiv  Detail & Related papers  (2026-02-02T09:14:51Z)
• Universal and Transferable Adversarial Attack on Large Language Models Using Exponentiated Gradient Descent [1.1187085721899017]
  Large language models (LLMs) are increasingly deployed in critical applications.<n>LLMs remain vulnerable to jailbreak attacks enabled by crafted adversarial triggers appended to user prompts.<n>We propose an intrinsic optimization method which directly optimize relaxed one-hot encodings of the adversarial suffix tokens.
  arXiv  Detail & Related papers  (2025-08-20T17:03:32Z)
• Fractured Chain-of-Thought Reasoning [61.647243580650446]
  We introduce Fractured Sampling, a unified inference-time strategy that interpolates between full CoT and solution-only sampling.<n>We show that Fractured Sampling consistently achieves superior accuracy-cost trade-offs, yielding steep log-linear scaling gains in Pass@k versus token budget.
  arXiv  Detail & Related papers  (2025-05-19T11:30:41Z)
• Adversarial Attack on Large Language Models using Exponentiated Gradient Descent [1.1187085721899017]
  Large Language Models are vulnerable to jailbreaking attacks.<n>We develop an intrinsic optimization technique using exponentiated gradient descent.<n>We show that the technique achieves a higher success rate with great efficiency compared to three other state-of-the-art jailbreaking techniques.
  arXiv  Detail & Related papers  (2025-05-14T21:50:46Z)
• Unveiling the Magic of Code Reasoning through Hypothesis Decomposition and Amendment [54.62926010621013]
  We introduce a novel task, code reasoning, to provide a new perspective for the reasoning abilities of large language models. We summarize three meta-benchmarks based on established forms of logical reasoning, and instantiate these into eight specific benchmark tasks. We present a new pathway exploration pipeline inspired by human intricate problem-solving methods.
  arXiv  Detail & Related papers  (2025-02-17T10:39:58Z)
• Proving Theorems Recursively [80.42431358105482]
  We propose POETRY, which proves theorems in a level-by-level manner. Unlike previous step-by-step methods, POETRY searches for a sketch of the proof at each level. We observe a substantial increase in the maximum proof length found by POETRY, from 10 to 26.
  arXiv  Detail & Related papers  (2024-05-23T10:35:08Z)
• Two Heads are Better than One: Towards Better Adversarial Robustness by Combining Transduction and Rejection [34.0779912244438]
  We show that a novel application of Tramer's classifier-to-detector technique in the transductive setting can give significantly improved sample-complexity for robust generalization. While our theoretical construction is computationally inefficient, it guides us to identify an efficient transductive algorithm to learn a selective model.
  arXiv  Detail & Related papers  (2023-05-27T17:06:17Z)
• 3D-QueryIS: A Query-based Framework for 3D Instance Segmentation [74.6998931386331]
  Previous methods for 3D instance segmentation often maintain inter-task dependencies and the tendency towards a lack of robustness. We propose a novel query-based method, termed as 3D-QueryIS, which is detector-free, semantic segmentation-free, and cluster-free. Our 3D-QueryIS is free from the accumulated errors caused by the inter-task dependencies.
  arXiv  Detail & Related papers  (2022-11-17T07:04:53Z)
• Versatile Weight Attack via Flipping Limited Bits [68.45224286690932]
  We study a novel attack paradigm, which modifies model parameters in the deployment stage. Considering the effectiveness and stealthiness goals, we provide a general formulation to perform the bit-flip based weight attack. We present two cases of the general formulation with different malicious purposes, i.e., single sample attack (SSA) and triggered samples attack (TSA)
  arXiv  Detail & Related papers  (2022-07-25T03:24:58Z)
• Efficient Neural Network Analysis with Sum-of-Infeasibilities [64.31536828511021]
  Inspired by sum-of-infeasibilities methods in convex optimization, we propose a novel procedure for analyzing verification queries on networks with extensive branching functions. An extension to a canonical case-analysis-based complete search procedure can be achieved by replacing the convex procedure executed at each search state with DeepSoI.
  arXiv  Detail & Related papers  (2022-03-19T15:05:09Z)
• Diverse Knowledge Distillation for End-to-End Person Search [81.4926655119318]
  Person search aims to localize and identify a specific person from a gallery of images. Recent methods can be categorized into two groups, i.e., two-step and end-to-end approaches. We propose a simple yet strong end-to-end network with diverse knowledge distillation to break the bottleneck.
  arXiv  Detail & Related papers  (2020-12-21T09:04:27Z)
• Weakly Supervised Generative Network for Multiple 3D Human Pose Hypotheses [74.48263583706712]
  3D human pose estimation from a single image is an inverse problem due to the inherent ambiguity of the missing depth. We propose a weakly supervised deep generative network to address the inverse problem.
  arXiv  Detail & Related papers  (2020-08-13T09:26:01Z)
• Robust Uncertainty-Aware Multiview Triangulation [20.02647320786556]
  We propose a robust and efficient method for multiview triangulation and uncertainty estimation. Our contribution is threefold: First, we propose an outlier rejection scheme using two-view RANSAC with the midpoint method. Second, we compare different local optimization methods for refining the initial solution and the inlier set. Third, we model the uncertainty of a triangulated point as a function of three factors: the number of cameras, the mean reprojection error and the maximum parallax angle.
  arXiv  Detail & Related papers  (2020-08-04T00:47:42Z)
• TEAM: We Need More Powerful Adversarial Examples for DNNs [6.7943676146532885]
  Adversarial examples can lead to misclassification of deep neural networks (DNNs) We propose a novel method to generate more powerful adversarial examples than previous methods. Our method can reliably produce adversarial examples with 100% attack success rate (ASR) while only by smaller perturbations.
  arXiv  Detail & Related papers  (2020-07-31T04:11:02Z)
• Deep Spatial Gradient and Temporal Depth Learning for Face Anti-spoofing [61.82466976737915]
  Depth supervised learning has been proven as one of the most effective methods for face anti-spoofing. We propose a new approach to detect presentation attacks from multiple frames based on two insights. The proposed approach achieves state-of-the-art results on five benchmark datasets.
  arXiv  Detail & Related papers  (2020-03-18T06:11:20Z)
• Efficient and Robust Registration on the 3D Special Euclidean Group [11.805432720871263]
  We present an accurate, robust and fast method for registration of 3D scans. We exploit the geometric properties of Lie groups as well as the robustness afforded by an iteratively reweighted least squares optimization.
  arXiv  Detail & Related papers  (2019-04-11T03:52:42Z)

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.