Spaces:
Running
Running
Sophie
commited on
Commit
·
c1b045f
1
Parent(s):
a132e72
added 0 citation-weight case; ui updates
Browse files- .streamlit/config.toml +5 -0
- src/streamlit_app.py +158 -230
.streamlit/config.toml
ADDED
|
@@ -0,0 +1,5 @@
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 1 |
+
[theme]
|
| 2 |
+
base="light"
|
| 3 |
+
primaryColor="#8f00ff"
|
| 4 |
+
textColor="#262730"
|
| 5 |
+
font="sans-serif"
|
src/streamlit_app.py
CHANGED
|
@@ -1,7 +1,6 @@
|
|
| 1 |
import streamlit as st
|
| 2 |
-
|
| 3 |
import json
|
| 4 |
-
import numpy as np
|
| 5 |
from sentence_transformers import SentenceTransformer
|
| 6 |
import os
|
| 7 |
import boto3
|
|
@@ -9,8 +8,6 @@ import psycopg2
|
|
| 9 |
from psycopg2.extensions import connection
|
| 10 |
from pgvector.psycopg2 import register_vector
|
| 11 |
import re
|
| 12 |
-
import requests
|
| 13 |
-
from concurrent.futures import ThreadPoolExecutor, as_completed
|
| 14 |
from collections import defaultdict
|
| 15 |
from dotenv import load_dotenv
|
| 16 |
from latex_clean import clean_latex_for_display
|
|
@@ -18,7 +15,6 @@ from latex_clean import clean_latex_for_display
|
|
| 18 |
# Config
|
| 19 |
load_dotenv()
|
| 20 |
|
| 21 |
-
|
| 22 |
def get_rds_connection() -> connection:
|
| 23 |
region = os.getenv("AWS_REGION")
|
| 24 |
secret_arn = os.getenv("RDS_SECRET_ARN")
|
|
@@ -40,21 +36,6 @@ def get_rds_connection() -> connection:
|
|
| 40 |
register_vector(conn)
|
| 41 |
return conn
|
| 42 |
|
| 43 |
-
|
| 44 |
-
AVAILABLE_TAGS = {
|
| 45 |
-
"arXiv": [
|
| 46 |
-
"math.AC", "math.AG", "math.AP", "math.AT", "math.CA", "math.CO",
|
| 47 |
-
"math.CT", "math.CV", "math.DG", "math.DS", "math.FA", "math.GM",
|
| 48 |
-
"math.GN", "math.GR", "math.GT", "math.HO", "math.IT", "math.KT",
|
| 49 |
-
"math.LO", "math.MG", "math.MP", "math.NA", "math.NT", "math.OA",
|
| 50 |
-
"math.OC", "math.PR", "math.QA", "math.RA", "math.RT", "math.SG",
|
| 51 |
-
"math.SP", "math.ST", "Statistics Theory"
|
| 52 |
-
],
|
| 53 |
-
"Stacks Project": [
|
| 54 |
-
"Sets", "Schemes", "Algebraic Stacks", "Étale Cohomology"
|
| 55 |
-
]
|
| 56 |
-
}
|
| 57 |
-
|
| 58 |
ALLOWED_TYPES = [
|
| 59 |
"theorem", "lemma", "proposition", "corollary"
|
| 60 |
]
|
|
@@ -66,7 +47,6 @@ ARXIV_ID_RE = re.compile(
|
|
| 66 |
|
| 67 |
EMBED_TABLE = "theorem_embedding_qwen"
|
| 68 |
|
| 69 |
-
|
| 70 |
# Load the Embedding Model
|
| 71 |
@st.cache_resource
|
| 72 |
def load_model():
|
|
@@ -81,104 +61,11 @@ def infer_type(name: str) -> str:
|
|
| 81 |
if not name:
|
| 82 |
return "theorem"
|
| 83 |
lower = name.lower()
|
| 84 |
-
for t in
|
| 85 |
if t in lower:
|
| 86 |
return t
|
| 87 |
return "theorem"
|
| 88 |
|
| 89 |
-
# Load Data from RDS
|
| 90 |
-
@st.cache_data
|
| 91 |
-
def load_papers_from_rds():
|
| 92 |
-
"""
|
| 93 |
-
Loads the theorem data from the RDS database.
|
| 94 |
-
Returns a list of theorem dictionaries with all necessary fields.
|
| 95 |
-
"""
|
| 96 |
-
try:
|
| 97 |
-
conn = get_rds_connection()
|
| 98 |
-
cur = conn.cursor()
|
| 99 |
-
|
| 100 |
-
# Fetch all papers with their theorems
|
| 101 |
-
cur.execute("""
|
| 102 |
-
WITH latest_slogan AS (SELECT DISTINCT
|
| 103 |
-
ON (ts.theorem_id)
|
| 104 |
-
ts.theorem_id, ts.slogan_id, ts.slogan
|
| 105 |
-
FROM theorem_slogan ts
|
| 106 |
-
ORDER BY ts.theorem_id, ts.slogan_id DESC
|
| 107 |
-
)
|
| 108 |
-
SELECT p.paper_id,
|
| 109 |
-
p.title,
|
| 110 |
-
p.authors,
|
| 111 |
-
p.link,
|
| 112 |
-
p.last_updated,
|
| 113 |
-
p.summary,
|
| 114 |
-
p.journal_ref,
|
| 115 |
-
p.primary_category,
|
| 116 |
-
p.categories,
|
| 117 |
-
t.name AS theorem_name,
|
| 118 |
-
ls.slogan AS theorem_slogan,
|
| 119 |
-
t.body AS theorem_body
|
| 120 |
-
FROM paper p
|
| 121 |
-
JOIN theorem t ON t.paper_id = p.paper_id
|
| 122 |
-
LEFT JOIN latest_slogan ls ON ls.theorem_id = t.theorem_id
|
| 123 |
-
ORDER BY p.paper_id, t.name;
|
| 124 |
-
""")
|
| 125 |
-
|
| 126 |
-
rows = cur.fetchall()
|
| 127 |
-
cur.close()
|
| 128 |
-
conn.close()
|
| 129 |
-
|
| 130 |
-
all_theorems_data = []
|
| 131 |
-
for row in rows:
|
| 132 |
-
(paper_id, title, authors, link, last_updated, summary,
|
| 133 |
-
journal_ref, primary_category, categories,
|
| 134 |
-
theorem_name, theorem_slogan, theorem_body) = row
|
| 135 |
-
|
| 136 |
-
# Determine type from name
|
| 137 |
-
inferred_type = infer_type(theorem_name or "")
|
| 138 |
-
|
| 139 |
-
# Determine source from url
|
| 140 |
-
link_str = link or ""
|
| 141 |
-
if link_str.startswith("http://arxiv.org") or link_str.startswith("https://arxiv.org"):
|
| 142 |
-
source = "arXiv"
|
| 143 |
-
all_theorems_data.append({
|
| 144 |
-
"paper_id": paper_id,
|
| 145 |
-
"authors": authors,
|
| 146 |
-
"paper_title": title,
|
| 147 |
-
"paper_url": link,
|
| 148 |
-
"year": last_updated.year,
|
| 149 |
-
"primary_category": primary_category,
|
| 150 |
-
"source": source,
|
| 151 |
-
"type": inferred_type,
|
| 152 |
-
"journal_published": bool(journal_ref),
|
| 153 |
-
"citations": None,
|
| 154 |
-
"theorem_name": theorem_name,
|
| 155 |
-
"theorem_slogan": theorem_slogan,
|
| 156 |
-
"theorem_body": theorem_body,
|
| 157 |
-
})
|
| 158 |
-
else:
|
| 159 |
-
source = "Stacks Project"
|
| 160 |
-
all_theorems_data.append({
|
| 161 |
-
"paper_id": paper_id,
|
| 162 |
-
"authors": authors,
|
| 163 |
-
"paper_title": title,
|
| 164 |
-
"paper_url": link,
|
| 165 |
-
"year": None,
|
| 166 |
-
"primary_category": primary_category,
|
| 167 |
-
"source": source,
|
| 168 |
-
"type": inferred_type,
|
| 169 |
-
"journal_published": None,
|
| 170 |
-
"citations": None,
|
| 171 |
-
"theorem_name": theorem_name,
|
| 172 |
-
"theorem_slogan": theorem_slogan,
|
| 173 |
-
"theorem_body": theorem_body,
|
| 174 |
-
})
|
| 175 |
-
|
| 176 |
-
return all_theorems_data
|
| 177 |
-
|
| 178 |
-
except Exception as e:
|
| 179 |
-
st.error(f"Error loading data from RDS: {e}")
|
| 180 |
-
return []
|
| 181 |
-
|
| 182 |
@st.cache_data(ttl=60*60*24) # cache for 24 hours
|
| 183 |
def load_authors():
|
| 184 |
conn = get_rds_connection()
|
|
@@ -211,13 +98,10 @@ def load_tags_per_source():
|
|
| 211 |
rows = cur.fetchall()
|
| 212 |
cur.close()
|
| 213 |
conn.close()
|
| 214 |
-
|
| 215 |
-
from collections import defaultdict
|
| 216 |
tags_per_source = defaultdict(set)
|
| 217 |
for source, cat in rows:
|
| 218 |
tags_per_source[source].add(cat)
|
| 219 |
|
| 220 |
-
# Make them plain lists so Streamlit cache can serialize easily
|
| 221 |
return {src: sorted(cats) for src, cats in tags_per_source.items()}
|
| 222 |
|
| 223 |
@st.cache_data(ttl=60*60*24) # cache for 24 hours
|
|
@@ -257,33 +141,10 @@ def parse_paper_filter(raw: str) -> dict:
|
|
| 257 |
titles.add(normalize_title(token))
|
| 258 |
return {"ids": ids, "titles": titles}
|
| 259 |
|
| 260 |
-
def
|
| 261 |
-
c = int(citations) if citations is not None else 0
|
| 262 |
-
if c == 0:
|
| 263 |
-
return float(similarity)
|
| 264 |
-
return float(similarity) + float(weight) * np.log(c)
|
| 265 |
-
|
| 266 |
-
def on_click_url(query: str, url: str, theorem_name: str, filters: dict):
|
| 267 |
-
nav_to(url)
|
| 268 |
-
safe_filters = make_json_safe(filters)
|
| 269 |
-
filters_json = json.dumps(safe_filters)
|
| 270 |
conn = get_rds_connection()
|
| 271 |
cur = conn.cursor()
|
| 272 |
-
cur.execute(
|
| 273 |
-
"INSERT INTO queries (query, url, theorem_name, filters) VALUES (%s, %s, %s, %s)",
|
| 274 |
-
(query, url, theorem_name, filters_json)
|
| 275 |
-
)
|
| 276 |
-
conn.commit()
|
| 277 |
-
cur.close()
|
| 278 |
-
conn.close()
|
| 279 |
|
| 280 |
-
def nav_to(url):
|
| 281 |
-
open_script = """
|
| 282 |
-
<script type="text/javascript">
|
| 283 |
-
window.open('%s', '_blank').focus();
|
| 284 |
-
</script>
|
| 285 |
-
""" % url
|
| 286 |
-
html(open_script)
|
| 287 |
|
| 288 |
def make_json_safe(obj):
|
| 289 |
if isinstance(obj, dict):
|
|
@@ -294,7 +155,7 @@ def make_json_safe(obj):
|
|
| 294 |
return list(obj)
|
| 295 |
elif isinstance(obj, list):
|
| 296 |
return [make_json_safe(v) for v in obj]
|
| 297 |
-
elif hasattr(obj, "item"):
|
| 298 |
return obj.item()
|
| 299 |
else:
|
| 300 |
return obj
|
|
@@ -380,16 +241,21 @@ def search_and_display(query: str, model, filters: dict):
|
|
| 380 |
|
| 381 |
params.extend([low, high])
|
| 382 |
|
| 383 |
-
|
|
|
|
|
|
|
|
|
|
| 384 |
|
| 385 |
-
|
| 386 |
-
|
| 387 |
-
|
| 388 |
-
|
| 389 |
-
|
| 390 |
-
|
| 391 |
-
|
| 392 |
-
|
|
|
|
|
|
|
| 393 |
SELECT
|
| 394 |
p.paper_id,
|
| 395 |
p.title,
|
|
@@ -412,86 +278,145 @@ def search_and_display(query: str, model, filters: dict):
|
|
| 412 |
JOIN {EMBED_TABLE} e ON e.slogan_id = ls.slogan_id
|
| 413 |
{'WHERE ' + ' AND '.join(where) if where else ''}
|
| 414 |
ORDER BY e.embedding <#> %s::vector ASC
|
| 415 |
-
LIMIT
|
| 416 |
-
|
| 417 |
-
|
| 418 |
-
|
| 419 |
-
|
| 420 |
-
|
| 421 |
-
|
| 422 |
-
|
| 423 |
-
|
| 424 |
-
|
| 425 |
-
|
| 426 |
-
|
| 427 |
-
|
| 428 |
-
|
| 429 |
-
|
| 430 |
-
|
| 431 |
-
|
| 432 |
-
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 433 |
|
| 434 |
-
conn = get_rds_connection()
|
| 435 |
-
cur = conn.cursor()
|
| 436 |
-
cur.execute(sql, exec_params)
|
| 437 |
-
rows = cur.fetchall()
|
| 438 |
cur.close()
|
| 439 |
conn.close()
|
| 440 |
|
| 441 |
-
# Populate result fields
|
| 442 |
-
items = []
|
| 443 |
-
for (paper_id, title, authors, link, last_updated, summary, journal_ref,
|
| 444 |
-
primary_category, categories, citations, theorem_id, theorem_name,
|
| 445 |
-
theorem_body, theorem_slogan, similarity, weighted_score) in rows:
|
| 446 |
-
|
| 447 |
-
# Determine source from url
|
| 448 |
-
link_str = link or ""
|
| 449 |
-
source = "arXiv" if link_str.startswith(
|
| 450 |
-
("http://arxiv.org", "https://arxiv.org")) or "arxiv.org" in link_str else "Stacks Project"
|
| 451 |
-
|
| 452 |
-
inferred_type = infer_type(theorem_name or "")
|
| 453 |
-
|
| 454 |
-
items.append({
|
| 455 |
-
"paper_id": paper_id,
|
| 456 |
-
"authors": authors,
|
| 457 |
-
"paper_title": title,
|
| 458 |
-
"paper_url": link,
|
| 459 |
-
"year": last_updated.year,
|
| 460 |
-
"primary_category": primary_category,
|
| 461 |
-
"source": source,
|
| 462 |
-
"type": inferred_type,
|
| 463 |
-
"journal_published": bool(journal_ref),
|
| 464 |
-
"citations": citations,
|
| 465 |
-
"theorem_name": theorem_name,
|
| 466 |
-
"theorem_slogan": theorem_slogan,
|
| 467 |
-
"theorem_body": theorem_body,
|
| 468 |
-
"similarity": float(similarity),
|
| 469 |
-
"score": weighted_score
|
| 470 |
-
})
|
| 471 |
-
|
| 472 |
-
# Compute weighted citation score if applicable
|
| 473 |
-
for it in items:
|
| 474 |
-
it["score"] = compute_score(it["similarity"], it.get("citations"), citation_weight)
|
| 475 |
-
|
| 476 |
-
# Sort results by weighted score, then cosine similarity, then paper id
|
| 477 |
-
items.sort(key=lambda x: (x["score"], x["similarity"], str(x.get("paper_id"))), reverse=True)
|
| 478 |
-
|
| 479 |
# Display results
|
| 480 |
-
st.subheader(f"Found {len(
|
| 481 |
-
if not
|
| 482 |
st.warning("No results found for the current filters.")
|
| 483 |
return
|
| 484 |
|
| 485 |
-
for i, info in enumerate(
|
| 486 |
expander_title = f"**Result {i + 1} | Similarity: {info['score']:.4f} | {info.get('type', '').title()}**"
|
| 487 |
with st.expander(expander_title, expanded=True):
|
| 488 |
st.markdown(f"**Paper:** *{info.get('paper_title', 'Unknown')}*")
|
| 489 |
st.markdown(f"**Authors:** {', '.join(info.get('authors') or []) or 'N/A'}")
|
| 490 |
st.markdown(f"**Source:** {info.get('source')}")
|
| 491 |
-
|
| 492 |
-
|
| 493 |
-
|
| 494 |
-
|
|
|
|
|
|
|
|
|
|
|
|
|
| 495 |
citations = info.get("citations")
|
| 496 |
cit_str = "Unknown" if citations is None else str(citations)
|
| 497 |
st.markdown(
|
|
@@ -506,15 +431,17 @@ def search_and_display(query: str, model, filters: dict):
|
|
| 506 |
cleaned_content = clean_latex_for_display(info['theorem_body'])
|
| 507 |
st.markdown(f"**{info['theorem_name'] or 'Theorem Body.'}**")
|
| 508 |
st.markdown(cleaned_content)
|
| 509 |
-
|
| 510 |
-
|
| 511 |
-
|
| 512 |
-
|
| 513 |
-
|
| 514 |
-
|
| 515 |
-
|
| 516 |
-
|
| 517 |
-
|
|
|
|
|
|
|
| 518 |
|
| 519 |
# --- Main App Interface ---
|
| 520 |
st.set_page_config(page_title="Theorem Search Demo", layout="wide")
|
|
@@ -529,6 +456,7 @@ tags_per_source = load_tags_per_source()
|
|
| 529 |
if model:
|
| 530 |
st.success(f"Successfully loaded {theorem_count} theorems from arXiv and the Stacks Project. Ready to search!")
|
| 531 |
# --- Sidebar filters ---
|
|
|
|
| 532 |
with st.sidebar:
|
| 533 |
st.header("Search Filters")
|
| 534 |
|
|
@@ -554,7 +482,6 @@ if model:
|
|
| 554 |
selected_authors = st.multiselect("Filter by Author(s):", authors)
|
| 555 |
|
| 556 |
# Tags per selected source(s)
|
| 557 |
-
tags_per_source = defaultdict(set)
|
| 558 |
union_tags = sorted({
|
| 559 |
t
|
| 560 |
for s in selected_sources
|
|
@@ -576,7 +503,8 @@ if model:
|
|
| 576 |
citation_range = st.slider("Filter by Citations:", 0, 1000, (0,1000), step=10)
|
| 577 |
citation_weight = st.slider("Citation Weight:", 0.0, 1.0, 0.0, step=0.01,
|
| 578 |
help="If nonzero, results are ranked by base_score $+$ weight $\\times$ "
|
| 579 |
-
"$\\log($citations$)$."
|
|
|
|
| 580 |
include_unknown_citations = st.checkbox(
|
| 581 |
"Include entries with unknown citation counts",
|
| 582 |
value=True,
|
|
|
|
| 1 |
import streamlit as st
|
| 2 |
+
import streamlit_antd_components as sac
|
| 3 |
import json
|
|
|
|
| 4 |
from sentence_transformers import SentenceTransformer
|
| 5 |
import os
|
| 6 |
import boto3
|
|
|
|
| 8 |
from psycopg2.extensions import connection
|
| 9 |
from pgvector.psycopg2 import register_vector
|
| 10 |
import re
|
|
|
|
|
|
|
| 11 |
from collections import defaultdict
|
| 12 |
from dotenv import load_dotenv
|
| 13 |
from latex_clean import clean_latex_for_display
|
|
|
|
| 15 |
# Config
|
| 16 |
load_dotenv()
|
| 17 |
|
|
|
|
| 18 |
def get_rds_connection() -> connection:
|
| 19 |
region = os.getenv("AWS_REGION")
|
| 20 |
secret_arn = os.getenv("RDS_SECRET_ARN")
|
|
|
|
| 36 |
register_vector(conn)
|
| 37 |
return conn
|
| 38 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 39 |
ALLOWED_TYPES = [
|
| 40 |
"theorem", "lemma", "proposition", "corollary"
|
| 41 |
]
|
|
|
|
| 47 |
|
| 48 |
EMBED_TABLE = "theorem_embedding_qwen"
|
| 49 |
|
|
|
|
| 50 |
# Load the Embedding Model
|
| 51 |
@st.cache_resource
|
| 52 |
def load_model():
|
|
|
|
| 61 |
if not name:
|
| 62 |
return "theorem"
|
| 63 |
lower = name.lower()
|
| 64 |
+
for t in ALLOWED_TYPES:
|
| 65 |
if t in lower:
|
| 66 |
return t
|
| 67 |
return "theorem"
|
| 68 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 69 |
@st.cache_data(ttl=60*60*24) # cache for 24 hours
|
| 70 |
def load_authors():
|
| 71 |
conn = get_rds_connection()
|
|
|
|
| 98 |
rows = cur.fetchall()
|
| 99 |
cur.close()
|
| 100 |
conn.close()
|
|
|
|
|
|
|
| 101 |
tags_per_source = defaultdict(set)
|
| 102 |
for source, cat in rows:
|
| 103 |
tags_per_source[source].add(cat)
|
| 104 |
|
|
|
|
| 105 |
return {src: sorted(cats) for src, cats in tags_per_source.items()}
|
| 106 |
|
| 107 |
@st.cache_data(ttl=60*60*24) # cache for 24 hours
|
|
|
|
| 141 |
titles.add(normalize_title(token))
|
| 142 |
return {"ids": ids, "titles": titles}
|
| 143 |
|
| 144 |
+
def save_feedback(feedback, query, url, theorem_name, filters):
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 145 |
conn = get_rds_connection()
|
| 146 |
cur = conn.cursor()
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 147 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 148 |
|
| 149 |
def make_json_safe(obj):
|
| 150 |
if isinstance(obj, dict):
|
|
|
|
| 155 |
return list(obj)
|
| 156 |
elif isinstance(obj, list):
|
| 157 |
return [make_json_safe(v) for v in obj]
|
| 158 |
+
elif hasattr(obj, "item"):
|
| 159 |
return obj.item()
|
| 160 |
else:
|
| 161 |
return obj
|
|
|
|
| 241 |
|
| 242 |
params.extend([low, high])
|
| 243 |
|
| 244 |
+
conn = get_rds_connection()
|
| 245 |
+
cur = conn.cursor()
|
| 246 |
+
|
| 247 |
+
results = []
|
| 248 |
|
| 249 |
+
# Fetch results from RDS
|
| 250 |
+
|
| 251 |
+
if citation_weight == 0.0:
|
| 252 |
+
sql = f"""
|
| 253 |
+
WITH latest_slogan AS (
|
| 254 |
+
SELECT DISTINCT ON (ts.theorem_id)
|
| 255 |
+
ts.theorem_id, ts.slogan_id, ts.slogan
|
| 256 |
+
FROM theorem_slogan ts
|
| 257 |
+
ORDER BY ts.theorem_id, ts.slogan_id DESC
|
| 258 |
+
)
|
| 259 |
SELECT
|
| 260 |
p.paper_id,
|
| 261 |
p.title,
|
|
|
|
| 278 |
JOIN {EMBED_TABLE} e ON e.slogan_id = ls.slogan_id
|
| 279 |
{'WHERE ' + ' AND '.join(where) if where else ''}
|
| 280 |
ORDER BY e.embedding <#> %s::vector ASC
|
| 281 |
+
LIMIT %s;
|
| 282 |
+
"""
|
| 283 |
+
exec_params = [query_vec, *params, query_vec, int(filters['top_k'])]
|
| 284 |
+
|
| 285 |
+
cur.execute(sql, exec_params)
|
| 286 |
+
rows = cur.fetchall()
|
| 287 |
+
|
| 288 |
+
for (paper_id, title, authors, link, last_updated, summary, journal_ref,
|
| 289 |
+
primary_category, categories, citations, theorem_id, theorem_name,
|
| 290 |
+
theorem_body, theorem_slogan, similarity) in rows:
|
| 291 |
+
link_str = link or ""
|
| 292 |
+
source = "arXiv" if "arxiv.org" in link_str else "Stacks Project"
|
| 293 |
+
inferred_type = infer_type(theorem_name or "")
|
| 294 |
+
year = last_updated.year if last_updated else None
|
| 295 |
+
|
| 296 |
+
results.append({
|
| 297 |
+
"paper_id": paper_id,
|
| 298 |
+
"authors": authors,
|
| 299 |
+
"paper_title": title,
|
| 300 |
+
"paper_url": link,
|
| 301 |
+
"year": year,
|
| 302 |
+
"primary_category": primary_category,
|
| 303 |
+
"source": source,
|
| 304 |
+
"type": inferred_type,
|
| 305 |
+
"journal_published": bool(journal_ref),
|
| 306 |
+
"citations": citations,
|
| 307 |
+
"theorem_id": theorem_id,
|
| 308 |
+
"theorem_name": theorem_name,
|
| 309 |
+
"theorem_slogan": theorem_slogan,
|
| 310 |
+
"theorem_body": theorem_body,
|
| 311 |
+
"similarity": float(similarity),
|
| 312 |
+
"score": float(similarity),
|
| 313 |
+
})
|
| 314 |
+
|
| 315 |
+
else:
|
| 316 |
+
pool_size = max(50, int(filters['top_k']) * 10)
|
| 317 |
+
|
| 318 |
+
sql = f"""
|
| 319 |
+
WITH latest_slogan AS (
|
| 320 |
+
SELECT DISTINCT ON (ts.theorem_id)
|
| 321 |
+
ts.theorem_id, ts.slogan_id, ts.slogan
|
| 322 |
+
FROM theorem_slogan ts
|
| 323 |
+
ORDER BY ts.theorem_id, ts.slogan_id DESC
|
| 324 |
+
),
|
| 325 |
+
candidates AS (
|
| 326 |
+
SELECT
|
| 327 |
+
p.paper_id,
|
| 328 |
+
p.title,
|
| 329 |
+
p.authors,
|
| 330 |
+
p.link,
|
| 331 |
+
p.last_updated,
|
| 332 |
+
p.summary,
|
| 333 |
+
p.journal_ref,
|
| 334 |
+
p.primary_category,
|
| 335 |
+
p.categories,
|
| 336 |
+
p.citations,
|
| 337 |
+
t.theorem_id,
|
| 338 |
+
t.name AS theorem_name,
|
| 339 |
+
t.body AS theorem_body,
|
| 340 |
+
ls.slogan AS theorem_slogan,
|
| 341 |
+
(1.0 - (e.embedding <#> %s::vector)) AS similarity
|
| 342 |
+
FROM paper p
|
| 343 |
+
JOIN theorem t ON t.paper_id = p.paper_id
|
| 344 |
+
JOIN latest_slogan ls ON ls.theorem_id = t.theorem_id
|
| 345 |
+
JOIN {EMBED_TABLE} e ON e.slogan_id = ls.slogan_id
|
| 346 |
+
{'WHERE ' + ' AND '.join(where) if where else ''}
|
| 347 |
+
ORDER BY e.embedding <#> %s::vector ASC
|
| 348 |
+
LIMIT {pool_size}
|
| 349 |
+
)
|
| 350 |
+
SELECT
|
| 351 |
+
*,
|
| 352 |
+
(
|
| 353 |
+
similarity +
|
| 354 |
+
%s * CASE
|
| 355 |
+
WHEN citations IS NOT NULL AND citations > 0
|
| 356 |
+
THEN ln(citations::float)
|
| 357 |
+
ELSE 0
|
| 358 |
+
END
|
| 359 |
+
) AS weighted_score
|
| 360 |
+
FROM candidates
|
| 361 |
+
ORDER BY weighted_score DESC, similarity DESC
|
| 362 |
+
LIMIT %s;
|
| 363 |
+
"""
|
| 364 |
+
|
| 365 |
+
exec_params = [query_vec, *params, query_vec, citation_weight, int(filters['top_k'])]
|
| 366 |
+
|
| 367 |
+
cur.execute(sql, exec_params)
|
| 368 |
+
rows = cur.fetchall()
|
| 369 |
+
|
| 370 |
+
for (paper_id, title, authors, link, last_updated, summary, journal_ref,
|
| 371 |
+
primary_category, categories, citations, theorem_id, theorem_name,
|
| 372 |
+
theorem_body, theorem_slogan, similarity, weighted_score) in rows:
|
| 373 |
+
link_str = link or ""
|
| 374 |
+
source = "arXiv" if "arxiv.org" in link_str else "Stacks Project"
|
| 375 |
+
inferred_type = infer_type(theorem_name or "")
|
| 376 |
+
year = last_updated.year if last_updated else None
|
| 377 |
+
|
| 378 |
+
results.append({
|
| 379 |
+
"paper_id": paper_id,
|
| 380 |
+
"authors": authors,
|
| 381 |
+
"paper_title": title,
|
| 382 |
+
"paper_url": link,
|
| 383 |
+
"year": year,
|
| 384 |
+
"primary_category": primary_category,
|
| 385 |
+
"source": source,
|
| 386 |
+
"type": inferred_type,
|
| 387 |
+
"journal_published": bool(journal_ref),
|
| 388 |
+
"citations": citations,
|
| 389 |
+
"theorem_id": theorem_id,
|
| 390 |
+
"theorem_name": theorem_name,
|
| 391 |
+
"theorem_slogan": theorem_slogan,
|
| 392 |
+
"theorem_body": theorem_body,
|
| 393 |
+
"similarity": float(similarity),
|
| 394 |
+
"score": float(weighted_score),
|
| 395 |
+
})
|
| 396 |
|
|
|
|
|
|
|
|
|
|
|
|
|
| 397 |
cur.close()
|
| 398 |
conn.close()
|
| 399 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 400 |
# Display results
|
| 401 |
+
st.subheader(f"Found {len(results)} Matching Results")
|
| 402 |
+
if not results:
|
| 403 |
st.warning("No results found for the current filters.")
|
| 404 |
return
|
| 405 |
|
| 406 |
+
for i, info in enumerate(results):
|
| 407 |
expander_title = f"**Result {i + 1} | Similarity: {info['score']:.4f} | {info.get('type', '').title()}**"
|
| 408 |
with st.expander(expander_title, expanded=True):
|
| 409 |
st.markdown(f"**Paper:** *{info.get('paper_title', 'Unknown')}*")
|
| 410 |
st.markdown(f"**Authors:** {', '.join(info.get('authors') or []) or 'N/A'}")
|
| 411 |
st.markdown(f"**Source:** {info.get('source')}")
|
| 412 |
+
sac.buttons(
|
| 413 |
+
items=
|
| 414 |
+
[sac.ButtonsItem(label=info.get("paper_url"), icon="link-45deg", href=info.get("paper_url"))],
|
| 415 |
+
variant="outline",
|
| 416 |
+
color="violet",
|
| 417 |
+
index=-1,
|
| 418 |
+
key=f"link_{i}"
|
| 419 |
+
)
|
| 420 |
citations = info.get("citations")
|
| 421 |
cit_str = "Unknown" if citations is None else str(citations)
|
| 422 |
st.markdown(
|
|
|
|
| 431 |
cleaned_content = clean_latex_for_display(info['theorem_body'])
|
| 432 |
st.markdown(f"**{info['theorem_name'] or 'Theorem Body.'}**")
|
| 433 |
st.markdown(cleaned_content)
|
| 434 |
+
sac.buttons(
|
| 435 |
+
items=
|
| 436 |
+
[
|
| 437 |
+
sac.ButtonsItem(icon="hand-thumbs-up"),
|
| 438 |
+
sac.ButtonsItem(icon="hand-thumbs-down")
|
| 439 |
+
],
|
| 440 |
+
variant="outline",
|
| 441 |
+
color="violet",
|
| 442 |
+
index=-1,
|
| 443 |
+
key=f"feedback_{i}")
|
| 444 |
+
|
| 445 |
|
| 446 |
# --- Main App Interface ---
|
| 447 |
st.set_page_config(page_title="Theorem Search Demo", layout="wide")
|
|
|
|
| 456 |
if model:
|
| 457 |
st.success(f"Successfully loaded {theorem_count} theorems from arXiv and the Stacks Project. Ready to search!")
|
| 458 |
# --- Sidebar filters ---
|
| 459 |
+
st.logo(image="images/math-ai-logo.jpg", size="large", link="https://sites.math.washington.edu/ai/")
|
| 460 |
with st.sidebar:
|
| 461 |
st.header("Search Filters")
|
| 462 |
|
|
|
|
| 482 |
selected_authors = st.multiselect("Filter by Author(s):", authors)
|
| 483 |
|
| 484 |
# Tags per selected source(s)
|
|
|
|
| 485 |
union_tags = sorted({
|
| 486 |
t
|
| 487 |
for s in selected_sources
|
|
|
|
| 503 |
citation_range = st.slider("Filter by Citations:", 0, 1000, (0,1000), step=10)
|
| 504 |
citation_weight = st.slider("Citation Weight:", 0.0, 1.0, 0.0, step=0.01,
|
| 505 |
help="If nonzero, results are ranked by base_score $+$ weight $\\times$ "
|
| 506 |
+
"$\\log($citations$)$. This will increase search time."
|
| 507 |
+
)
|
| 508 |
include_unknown_citations = st.checkbox(
|
| 509 |
"Include entries with unknown citation counts",
|
| 510 |
value=True,
|