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 |