REVIEW 1 cited by
Getting More out of Large Language Models for Proofs
Not yet reviewed by Pith; the record is open.
This paper has not been read by Pith yet. Machine review is queued; the pith claim, tier, and objections will appear here once it completes.
SPECIMEN: schema-true, not a live event
T0 review · schema-true
One-sentence machine reading of the paper's core claim.
pith:XXXXXXXX · record.json · timestamp
Signed reviews
read the original abstract
Large language models have the potential to simplify formal theorem proving and make it more accessible. But how to get the most out of these models is still an open question. To answer this question, we take a step back and explore the failure cases of these models using common prompting-based techniques. Our talk will discuss these failure cases and what they can teach us about how to get more out of these models.
Forward citations
Cited by 1 Pith paper
-
A Case Study on the Effectiveness of LLMs in Verification with Proof Assistants
In an ablation across five LLMs and two Rocq projects, informed prompts with dependencies and in-file context produced the highest proof success (up to 52% of hs-to-coq theorems), and success fell sharply without context.
Discussion (0). Continue with ORCID to comment.