Cover Image

ProofBridge: Auto-Formalization of Natural Language Proofs in Lean via Joint Embeddings

Fuente: arXiv

Saved in:

Bibliographic Details
Main Authors:	Jana, Prithwish, Kale, Kaan, Tanriverdi, Ahmet Ege, Song, Cruise, Vishwanath, Sriram, Ganesh, Vijay
Format:	Preprint
Published:	2025
Subjects:	Logic in Computer Science Artificial Intelligence I.2.3; I.2.7; F.4; F.3.1; I.2.6
Online Access:	Acceder al recurso
Tags:	Add Tag No Tags, Be the first to tag this record!

Similar Items

Formal Proofs as Structured Explanations: Proposing Several Tasks on Explainable Natural Language Inference
by: Abzianidze, Lasha
Published: (2023)

Unravelling Abstract Cyclic Proofs into Proofs by Induction
by: Grotenhuis, Lide, et al.
Published: (2026)

Test Case Features as Hyper-heuristics for Inductive Programming
by: McDaid, Edward, et al.
Published: (2024)

A Proof System with Causal Labels (Part II): checking Counterfactual Fairness
by: Ceragioli, Leonardo, et al.
Published: (2025)

A Proof System with Causal Labels (Part I): checking Individual Fairness and Intersectionality
by: Ceragioli, Leonardo, et al.
Published: (2025)

Instruction and Solution Probabilities as Heuristics for Inductive Programming
by: McDaid, Edward, et al.
Published: (2025)

OnlineProver: Experience with a Visualisation Tool for Teaching Formal Proofs
by: Perháč, Ján, et al.
Published: (2025)

Superpolynomial Length Lower Bounds for Tree-Like Semantic Proof Systems with Bounded Line Size
by: de Rezende, Susanna F., et al.
Published: (2026)

Proof-Carrying Neuro-Symbolic Code
by: Komendantskaya, Ekaterina
Published: (2025)

Ancestry Tree Clustering for Particle Filter Diversity Maintenance
by: Vallivaara, Ilari, et al.
Published: (2025)

Understanding Syllogistic Reasoning in LLMs from Formal and Natural Language Perspectives
by: Poddar, Aheli, et al.
Published: (2025)

Data Verification is the Future of Quantum Computing Copilots
by: Song, Junhao, et al.
Published: (2026)

Non-Compact Proofs
by: Artemov, Sergei
Published: (2025)

TerraFormer: Automated Infrastructure-as-Code with LLMs Fine-Tuned via Policy-Guided Verifier Feedback
by: Jana, Prithwish, et al.
Published: (2026)

The Rectilinear Marco Polo Problem
by: Gila, Ofek, et al.
Published: (2025)

Exponential Resolution Lower Bounds for Weak Pigeonhole Principle and Perfect Matching Formulas over Sparse Graphs
by: de Rezende, Susanna F., et al.
Published: (2019)

Yanasse: Finding New Proofs from Deep Vision's Analogies, Part 1
by: Linhares, Alexandre
Published: (2026)

Serial Properties, Selector Proofs, and the Provability of Consistency
by: Artemov, Sergei
Published: (2024)

Inductive First-Order Formula Synthesis by ASP: A Case Study in Invariant Inference
by: Yang, Ziyi, et al.
Published: (2026)

Reasoning and Planning with Dynamically Changing Norms
by: Olson, Taylor, et al.
Published: (2026)

A Rust-to-Lean Verification Pipeline with AI Provers: An Experience Report
by: Klaus, Natalia, et al.
Published: (2026)

A Coq-based Axiomatization of Tarski's Mereogeometry
by: Barlatier, Patrick, et al.
Published: (2025)

Algorithmic Trading Strategy Development and Optimisation
by: Yuan, Owen Nyo Wei, et al.
Published: (2026)

Liquid Amortization: Proving Amortized Complexity with LiquidHaskell (Functional Pearl)
by: van Brügge, Jan
Published: (2024)

Graph Colouring Is Hard on Average for Polynomial Calculus and Nullstellensatz
by: Conneryd, Jonas, et al.
Published: (2025)

On bounded depth proofs for Tseitin formulas on the grid; revisited
by: Håstad, Johan, et al.
Published: (2022)

Clique Is Hard on Average for Sherali-Adams with Bounded Coefficients
by: de Rezende, Susanna F., et al.
Published: (2024)

Supercritical Tradeoffs for Monotone Circuits
by: Göös, Mika, et al.
Published: (2024)

A Prescriptive Framework for Determining Optimal Days for Short-Term Traffic Counts
by: Mukwaya, Arthur, et al.
Published: (2025)

From Scientific Texts to Verifiable Code: Automating the Process with Transformers
by: Wang, Changjie, et al.
Published: (2025)

Tokenization Disparities as Infrastructure Bias: How Subword Systems Create Inequities in LLM Access and Efficiency
by: Teklehaymanot, Hailay Kidu, et al.
Published: (2025)

Mechanized Foundations of Structural Governance: Machine-Checked Proofs for Governed Intelligence
by: McCann, Alan L.
Published: (2026)

Development of Hybrid Artificial Intelligence Training on Real and Synthetic Data: Benchmark on Two Mixed Training Strategies
by: Wachter, Paul, et al.
Published: (2025)

Canonical for Automated Theorem Proving in Lean
by: Norman, Chase, et al.
Published: (2025)

A Sequent Calculus for General Inductive Definitions
by: Eede, Robbe Van den, et al.
Published: (2026)

The Effect of State Representation on LLM Agent Behavior in Dynamic Routing Games
by: Goodyear, Lyle, et al.
Published: (2025)

FastLEC: Parallel Datapath Equivalence Checking with Hybrid Engines
by: Zhang, Xindi, et al.
Published: (2025)

SPARQL in N3: SPARQL CONSTRUCT as a rule language for the Semantic Web (Extended Version)
by: Arndt, Dörthe, et al.
Published: (2025)

The Stable Model Semantics for Higher-Order Logic Programming
by: Bogaerts, Bart, et al.
Published: (2024)

Greedy Spanners in Euclidean Spaces Admit Sublinear Separators
by: Le, Hung, et al.
Published: (2021)