Cover Image

Natural Language Translation of Formal Proofs through Informalization of Proof Steps and Recursive Summarization along Proof Structure

Fuente: arXiv

Saved in:

Bibliographic Details
Main Authors:	Hattori, Seiji, Matsuzaki, Takuya, Fujiwara, Makoto
Format:	Preprint
Published:	2025
Subjects:	Computation and Language
Online Access:	Acceder al recurso
Tags:	Add Tag No Tags, Be the first to tag this record!

Similar Items

From Informal to Formal -- Incorporating and Evaluating LLMs on Natural Language Requirements to Verifiable Formal Proofs
by: Cao, Jialun, et al.
Published: (2025)

Hilbert: Recursively Building Formal Proofs with Informal Reasoning
by: Varambally, Sumanth, et al.
Published: (2025)

Translating Informal Proofs into Formal Proofs Using a Chain of States
by: Wang, Ziyu, et al.
Published: (2025)

A Natural Formalized Proof Language
by: Xie, Lihan, et al.
Published: (2024)

FormalProofBench: Can Models Write Graduate Level Math Proofs That Are Formally Verified?
by: Ravi, Nikil, et al.
Published: (2026)

Exploring the Role of Reasoning Structures for Constructing Proofs in Multi-Step Natural Language Reasoning with Large Language Models
by: Zheng, Zi'ou, et al.
Published: (2024)

Autograding Mathematical Induction Proofs with Natural Language Processing
by: Zhao, Chenyan, et al.
Published: (2024)

Reliable Fine-Grained Evaluation of Natural Language Math Proofs
by: Ma, Wenjie, et al.
Published: (2025)

Advocate for Complete Benchmarks for Formal Reasoning with Formal/Informal Statements and Formal/Informal Proofs
by: Yousefzadeh, Roozbeh, et al.
Published: (2025)

Proof-RM: A Scalable and Generalizable Reward Model for Math Proof
by: Yang, Haotong, et al.
Published: (2026)

Not All Proofs Are Equal: Evaluating LLM Proof Quality Beyond Correctness
by: Petrov, Ivo, et al.
Published: (2026)

APE-Bench: Evaluating Automated Proof Engineering for Formal Math Libraries
by: Xin, Huajian, et al.
Published: (2025)

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

Neural Theorem Proving: Generating and Structuring Proofs for Formal Verification
by: Rao, Balaji, et al.
Published: (2025)

Proof Flow: Preliminary Study on Generative Flow Network Language Model Tuning for Formal Reasoning
by: Ho, Matthew, et al.
Published: (2024)

The Proof is in the Almond Cookies
by: van Trijp, Remi, et al.
Published: (2025)

Proof2Hybrid: Automatic Mathematical Benchmark Synthesis for Proof-Centric Problems
by: Peng, Yebo, et al.
Published: (2025)

ProofBridge: Auto-Formalization of Natural Language Proofs in Lean via Joint Embeddings
by: Jana, Prithwish, et al.
Published: (2025)

The Open Proof Corpus: A Large-Scale Study of LLM-Generated Mathematical Proofs
by: Dekoninck, Jasper, et al.
Published: (2025)

Cypher is Turing-Complete: A Formal Proof via 2-Counter Machine Simulation
by: Halftermeyer, Pierre
Published: (2026)

Solving Inequality Proofs with Large Language Models
by: Lu, Pan, et al.
Published: (2025)

Are LLMs Rigorous Logical Reasoners? Empowering Natural Language Proof Generation by Stepwise Decoding with Contrastive Learning
by: Su, Ying, et al.
Published: (2023)

Coinductive Proofs for Temporal Hyperliveness
by: Correnson, Arthur, et al.
Published: (2025)

Symmetric Proofs of Parameterized Programs
by: Cheng, Ruotong, et al.
Published: (2026)

ProofWala: A Framework for Multilingual Proof Data Synthesis and Theorem-Proving
by: Thakur, Amitayush, et al.
Published: (2025)

Mechanised Hypersafety Proofs about Structured Data: Extended Version
by: Gladshtein, Vladimir, et al.
Published: (2024)

More Church-Rosser Proofs in BELUGA
by: Momigliano, Alberto, et al.
Published: (2024)

MiniF2F in Rocq: Automatic Translation Between Proof Assistants -- A Case Study
by: Viennot, Jules, et al.
Published: (2025)

Aletheia tackles FirstProof autonomously
by: Feng, Tony, et al.
Published: (2026)

Hierarchical Attention Generates Better Proofs
by: Chen, Jianlong, et al.
Published: (2025)

ProofSketch: Efficient Verified Reasoning for Large Language Models
by: Sheshanarayana, Disha, et al.
Published: (2025)

ProofOptimizer: Training Language Models to Simplify Proofs without Human Demonstrations
by: Gu, Alex, et al.
Published: (2025)

An Elementary Proof of the FMP for Kleene Algebra
by: Kappé, Tobias
Published: (2022)

PCRLLM: Proof-Carrying Reasoning with Large Language Models under Stepwise Logical Constraints
by: Li, Tangrui, et al.
Published: (2025)

Cyclic Proofs in Hoare Logic and its Reverse
by: Brotherston, James, et al.
Published: (2025)

Pleasant Imperative Program Proofs with GallinaC
by: Fort, Frédéric, et al.
Published: (2025)

Proof or Bluff? Evaluating LLMs on 2025 USA Math Olympiad
by: Petrov, Ivo, et al.
Published: (2025)

Enabling AI ASICs for Zero Knowledge Proof
by: Tong, Jianming, et al.
Published: (2026)

MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data
by: Huang, Yinya, et al.
Published: (2024)

LogicTree: Structured Proof Exploration for Coherent and Rigorous Logical Reasoning with Large Language Models
by: He, Kang, et al.
Published: (2025)