paper-with-me

Papers

Generating Natural Language Proofs with Verifier-Guided Search

2022-05-25 · Kaiyu Yang, Jia Deng, Danqi Chen

Reasoning over natural language is a challenging problem in NLP. In this work, we focus on proof generation: Given a hypothesis and a set of supporting facts, the model generates a proof tree indicating how to derive the hypothesis from supporting facts. Compared to generating the entire proof in one shot, stepwise generation can better exploit the compositionality and generalize to longer proofs but has achieved limited success on real-world data. Existing stepwise methods struggle to generate proof steps that are both logically valid and relevant to the hypothesis. Instead, they tend to hallucinate invalid steps given the hypothesis. In this paper, we present a novel stepwise method, NLProofS (Natural Language Proof Search), which learns to generate relevant steps conditioning on the hypothesis. At the core of our approach, we train an independent verifier to check the validity of the proof steps to prevent hallucination. Instead of generating steps greedily, we search for proofs maximizing a global proof score judged by the verifier. NLProofS achieves state-of-the-art performance on EntailmentBank and RuleTaker. Specifically, it improves the correctness of predicted proofs from 27.7% to 33.3% in the distractor setting of EntailmentBank, demonstrating the effectiveness of NLProofS in generating challenging human-authored proofs.

📄 PDF Abstract BibTeX arXiv:2205.12443

Code (1)

princeton-nlp/NLProofS 공식 구현 pytorch

Tasks

Hallucinationvalid

Similar Papers 제목 키워드 기반

Do We Need Frontier Models to Verify Mathematical Proofs?

2026-04-02 · Aaditya Naik, Guruprerana Shabadi, Rajeev Alur, Mayur Naik arxiv

Advances in training, post-training, and inference-time methods have enabled frontier reasoning models to win gold medals in math competitions and settle challenging open problems. Gaining trust in the responses of these…

Neural Interactive Proofs

2024-12-12 · Lewis Hammond, Sam Adam-Day

We consider the problem of how a trusted, but computationally bounded agent (a 'verifier') can learn to interact with one or more powerful but untrusted agents ('provers') in order to solve a given task. More specificall…

Certified Program Synthesis with a Multi-Modal Verifier

2026-04-17 · Yueyang Feng, Dipesh Kafle, Vladimir Gladshtein, Vitaly Kurin 외 arxiv

Certified program synthesis (aka vericoding) is the process of automatically generating a program, its formal specification, and a machine-checkable proof of their alignment from a natural-language description. Two chall…

Program Synthesis

Laurel: Unblocking Automated Verification with Large Language Models

2024-05-27 · Eric Mugnier, Emmanuel Anaya Gonzalez, Ranjit Jhala, Nadia Polikarpova 외

Program verifiers such as Dafny automate proofs by outsourcing them to an SMT solver. This automation is not perfect, however, and the solver often requires hints in the form of assertions, creating a burden for the proo…

LEMMA

LeanTutor: A Formally-Verified AI Tutor for Mathematical Proofs

2025-06-10 · Manooshree Patel, Rayna Bhattacharyya, Thomas Lu, Arnav Mehta 외

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 Proofs