Spaces:
Sleeping
Sleeping
""" | |
Gradio application for SFOSR (Semantic Formal Ontology Structure Representation) System. | |
Provides an interface to analyze, verify, and construct proofs using the SFOSR framework. | |
Users can input SFOSR JSON directly or use the proof tab with JSON generated externally (e.g., from LogicBench tasks via LLM). | |
""" | |
import gradio as gr | |
import json | |
import os | |
import sys | |
import traceback | |
# --- Basic diagnostics --- | |
print("==== Starting SFOSR Gradio App ====") | |
print(f"Working directory: {os.getcwd()}") | |
print(f"Python version: {sys.version}") | |
print(f"Files in directory: {os.listdir('.')}") | |
print(f"sfosr_core directory exists: {os.path.exists('sfosr_core')}") | |
if os.path.exists('sfosr_core'): | |
print(f"Files in sfosr_core: {os.listdir('sfosr_core')}") | |
from sfosr_core.sfosr_system import SFOSRSystem # Assuming sfosr_system.py is in sfosr_core | |
# --- Configuration --- | |
DB_PATH = "sfosr.db" # Assumes the database is in the root directory | |
# Check if DB exists, otherwise handle appropriately (e.g., log an error) | |
if not os.path.exists(DB_PATH): | |
print(f"Error: Database file not found at {DB_PATH}. Current working directory: {os.getcwd()}, Files in directory: {os.listdir()}") | |
# In a real scenario, you might want to exit or provide a way to upload/create it. | |
sfosr_instance = None # Indicate that the system is not ready | |
else: | |
# --- Initialize SFOSR System --- | |
try: | |
sfosr_instance = SFOSRSystem(db_path=DB_PATH) | |
print("SFOSR System initialized successfully.") | |
except Exception as e: | |
print(f"Error initializing SFOSR System: {e}\nTraceback: {traceback.format_exc()}") | |
sfosr_instance = None # Indicate that the system failed to initialize | |
# --- Helper Functions for Gradio --- | |
def handle_system_unavailable(num_outputs=4): | |
"""Returns error messages if the SFOSR system isn't ready.""" | |
error_msg = "SFOSR System is not available. Please check server logs." | |
return [error_msg] + ["" for _ in range(num_outputs - 1)] | |
def process_input_json(json_string): | |
"""Safely parse input JSON string.""" | |
if not json_string: | |
return None, "Input JSON cannot be empty." | |
try: | |
data = json.loads(json_string) | |
if not isinstance(data, dict): | |
return None, "Input must be a valid JSON object (dictionary)." | |
if "vectors" not in data or not isinstance(data["vectors"], list): | |
return None, "Input JSON must contain a 'vectors' key with a list of vectors." | |
# Add more validation as needed (e.g., text key) | |
return data, None | |
except json.JSONDecodeError as e: | |
return None, f"Invalid JSON format: {e}" | |
except Exception as e: | |
return None, f"Error processing input: {e}" | |
def run_analysis_verification(input_json_str): | |
"""Gradio function to run analysis and verification.""" | |
if sfosr_instance is None: | |
return handle_system_unavailable(num_outputs=4) | |
input_data, error = process_input_json(input_json_str) | |
if error: | |
return f"Input Error: {error}", "", "", "" | |
try: | |
# Use the main process method which handles both analysis and verification | |
result = sfosr_instance.process(input_data) | |
# Format the output | |
analysis_summary = f"**Analysis Status:** {result.get('analysis', {}).get('status', 'N/A')}\n" \ | |
f"**Compilable:** {result.get('analysis', {}).get('is_compilable', 'N/A')}\n" \ | |
f"**Graph Metrics:** {result.get('analysis', {}).get('graph_metrics', {})}" | |
verification_summary = f"**Total Vectors Processed:** {result.get('verification', {}).get('total_vectors', 0)}\n" \ | |
f"**Valid Vectors:** {result.get('verification', {}).get('valid_count', 0)}\n" \ | |
f"**Compliance Rate:** {result.get('verification', {}).get('compliance_rate', 0.0):.2f}" | |
vector_details = result.get('verification', {}).get('vectors_data', {}) | |
# Optional: Add graph visualization logic here later | |
graph_output = "Graph visualization placeholder" | |
return analysis_summary, verification_summary, vector_details, graph_output | |
except Exception as e: | |
error_trace = traceback.format_exc() | |
print(f"Error during SFOSR processing: {e}\n{error_trace}") # Log for debugging | |
return f"An error occurred: {e}", "", vector_details, graph_output # Return partial results if possible | |
def run_proof_construction(input_json_str, source_concept, target_concept): | |
"""Gradio function to run proof construction.""" | |
if sfosr_instance is None: | |
return handle_system_unavailable(num_outputs=2) | |
input_data, error = process_input_json(input_json_str) | |
if error: | |
return f"Input Error: {error}", "" | |
if not source_concept or not target_concept: | |
return "Source and Target concepts cannot be empty.", "" | |
# Add the proof query to the input data | |
# If input_data doesn't exist yet (e.g., empty string), create it. | |
if input_data is None: | |
input_data = {} | |
input_data["proof_query"] = { | |
"source": source_concept, | |
"target": target_concept | |
} | |
try: | |
# Use the main process method - it includes proof if query exists | |
result = sfosr_instance.process(input_data) | |
proof_result = result.get("proof") | |
if not proof_result: | |
# This might happen if the process function structure changes or proof wasn't run | |
return "Proof was not attempted or failed silently (check input vectors and concepts).", "" | |
proof_status = f"**Proof Status:** {proof_result.get('status', 'N/A')}\n" \ | |
f"**Is Valid:** {proof_result.get('is_valid', 'N/A')}" | |
if proof_result.get('reason'): | |
proof_status += f"\n**Reason:** {proof_result.get('reason')}" | |
proof_details = proof_result # Return the whole proof structure for now | |
return proof_status, proof_details | |
except Exception as e: | |
error_trace = traceback.format_exc() | |
print(f"Error during SFOSR proof: {e}\n{error_trace}") # Log for debugging | |
return f"An error occurred: {e}", "" | |
# --- Example Input Formats --- | |
example_verify_json = '''{ | |
"text": "Загрязнение воздуха вызывает респираторные заболевания. Загрязнение происходит из-за выбросов заводов.", | |
"vectors": [ | |
{ | |
"id": "V1", | |
"source": "ЗагрязнениеВоздуха", | |
"target": "РеспираторныеЗаболевания", | |
"type": "Causality", | |
"axis": "relationship", | |
"justification": "Многочисленные эпидемиологические исследования подтверждают эту связь." | |
}, | |
{ | |
"id": "V2", | |
"source": "ВыбросыЗаводов", | |
"target": "ЗагрязнениеВоздуха", | |
"type": "Causality", | |
"axis": "relationship", | |
"justification": "Промышленные выбросы - один из основных источников загрязняющих веществ." | |
} | |
] | |
}''' | |
# Example JSON potentially generated from LogicBench task: "If it rains, the ground gets wet. The ground is not wet. Question: Did it rain?" | |
# We might want to prove: Rain -> False or check consistency | |
example_logicbench_proof_json = '''{ | |
"vectors": [ | |
{ | |
"id": "LB1", | |
"source": "Rain", | |
"target": "GroundWet", | |
"type": "Implication", | |
"axis": "logic", | |
"justification": "If it rains, the ground gets wet." | |
}, | |
{ | |
"id": "LB2", | |
"source": "GroundWet", | |
"target": "False", | |
"type": "IsA", | |
"axis": "logic", | |
"justification": "The ground is not wet." | |
} | |
] | |
}''' | |
example_logicbench_source = "Rain" | |
example_logicbench_target = "False" # Target to prove based on the question "Did it rain?" | |
# --- Gradio Interface Definition --- | |
with gr.Blocks(theme=gr.themes.Soft()) as demo: | |
gr.Markdown( | |
""" | |
# SFOSR: Система Формальной Оценки Смысла и Верификации | |
## Что это такое? | |
SFOSR (Semantic Formal Ontology Structure Representation) - это система для анализа, верификации и формализации смысловых структур. | |
Она позволяет представить смысловые связи между концептами в виде векторов, проверить их структурную и логическую валидность, | |
и автоматически построить доказательства между концептами. | |
## Для чего это нужно? | |
- **Формализация знаний** - представление утверждений в структурированном виде | |
- **Проверка валидности** - выявление логических ошибок и противоречий | |
- **Построение доказательств** - автоматическое нахождение логических цепочек между концептами | |
- **Оценка достоверности** - выявление слабых мест в структуре аргументации | |
## Как это работает? | |
1. Вы представляете утверждения в виде векторов между концептами (например: "A вызывает B") | |
2. Система анализирует структуру этих векторов и соответствие контрактам | |
3. Система верифицирует векторы, используя базу знаний и правила | |
4. Вы можете построить доказательства между концептами, используя имеющиеся векторы | |
Выберите вкладку ниже, чтобы начать работу: | |
""" | |
) | |
with gr.Tabs(): | |
with gr.TabItem("Анализ и Верификация"): | |
gr.Markdown( | |
""" | |
### Как пользоваться: | |
1. **Введите JSON** с векторами в поле ниже (см. пример) | |
2. **Нажмите кнопку** "Запустить Анализ и Верификацию" | |
3. **Посмотрите результаты** анализа и верификации справа | |
#### Структура входных данных: | |
- `text`: Контекст (опционально) | |
- `vectors`: Массив векторов, каждый из которых содержит: | |
- `id`: Уникальный идентификатор вектора | |
- `source`: Исходный концепт | |
- `target`: Целевой концепт | |
- `type`: Тип связи (Causality, Implication, Definition и т.д.) | |
- `axis`: Ось связи (relationship, logic и т.д.) | |
- `justification`: Обоснование связи | |
""" | |
) | |
with gr.Row(): | |
with gr.Column(scale=1): | |
gr.Markdown("### Входные данные (JSON)") | |
input_json_av = gr.Textbox( | |
lines=15, | |
label="SFOSR JSON", | |
info="Введите JSON с векторами для анализа и верификации", | |
placeholder='{\n "text": "Загрязнение воздуха вызывает респираторные заболевания.",\n "vectors": [\n {\n "id": "V1",\n "source": "ЗагрязнениеВоздуха",\n "target": "РеспираторныеЗаболевания",\n "type": "Causality",\n "axis": "relationship",\n "justification": "Научные исследования подтверждают эту связь."\n }\n ]\n}' | |
) | |
av_button = gr.Button("Запустить Анализ и Верификацию", variant="primary") | |
with gr.Column(scale=1): | |
gr.Markdown("### Результаты Анализа") | |
analysis_output = gr.Markdown() | |
gr.Markdown("### Результаты Верификации") | |
verification_output = gr.Markdown() | |
gr.Markdown("### Детали Проверки Векторов") | |
vector_details_output = gr.JSON(label="Детали по Векторам") | |
gr.Markdown("### Граф Концептов") | |
graph_placeholder_output = gr.Textbox(label="Информация о Графе") # Placeholder | |
gr.Examples( | |
examples=[ | |
[example_verify_json] | |
], | |
inputs=input_json_av, | |
label="Примеры входных данных" | |
) | |
with gr.TabItem("Построение Доказательств / Задачи Логики"): | |
gr.Markdown( | |
""" | |
### Как пользоваться: | |
1. **Подготовьте SFOSR JSON:** | |
- Для обычных задач: Создайте JSON с векторами-посылками. | |
- Для задач типа LogicBench: Используйте внешнюю LLM (например, спросите в чате), чтобы преобразовать текстовый контекст задачи в SFOSR JSON формат. | |
2. **Вставьте JSON** с векторами в поле ниже. | |
3. **Определите цель доказательства:** Исходя из вопроса задачи, определите, какую связь между концептами нужно доказать. | |
Например, для вопроса "Идет ли дождь?" и контекста "Если идет дождь, земля мокрая. Земля сухая.", | |
возможно, нужно доказать связь от "Rain" к "False". | |
4. **Укажите Исходный и Целевой концепты** в соответствующие поля. | |
5. **Нажмите кнопку** "Найти Доказательство". | |
6. **Интерпретируйте результат:** Успешное доказательство (Valid: True) или его отсутствие поможет ответить на исходный вопрос задачи. | |
#### Что такое доказательство? | |
Доказательство - это цепочка логических шагов, которая показывает, как от исходного концепта можно | |
прийти к целевому, используя имеющиеся векторы и правила вывода. Например, если у вас есть | |
векторы "A → B" и "B → C", система может вывести "A → C". | |
""" | |
) | |
with gr.Row(): | |
with gr.Column(scale=1): | |
gr.Markdown("### Входные Данные и Запрос") | |
input_json_p = gr.Textbox( | |
lines=15, # Increased lines for potentially larger JSON | |
label="SFOSR JSON с Векторами", | |
info="Введите JSON с векторами, которые будут использованы как посылки для доказательства (можно сгенерировать из текста через LLM)", | |
placeholder='{\n "vectors": [\n {\n "id": "V1", "source": "КонцептА", "target": "КонцептБ", "type": "Implication", "axis": "logic" \n }\n // ... другие векторы ...\n ]\n}' | |
) | |
source_concept_input = gr.Textbox( | |
label="Исходный Концепт", | |
info="Введите имя концепта, от которого начинается доказательство", | |
placeholder="Например: Rain" | |
) | |
target_concept_input = gr.Textbox( | |
label="Целевой Концепт", | |
info="Введите имя концепта, к которому нужно построить доказательство", | |
placeholder="Например: False" | |
) | |
p_button = gr.Button("Найти Доказательство", variant="primary") | |
with gr.Column(scale=1): | |
gr.Markdown("### Статус Доказательства") | |
proof_status_output = gr.Markdown() | |
gr.Markdown("### Детали Доказательства / Путь") | |
proof_details_output = gr.JSON(label="Структура Доказательства") | |
gr.Examples( | |
examples=[ | |
# Example with manually created proof vectors | |
# [example_proof_json, "ВыбросыЗаводов", "РеспираторныеЗаболевания"], | |
# Example potentially derived from LogicBench task | |
[example_logicbench_proof_json, example_logicbench_source, example_logicbench_target] | |
], | |
inputs=[input_json_p, source_concept_input, target_concept_input], | |
label="Примеры для Построения Доказательств" | |
) | |
with gr.TabItem("Справка"): | |
gr.Markdown( | |
""" | |
## Подробная документация по SFOSR | |
### Типы Векторов | |
SFOSR поддерживает различные типы векторов, каждый из которых представляет определенный вид связи между концептами: | |
- **Causality** - причинно-следственная связь ("A вызывает B") | |
- **Implication** - логическое следование ("Если A, то B") | |
- **Definition** - определение ("A определяется как B") | |
- **PartOf** - отношение часть-целое ("A является частью B") | |
- **IsA** - отношение типа ("A является типом B") | |
- **Action** - действие ("A выполняет действие над B") | |
- **Dependency** - зависимость ("A зависит от B") | |
- **И другие** (см. документацию) | |
### Оси Векторов | |
Каждый вектор относится к определенной оси, которая указывает на область применения связи: | |
- **relationship** - связь между объектами в реальном мире | |
- **logic** - логическая связь | |
- **classification** - таксономическая связь | |
- **process** - связь в процессе | |
- **И другие** (см. документацию) | |
### Процесс Верификации | |
Система проводит несколько уровней проверки для каждого вектора: | |
1. **Синтаксическая валидация** - проверка наличия всех необходимых полей | |
2. **Структурная валидация** - проверка соответствия контрактам и правилам | |
3. **Семантическая валидация** - проверка согласованности с базой знаний | |
### Построение Доказательств | |
Для построения доказательств система использует правила вывода: | |
- **Chain Rule** - "A → B" и "B → C" дает "A → C" | |
- **Causality Transfer** - "A causes B" и "B implies C" дает "A causes C" | |
- **И другие правила** | |
### Дополнительные Ресурсы | |
- [GitHub репозиторий](https://github.com/DanielSwift1992/SFOSR) (Скоро доступен) | |
- [Теоретическая база](https://lesswrong.com/) (Скоро доступен) | |
""" | |
) | |
# --- Event Handlers --- | |
if sfosr_instance: # Only wire up buttons if the system initialized | |
# Analyze & Verify Tab | |
av_button.click( | |
fn=run_analysis_verification, | |
inputs=[input_json_av], | |
outputs=[analysis_output, verification_output, vector_details_output, graph_placeholder_output] | |
) | |
# Construct Proof Tab | |
p_button.click( | |
fn=run_proof_construction, | |
inputs=[input_json_p, source_concept_input, target_concept_input], | |
outputs=[proof_status_output, proof_details_output] | |
) | |
# REMOVED LogicBench Integration Tab Handler | |
else: | |
# Display a persistent error if the system couldn't load | |
gr.Markdown( | |
""" | |
## Ошибка: Система SFOSR не инициализирована | |
Возможные причины: | |
1. Файл базы данных `sfosr.db` не найден | |
2. Проблема с импортом модулей `sfosr_core` | |
3. Ошибка в коде системы | |
Пожалуйста, проверьте логи сервера для получения более подробной информации. | |
""" | |
) | |
# --- Launch the App --- | |
if __name__ == "__main__": | |
demo.launch() # Share=True for public link if needed |