Pith Number

pith:SMEZMH2X

pith:2025:SMEZMH2XHN3UOKTAYVYDTMSQTG

not attested not anchored not stored refs pending

A Neuro-Symbolic Approach for Reliable Proof Generation with LLMs: A Case Study in Euclidean Geometry

Dafna Shahaf, Eitan Stern, Oren Sultan

Retrieving similar proofs and verifier feedback boosts an LLM's geometry proof accuracy by 58 to 70 percent.

arxiv:2505.14479 v9 · 2025-05-20 · cs.AI · cs.CL

Open paper page JSON Open Graph Bundle Merged state Verified badge What is a Pith Number?

Add to your LaTeX paper

\usepackage{pith}
\pithnumber{SMEZMH2XHN3UOKTAYVYDTMSQTG}

Prints a linked badge after your title and injects PDF metadata. Compiles on arXiv. Learn more · Embed verified badge

Record completeness

1 Bitcoin timestamp

2 Internet Archive

3 Author claim open · sign in to claim

4 Citations open

5 Replications open

✓ Portable graph bundle live · download bundle · merged state

The bundle contains the canonical record plus signed events. A mirror can host it anywhere and recompute the same current state with the deterministic merge algorithm.

Claims

C1strongest claim

We demonstrate that our method significantly improves proof accuracy for OpenAI's o1 model (58%-70% improvement); both analogous problems and the verifier's feedback contribute to these gains.

C2weakest assumption

The formal verifier can accurately evaluate generated proofs and provide feedback that helps the LLM fix errors, assuming the verifier is complete for the problem domain and the feedback is effectively usable by the model.

C3one line summary

A neuro-symbolic approach using analogous problem retrieval and formal verification feedback improves LLM proof generation accuracy on Euclidean geometry problems by 58-70% for the o1 model.

Formal links

2 machine-checked theorem links

Cited by

2 papers in Pith

Unlocking LLM Creativity in Science through Analogical Reasoning

LLMs with in-context learning for Algorithmic Theoretical Physics

Receipt and verification

First computed	2026-05-26T01:03:12.739303Z
Builder	pith-number-builder-2026-05-17-v1
Signature	Pith Ed25519 (`pith-v1-2026-05`) · public key
Schema	pith-number/v1.0

Canonical hash

9309961f573b77472a60c57039b25099848211aeae4c99de92d92b2ca284b783

Aliases

arxiv: 2505.14479 · arxiv_version: 2505.14479v9 · doi: 10.48550/arxiv.2505.14479 · pith_short_12: SMEZMH2XHN3U · pith_short_16: SMEZMH2XHN3UOKTA · pith_short_8: SMEZMH2X

Agent API

Resolver JSON Graph JSON Events JSON Schema Signing key

Verify this Pith Number yourself

curl -sH 'Accept: application/ld+json' https://pith.science/pith/SMEZMH2XHN3UOKTAYVYDTMSQTG \
  | jq -c '.canonical_record' \
  | python3 -c "import sys,json,hashlib; b=json.dumps(json.loads(sys.stdin.read()), sort_keys=True, separators=(',',':'), ensure_ascii=False).encode(); print(hashlib.sha256(b).hexdigest())"
# expect: 9309961f573b77472a60c57039b25099848211aeae4c99de92d92b2ca284b783

Canonical record JSON

{
  "metadata": {
    "abstract_canon_sha256": "6e8a0a6c6a58a36468481d6796d1d1b33d52c5b4fbb664e0ada189d181f95f47",
    "cross_cats_sorted": [
      "cs.CL"
    ],
    "license": "http://arxiv.org/licenses/nonexclusive-distrib/1.0/",
    "primary_cat": "cs.AI",
    "submitted_at": "2025-05-20T15:13:32Z",
    "title_canon_sha256": "0efb8506f134bc83a6392e5fb9e845ddcb611ecaccbc3ebe2dcbc28c234978af"
  },
  "schema_version": "1.0",
  "source": {
    "id": "2505.14479",
    "kind": "arxiv",
    "version": 9
  }
}