<?xml version="1.0" encoding="UTF-8"?>
<modsCollection xmlns="http://www.loc.gov/mods/v3">
<mods ID="lama-etal-2024-benchmarking">
    <titleInfo>
        <title>Benchmarking Automated Theorem Proving with Large Language Models</title>
    </titleInfo>
    <name type="personal">
        <namePart type="given">Vanessa</namePart>
        <namePart type="family">Lama</namePart>
        <role>
            <roleTerm authority="marcrelator" type="text">author</roleTerm>
        </role>
    </name>
    <name type="personal">
        <namePart type="given">Catherine</namePart>
        <namePart type="family">Ma</namePart>
        <role>
            <roleTerm authority="marcrelator" type="text">author</roleTerm>
        </role>
    </name>
    <name type="personal">
        <namePart type="given">Tirthankar</namePart>
        <namePart type="family">Ghosal</namePart>
        <role>
            <roleTerm authority="marcrelator" type="text">author</roleTerm>
        </role>
    </name>
    <originInfo>
        <dateIssued>2024-11</dateIssued>
    </originInfo>
    <typeOfResource>text</typeOfResource>
    <relatedItem type="host">
        <titleInfo>
            <title>Proceedings of the 1st Workshop on NLP for Science (NLP4Science)</title>
        </titleInfo>
        <name type="personal">
            <namePart type="given">Lotem</namePart>
            <namePart type="family">Peled-Cohen</namePart>
            <role>
                <roleTerm authority="marcrelator" type="text">editor</roleTerm>
            </role>
        </name>
        <name type="personal">
            <namePart type="given">Nitay</namePart>
            <namePart type="family">Calderon</namePart>
            <role>
                <roleTerm authority="marcrelator" type="text">editor</roleTerm>
            </role>
        </name>
        <name type="personal">
            <namePart type="given">Shir</namePart>
            <namePart type="family">Lissak</namePart>
            <role>
                <roleTerm authority="marcrelator" type="text">editor</roleTerm>
            </role>
        </name>
        <name type="personal">
            <namePart type="given">Roi</namePart>
            <namePart type="family">Reichart</namePart>
            <role>
                <roleTerm authority="marcrelator" type="text">editor</roleTerm>
            </role>
        </name>
        <originInfo>
            <publisher>Association for Computational Linguistics</publisher>
            <place>
                <placeTerm type="text">Miami, FL, USA</placeTerm>
            </place>
        </originInfo>
        <genre authority="marcgt">conference publication</genre>
    </relatedItem>
    <abstract>Theorem proving presents a significant challenge for large language models (LLMs) due to the requirement for formal proofs to be rigorously checked by proof assistants, such as Lean, eliminating any margin for error or hallucination. While existing LLM-based theorem provers attempt to operate autonomously, they often struggle with novel and complex theorems where human insights are essential. Lean Copilot is a novel framework that integrates LLM inference into the Lean proof assistant environment. In this work, we benchmark performance of several LLMs including general and math-specific models for theorem proving using the Lean Copilot framework. Our initial investigation suggests that a general-purpose large model like LLaMa-70B still has edge over math-specific smaller models for the task under consideration. We provide useful insights into the performance of different LLMs we chose for the task.</abstract>
    <identifier type="citekey">lama-etal-2024-benchmarking</identifier>
    <location>
        <url>https://aclanthology.org/2024.nlp4science-1.18</url>
    </location>
    <part>
        <date>2024-11</date>
        <extent unit="page">
            <start>208</start>
            <end>218</end>
        </extent>
    </part>
</mods>
</modsCollection>

%0 Conference Proceedings
%T Benchmarking Automated Theorem Proving with Large Language Models
%A Lama, Vanessa
%A Ma, Catherine
%A Ghosal, Tirthankar
%Y Peled-Cohen, Lotem
%Y Calderon, Nitay
%Y Lissak, Shir
%Y Reichart, Roi
%S Proceedings of the 1st Workshop on NLP for Science (NLP4Science)
%D 2024
%8 November
%I Association for Computational Linguistics
%C Miami, FL, USA
%F lama-etal-2024-benchmarking
%X Theorem proving presents a significant challenge for large language models (LLMs) due to the requirement for formal proofs to be rigorously checked by proof assistants, such as Lean, eliminating any margin for error or hallucination. While existing LLM-based theorem provers attempt to operate autonomously, they often struggle with novel and complex theorems where human insights are essential. Lean Copilot is a novel framework that integrates LLM inference into the Lean proof assistant environment. In this work, we benchmark performance of several LLMs including general and math-specific models for theorem proving using the Lean Copilot framework. Our initial investigation suggests that a general-purpose large model like LLaMa-70B still has edge over math-specific smaller models for the task under consideration. We provide useful insights into the performance of different LLMs we chose for the task.
%U https://aclanthology.org/2024.nlp4science-1.18
%P 208-218

Markdown (Informal)

[Benchmarking Automated Theorem Proving with Large Language Models](https://aclanthology.org/2024.nlp4science-1.18) (Lama et al., NLP4Science 2024)

• Benchmarking Automated Theorem Proving with Large Language Models (Lama et al., NLP4Science 2024)

ACL

• Vanessa Lama, Catherine Ma, and Tirthankar Ghosal. 2024. Benchmarking Automated Theorem Proving with Large Language Models. In Proceedings of the 1st Workshop on NLP for Science (NLP4Science), pages 208–218, Miami, FL, USA. Association for Computational Linguistics.