Papers Mathematical Proofs
“Mathematical Proofs” 태그가 달린 논문 90편 · 필터 해제
Prover Agent: An Agent-based Framework for Formal Mathematical Proofs
We present Prover Agent, a novel AI agent for automated theorem proving that integrates large language models (LLMs) with a formal proof assistant, Lean. Prover Agent coordinates an informal reasoning LLM, a formal prove…
AI AgentAutomated Theorem ProvingMathematical ProofsThe Alignment Trap: Complexity Barriers
This paper argues that AI alignment is not merely difficult, but is founded on a fundamental logical contradiction. We first establish The Enumeration Paradox: we use machine learning precisely because we cannot enumerat…
Mathematical ProofsStepProof: Step-by-step verification of natural language mathematical proofs
Interactive theorem provers (ITPs) are powerful tools for the formal verification of mathematical proofs down to the axiom level. However, their lack of a natural language interface remains a significant limitation. Rece…
Mathematical ProofsSentenceLeanTutor: A Formally-Verified AI Tutor for Mathematical Proofs
We present LeanTutor, a Large Language Model (LLM)-based tutoring system for math proofs. LeanTutor interacts with the student in natural language, formally verifies student-written math proofs in Lean, generates correct…
Large Language ModelMathMathematical ProofsBeyond Chemical QA: Evaluating LLM's Chemical Reasoning with Modular Chemical Operations
While large language models (LLMs) with Chain-of-Thought (CoT) reasoning excel in mathematics and coding, their potential for systematic reasoning in chemistry, a domain demanding rigorous structural analysis for real-wo…
Chemical Reaction PredictionDrug DesignMathematical ProofsHybridProver: Augmenting Theorem Proving with LLM-Driven Proof Synthesis and Refinement
Formal methods is pivotal for verifying the reliability of critical systems through rigorous mathematical proofs. However, its adoption is hindered by labor-intensive manual proofs and the expertise required to use theor…
Automated Theorem ProvingMathematical ProofsIdentification of Probabilities of Causation: A Complete Characterization
Probabilities of causation are fundamental to modern decision-making. Pearl first introduced three binary probabilities of causation, and Tian and Pearl later derived tight bounds for them using Balke's linear programmin…
Decision MakingMathematical ProofsProvably safe and human-like car-following behaviors: Part 2. A parsimonious multi-phase model with projected braking
Ensuring safe and human-like trajectory planning for automated vehicles amidst real-world uncertainties remains a critical challenge. While existing car-following models often struggle to consistently provide rigorous sa…
Mathematical ProofsTrajectory PlanningA Theoretical Analysis of Compositional Generalization in Neural Networks: A Necessary and Sufficient Condition
Compositional generalization is a crucial property in artificial intelligence, enabling models to handle novel combinations of known components. While most deep learning models lack this capability, certain models succee…
Mathematical ProofsNeurodivergent Influenceability as a Contingent Solution to the AI Alignment Problem
The AI alignment problem, which focusses on ensuring that artificial intelligence (AI), including AGI and ASI, systems act according to human values, presents profound challenges. With the progression from narrow AI to A…
Experimental DesignMathematical ProofsHierarchical Attention Generates Better Proofs
Large language models (LLMs) have shown promise in formal theorem proving, but their token-level processing often fails to capture the inherent hierarchical nature of mathematical proofs. We introduce \textbf{Hierarchica…
Automated Theorem ProvingMathematical ProofsMathematical ReasoningStatistical Guarantees in Synthetic Data through Conformal Adversarial Generation
The generation of high-quality synthetic data presents significant challenges in machine learning research, particularly regarding statistical fidelity and uncertainty quantification. Existing generative models produce c…
Conformal PredictionMathematical ProofsPredictionUncertainty QuantificationMathematical Approach in Hybrid Beamforming for ISAC Systems
This document serves as supplementary material for a journal paper submission, presenting detailed mathematical proofs and derivations that support the results outlined in the main manuscript. In this work, we formulate …
Integrated sensing and communicationISACMathematical ProofsBoundary Effects in Biological Planar Networks: Pentagons Dominate Marginal Cells
The topological and geometrical features at the boundary zone of planar polygonal networks remain poorly understood. Based on observations and mathematical proofs, we propose that marginal cells in Pyropia haitanensis th…
Mathematical ProofsFence Theorem: Preprocessing is Dual-Objective Semantic Structure Isolator in 3D Anomaly Detection
3D anomaly detection (AD) is prominent but difficult due to lacking a unified theoretical foundation for preprocessing design. We establish the Fence Theorem, formalizing preprocessing as a dual-objective semantic isolat…
3D Anomaly DetectionAnomaly DetectionMathematical ProofsPatch Matching+1Theorem Prover as a Judge for Synthetic Data Generation
The demand for synthetic data in mathematical reasoning has increased due to its potential to enhance the mathematical capabilities of large language models (LLMs). However, ensuring the validity of intermediate reasonin…
Mathematical ProofsMathematical Reasoningreinforcement-learningReinforcement Learning+1Efficient Long-Decoding Inference with Reasoning-Aware Attention Sparsity
Large Language Models (LLMs) have demonstrated strong capabilities across various domains, with recent advancements in challenging reasoning tasks such as mathematics and programming. However, solving reasoning tasks oft…
Mathematical ProofsGenerating Millions Of Lean Theorems With Proofs By Exploring State Transition Graphs
Large Language Models (LLMs) have demonstrated significant potential in generating mathematical proofs. However, a persistent challenge is that LLMs occasionally make mistakes, while even a minor mistake can invalidate a…
Automated Theorem ProvingMathematical ProofsAutomating Mathematical Proof Generation Using Large Language Model Agents and Knowledge Graphs
Large Language Models have demonstrated remarkable capabilities in natural language processing tasks, including mathematical problem-solving that requires multi-step logical reasoning. However, challenges persist in auto…
Formal LogicKnowledge GraphsLanguage ModelingLanguage Modelling+5LemmaHead: RAG Assisted Proof Generation Using Large Language Models
Developing the logic necessary to solve mathematical problems or write mathematical proofs is one of the more difficult objectives for large language models (LLMS). Currently, the most popular methods in literature consi…
Automated Theorem ProvingMathematical ProofsMathematical ReasoningRAG+1