Spaces:
Sleeping
Sleeping
Commit
·
6d67071
1
Parent(s):
df59efe
Add LogicBench integration tab (UI and placeholder logic)
Browse files
app.py
CHANGED
@@ -2,6 +2,7 @@
|
|
2 |
Gradio application for SFOSR (Semantic Formal Ontology Structure Representation) System.
|
3 |
|
4 |
Provides an interface to analyze, verify, and construct proofs using the SFOSR framework.
|
|
|
5 |
"""
|
6 |
|
7 |
import gradio as gr
|
@@ -40,9 +41,10 @@ else:
|
|
40 |
|
41 |
# --- Helper Functions for Gradio ---
|
42 |
|
43 |
-
def handle_system_unavailable():
|
44 |
-
"""Returns
|
45 |
-
|
|
|
46 |
|
47 |
def process_input_json(json_string):
|
48 |
"""Safely parse input JSON string."""
|
@@ -64,7 +66,7 @@ def process_input_json(json_string):
|
|
64 |
def run_analysis_verification(input_json_str):
|
65 |
"""Gradio function to run analysis and verification."""
|
66 |
if sfosr_instance is None:
|
67 |
-
return handle_system_unavailable()
|
68 |
|
69 |
input_data, error = process_input_json(input_json_str)
|
70 |
if error:
|
@@ -91,13 +93,14 @@ def run_analysis_verification(input_json_str):
|
|
91 |
return analysis_summary, verification_summary, vector_details, graph_output
|
92 |
|
93 |
except Exception as e:
|
94 |
-
|
95 |
-
|
|
|
96 |
|
97 |
def run_proof_construction(input_json_str, source_concept, target_concept):
|
98 |
"""Gradio function to run proof construction."""
|
99 |
if sfosr_instance is None:
|
100 |
-
return handle_system_unavailable()
|
101 |
|
102 |
input_data, error = process_input_json(input_json_str)
|
103 |
if error:
|
@@ -120,7 +123,7 @@ def run_proof_construction(input_json_str, source_concept, target_concept):
|
|
120 |
|
121 |
if not proof_result:
|
122 |
# This might happen if the process function structure changes or proof wasn't run
|
123 |
-
return "Proof was not attempted or failed silently.", ""
|
124 |
|
125 |
proof_status = f"**Proof Status:** {proof_result.get('status', 'N/A')}\n" \
|
126 |
f"**Is Valid:** {proof_result.get('is_valid', 'N/A')}"
|
@@ -132,9 +135,75 @@ def run_proof_construction(input_json_str, source_concept, target_concept):
|
|
132 |
return proof_status, proof_details
|
133 |
|
134 |
except Exception as e:
|
135 |
-
|
|
|
136 |
return f"An error occurred: {e}", ""
|
137 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
138 |
|
139 |
# --- Example Input Formats ---
|
140 |
example_verify_json = '''{
|
@@ -180,6 +249,10 @@ example_proof_json = '''{
|
|
180 |
]
|
181 |
}'''
|
182 |
|
|
|
|
|
|
|
|
|
183 |
# --- Gradio Interface Definition ---
|
184 |
|
185 |
with gr.Blocks(theme=gr.themes.Soft()) as demo:
|
@@ -250,7 +323,7 @@ with gr.Blocks(theme=gr.themes.Soft()) as demo:
|
|
250 |
gr.Markdown("### Детали Проверки Векторов")
|
251 |
vector_details_output = gr.JSON(label="Детали по Векторам")
|
252 |
gr.Markdown("### Граф Концептов")
|
253 |
-
graph_placeholder_output = gr.Textbox(label="Информация о Графе")
|
254 |
|
255 |
gr.Examples(
|
256 |
examples=[
|
@@ -310,7 +383,60 @@ with gr.Blocks(theme=gr.themes.Soft()) as demo:
|
|
310 |
inputs=[input_json_p, source_concept_input, target_concept_input],
|
311 |
label="Пример построения доказательства"
|
312 |
)
|
313 |
-
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
314 |
with gr.TabItem("Справка"):
|
315 |
gr.Markdown(
|
316 |
"""
|
@@ -364,17 +490,27 @@ with gr.Blocks(theme=gr.themes.Soft()) as demo:
|
|
364 |
|
365 |
# --- Event Handlers ---
|
366 |
if sfosr_instance: # Only wire up buttons if the system initialized
|
|
|
367 |
av_button.click(
|
368 |
fn=run_analysis_verification,
|
369 |
inputs=[input_json_av],
|
370 |
outputs=[analysis_output, verification_output, vector_details_output, graph_placeholder_output]
|
371 |
)
|
372 |
-
|
|
|
373 |
p_button.click(
|
374 |
fn=run_proof_construction,
|
375 |
inputs=[input_json_p, source_concept_input, target_concept_input],
|
376 |
outputs=[proof_status_output, proof_details_output]
|
377 |
)
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
378 |
else:
|
379 |
# Display a persistent error if the system couldn't load
|
380 |
gr.Markdown(
|
|
|
2 |
Gradio application for SFOSR (Semantic Formal Ontology Structure Representation) System.
|
3 |
|
4 |
Provides an interface to analyze, verify, and construct proofs using the SFOSR framework.
|
5 |
+
Includes a tab for integrating with LogicBench tasks (requires LLM for text-to-SFOSR conversion).
|
6 |
"""
|
7 |
|
8 |
import gradio as gr
|
|
|
41 |
|
42 |
# --- Helper Functions for Gradio ---
|
43 |
|
44 |
+
def handle_system_unavailable(num_outputs=4):
|
45 |
+
"""Returns error messages if the SFOSR system isn't ready."""
|
46 |
+
error_msg = "SFOSR System is not available. Please check server logs."
|
47 |
+
return [error_msg] + ["" for _ in range(num_outputs - 1)]
|
48 |
|
49 |
def process_input_json(json_string):
|
50 |
"""Safely parse input JSON string."""
|
|
|
66 |
def run_analysis_verification(input_json_str):
|
67 |
"""Gradio function to run analysis and verification."""
|
68 |
if sfosr_instance is None:
|
69 |
+
return handle_system_unavailable(num_outputs=4)
|
70 |
|
71 |
input_data, error = process_input_json(input_json_str)
|
72 |
if error:
|
|
|
93 |
return analysis_summary, verification_summary, vector_details, graph_output
|
94 |
|
95 |
except Exception as e:
|
96 |
+
error_trace = traceback.format_exc()
|
97 |
+
print(f"Error during SFOSR processing: {e}\n{error_trace}") # Log for debugging
|
98 |
+
return f"An error occurred: {e}", "", vector_details, graph_output # Return partial results if possible
|
99 |
|
100 |
def run_proof_construction(input_json_str, source_concept, target_concept):
|
101 |
"""Gradio function to run proof construction."""
|
102 |
if sfosr_instance is None:
|
103 |
+
return handle_system_unavailable(num_outputs=2)
|
104 |
|
105 |
input_data, error = process_input_json(input_json_str)
|
106 |
if error:
|
|
|
123 |
|
124 |
if not proof_result:
|
125 |
# This might happen if the process function structure changes or proof wasn't run
|
126 |
+
return "Proof was not attempted or failed silently (check input vectors and concepts).", ""
|
127 |
|
128 |
proof_status = f"**Proof Status:** {proof_result.get('status', 'N/A')}\n" \
|
129 |
f"**Is Valid:** {proof_result.get('is_valid', 'N/A')}"
|
|
|
135 |
return proof_status, proof_details
|
136 |
|
137 |
except Exception as e:
|
138 |
+
error_trace = traceback.format_exc()
|
139 |
+
print(f"Error during SFOSR proof: {e}\n{error_trace}") # Log for debugging
|
140 |
return f"An error occurred: {e}", ""
|
141 |
|
142 |
+
# --- Placeholder for LogicBench Integration ---
|
143 |
+
def run_logicbench_task(logicbench_context, logicbench_question):
|
144 |
+
"""Placeholder function for LogicBench task processing."""
|
145 |
+
print(f"Received LogicBench Context: {logicbench_context[:100]}...")
|
146 |
+
print(f"Received LogicBench Question: {logicbench_question}")
|
147 |
+
|
148 |
+
# --- Stage 1: Text-to-SFOSR Conversion (using LLM - TO BE IMPLEMENTED) ---
|
149 |
+
generated_sfosr_json = {
|
150 |
+
"text": logicbench_context,
|
151 |
+
"vectors": [
|
152 |
+
{"id": "placeholder", "source": "PlaceholderSource", "target": "PlaceholderTarget",
|
153 |
+
"type": "PlaceholderType", "axis": "placeholder", "justification": "LLM Step Not Implemented"}
|
154 |
+
]
|
155 |
+
}
|
156 |
+
generated_sfosr_str = json.dumps(generated_sfosr_json, indent=2, ensure_ascii=False)
|
157 |
+
|
158 |
+
# --- Stage 2: SFOSR Processing (using the generated JSON) ---
|
159 |
+
if sfosr_instance is None:
|
160 |
+
final_answer = "Error: SFOSR System not available."
|
161 |
+
sfosr_proof_status = ""
|
162 |
+
sfosr_proof_details = ""
|
163 |
+
else:
|
164 |
+
try:
|
165 |
+
# Determine source/target for proof based on the question (requires logic)
|
166 |
+
# For now, let's use placeholder source/target from the generated JSON
|
167 |
+
# This part needs significant refinement based on how questions are mapped
|
168 |
+
source_concept_lb = generated_sfosr_json["vectors"][0]["source"]
|
169 |
+
target_concept_lb = generated_sfosr_json["vectors"][0]["target"]
|
170 |
+
|
171 |
+
logicbench_input_data = generated_sfosr_json
|
172 |
+
logicbench_input_data["proof_query"] = {
|
173 |
+
"source": source_concept_lb,
|
174 |
+
"target": target_concept_lb
|
175 |
+
}
|
176 |
+
|
177 |
+
# Call the main process method
|
178 |
+
sfosr_result = sfosr_instance.process(logicbench_input_data)
|
179 |
+
sfosr_proof_result = sfosr_result.get("proof")
|
180 |
+
|
181 |
+
# --- Stage 3: Interpret SFOSR Result as LogicBench Answer (TO BE IMPLEMENTED) ---
|
182 |
+
if sfosr_proof_result and sfosr_proof_result.get("is_valid"):
|
183 |
+
final_answer = "Answer: Yes (Placeholder - based on successful SFOSR proof)"
|
184 |
+
else:
|
185 |
+
final_answer = "Answer: No/Unknown (Placeholder - SFOSR proof failed or invalid)"
|
186 |
+
|
187 |
+
# Format proof output for display
|
188 |
+
if sfosr_proof_result:
|
189 |
+
sfosr_proof_status = f"**Proof Status:** {sfosr_proof_result.get('status', 'N/A')}\n" \
|
190 |
+
f"**Is Valid:** {sfosr_proof_result.get('is_valid', 'N/A')}"
|
191 |
+
if sfosr_proof_result.get('reason'):
|
192 |
+
sfosr_proof_status += f"\n**Reason:** {sfosr_proof_result.get('reason')}"
|
193 |
+
sfosr_proof_details = sfosr_proof_result
|
194 |
+
else:
|
195 |
+
sfosr_proof_status = "SFOSR Proof was not generated or failed."
|
196 |
+
sfosr_proof_details = {}
|
197 |
+
|
198 |
+
except Exception as e:
|
199 |
+
error_trace = traceback.format_exc()
|
200 |
+
print(f"Error during LogicBench task processing: {e}\n{error_trace}")
|
201 |
+
final_answer = f"Error processing task: {e}"
|
202 |
+
sfosr_proof_status = "Error during processing"
|
203 |
+
sfosr_proof_details = {}
|
204 |
+
|
205 |
+
return final_answer, generated_sfosr_str, sfosr_proof_status, sfosr_proof_details
|
206 |
+
|
207 |
|
208 |
# --- Example Input Formats ---
|
209 |
example_verify_json = '''{
|
|
|
249 |
]
|
250 |
}'''
|
251 |
|
252 |
+
# Example for LogicBench (replace with actual examples)
|
253 |
+
example_logicbench_context = "If it rains, the ground gets wet. The ground is not wet."
|
254 |
+
example_logicbench_question = "Did it rain?"
|
255 |
+
|
256 |
# --- Gradio Interface Definition ---
|
257 |
|
258 |
with gr.Blocks(theme=gr.themes.Soft()) as demo:
|
|
|
323 |
gr.Markdown("### Детали Проверки Векторов")
|
324 |
vector_details_output = gr.JSON(label="Детали по Векторам")
|
325 |
gr.Markdown("### Граф Концептов")
|
326 |
+
graph_placeholder_output = gr.Textbox(label="Информация о Графе") # Placeholder
|
327 |
|
328 |
gr.Examples(
|
329 |
examples=[
|
|
|
383 |
inputs=[input_json_p, source_concept_input, target_concept_input],
|
384 |
label="Пример построения доказательства"
|
385 |
)
|
386 |
+
|
387 |
+
with gr.TabItem("Интеграция с LogicBench"):
|
388 |
+
gr.Markdown(
|
389 |
+
"""
|
390 |
+
### Решение Задач LogicBench (Экспериментально)
|
391 |
+
|
392 |
+
Эта вкладка демонстрирует гибридный подход:
|
393 |
+
1. **LLM** преобразует текстовую задачу из LogicBench в структурированные SFOSR векторы (JSON).
|
394 |
+
2. **SFOSR** система анализирует и пытается доказать ответ на вопрос задачи, используя сгенерированные векторы.
|
395 |
+
|
396 |
+
**Внимание:** Шаг 1 (LLM преобразование) еще не реализован. Сейчас используется placeholder.
|
397 |
+
|
398 |
+
#### Как пользоваться (когда будет реализовано):
|
399 |
+
1. Вставьте **Контекст/Посылки** из задачи LogicBench.
|
400 |
+
2. Вставьте **Вопрос** из задачи LogicBench.
|
401 |
+
3. Нажмите кнопку "Решить Задачу LogicBench".
|
402 |
+
4. Посмотрите **Финальный Ответ** и детали работы SFOSR.
|
403 |
+
"""
|
404 |
+
)
|
405 |
+
with gr.Row():
|
406 |
+
with gr.Column(scale=1):
|
407 |
+
gr.Markdown("### Входные данные из LogicBench")
|
408 |
+
lb_context_input = gr.Textbox(
|
409 |
+
lines=10,
|
410 |
+
label="Контекст / Посылки",
|
411 |
+
info="Вставьте текст контекста или посылок из задачи LogicBench",
|
412 |
+
placeholder="Пример: Если идет дождь, трава мокрая. Трава сухая."
|
413 |
+
)
|
414 |
+
lb_question_input = gr.Textbox(
|
415 |
+
lines=2,
|
416 |
+
label="Вопрос",
|
417 |
+
info="Вставьте вопрос из задачи LogicBench",
|
418 |
+
placeholder="Пример: Идет ли дождь?"
|
419 |
+
)
|
420 |
+
lb_button = gr.Button("Решить Задачу LogicBench", variant="primary")
|
421 |
+
|
422 |
+
with gr.Column(scale=1):
|
423 |
+
gr.Markdown("### Результат Решения")
|
424 |
+
lb_final_answer_output = gr.Markdown(label="Финальный Ответ")
|
425 |
+
with gr.Accordion("Детали Обработки SFOSR", open=False):
|
426 |
+
gr.Markdown("#### Сгенерированный SFOSR JSON (LLM Шаг - Placeholder)")
|
427 |
+
lb_sfosr_json_output = gr.Code(language="json", label="SFOSR JSON")
|
428 |
+
gr.Markdown("#### Результат Доказательства SFOSR")
|
429 |
+
lb_proof_status_output = gr.Markdown(label="Статус Доказательства SFOSR")
|
430 |
+
lb_proof_details_output = gr.JSON(label="Структура Доказательства SFOSR")
|
431 |
+
|
432 |
+
gr.Examples(
|
433 |
+
examples=[
|
434 |
+
[example_logicbench_context, example_logicbench_question]
|
435 |
+
],
|
436 |
+
inputs=[lb_context_input, lb_question_input],
|
437 |
+
label="Пример Задачи LogicBench"
|
438 |
+
)
|
439 |
+
|
440 |
with gr.TabItem("Справка"):
|
441 |
gr.Markdown(
|
442 |
"""
|
|
|
490 |
|
491 |
# --- Event Handlers ---
|
492 |
if sfosr_instance: # Only wire up buttons if the system initialized
|
493 |
+
# Analyze & Verify Tab
|
494 |
av_button.click(
|
495 |
fn=run_analysis_verification,
|
496 |
inputs=[input_json_av],
|
497 |
outputs=[analysis_output, verification_output, vector_details_output, graph_placeholder_output]
|
498 |
)
|
499 |
+
|
500 |
+
# Construct Proof Tab
|
501 |
p_button.click(
|
502 |
fn=run_proof_construction,
|
503 |
inputs=[input_json_p, source_concept_input, target_concept_input],
|
504 |
outputs=[proof_status_output, proof_details_output]
|
505 |
)
|
506 |
+
|
507 |
+
# LogicBench Integration Tab
|
508 |
+
lb_button.click(
|
509 |
+
fn=run_logicbench_task,
|
510 |
+
inputs=[lb_context_input, lb_question_input],
|
511 |
+
outputs=[lb_final_answer_output, lb_sfosr_json_output, lb_proof_status_output, lb_proof_details_output]
|
512 |
+
)
|
513 |
+
|
514 |
else:
|
515 |
# Display a persistent error if the system couldn't load
|
516 |
gr.Markdown(
|